Linux-load
- Signature
(linux-load kernel-image-filename
disk-image-filename
command-line x86 state)
→
(mv x86 state)- Arguments
- kernel-image-filename — Guard (stringp kernel-image-filename).
- disk-image-filename — Guard (stringp disk-image-filename).
- command-line — Guard (stringp command-line).
Definitions and Theorems
Function: linux-load
(defun linux-load (kernel-image-filename disk-image-filename
command-line x86 state)
(declare (xargs :stobjs (x86 state)))
(declare (xargs :guard (and (stringp kernel-image-filename)
(stringp disk-image-filename)
(stringp command-line))))
(let ((__function__ 'linux-load))
(declare (ignorable __function__))
(b*
((x86 (!ctri 0
(logior 1610612752 (ash 1 0) (ash 1 31))
x86))
(kernel-ptr 16777216)
((mv kernel-image state)
(read-file-into-byte-list kernel-image-filename state))
((unless
(canonical-address-p (+ kernel-ptr (len kernel-image))))
(raise
"Kernel too large to load at ~x0, not enough canonical addresses"
kernel-ptr)
(mv x86 state))
((mv & x86)
(write-bytes-to-memory kernel-ptr kernel-image x86))
(zero-page-ptr 4096)
(gdt-ptr (+ zero-page-ptr 4096))
(gdt-size 32)
(command-line-ptr (+ gdt-ptr gdt-size))
(disk-image-ptr 2147483648)
(command-line-c-str (string-to-c-str command-line))
((unless (canonical-address-p (+ command-line-ptr
(len command-line-c-str))))
(raise
"Command line too large to load at ~x0, not enough canonical addresses"
command-line-ptr)
(mv x86 state))
((mv & x86)
(write-bytes-to-memory command-line-ptr
command-line-c-str x86))
((mv disk-image-size x86 state)
(read-file-into-memory disk-image-filename
disk-image-ptr x86 state))
(x86 (init-zero-page zero-page-ptr command-line-ptr
disk-image-ptr disk-image-size
kernel-ptr kernel-image x86))
(cs-descriptor (gdt-entry 41115 0 1048575))
((mv & x86)
(write-bytes-to-memory (+ gdt-ptr 16)
(pack-u64 cs-descriptor)
x86))
(ds-descriptor (gdt-entry 49299 0 1048575))
((mv & x86)
(write-bytes-to-memory (+ gdt-ptr 24)
(pack-u64 ds-descriptor)
x86))
(x86 (!stri *gdtr*
(!gdtr/idtrbits->base-addr
gdt-ptr
(!gdtr/idtrbits->limit (1- gdt-size) 0))
x86))
(x86 (load-segment-reg *cs* 16 cs-descriptor x86))
(x86 (load-segment-reg *ds* 24 ds-descriptor x86))
(x86 (load-segment-reg *es* 24 ds-descriptor x86))
(x86 (load-segment-reg *ss* 24 ds-descriptor x86))
(x86 (!rflags (logand (lognot (ash 1 9)) (rflags x86))
x86))
(x86 (!rgfi *rsi* zero-page-ptr x86))
((unless
(and (> (len kernel-image) 497)
(canonical-address-p (+ kernel-ptr
(* (nth 497 kernel-image) 512)
1024))))
(mv x86 state))
((mv & x86)
(init-x86-state-64 nil
(+ kernel-ptr
(* (nth 497 kernel-image) 512)
1024)
nil nil nil nil nil nil nil (rflags x86)
nil x86)))
(mv x86 state))))
