X86isa-build-instructions
Building books related to the x86 ISA and the machine-code
analysis framework.
Note: If you intend on running a kernel in the x86 model,
like Linux, then you will NOT use the app-view, so the value of
X86ISA_EXEC (described below) is not relevant for your use case.
app-view is used for running user software in the x86 model without
running a kernel by specifying the semantics of syscalls provided by the
kernel in the logic and (depending on the value of X86ISA_EXEC)
potentially passing through syscalls to the machine ACL2 is running on in
execution. See the app-view doc topic for more information.
Some ways of building the x86isa books are:
-
Using cert.pl top in the books/projects/x86isa directory of the
ACL2 source tree: This build::cert.pl option should work well for most
users. Users who want to execute programs that utilize SYSCALL,
RDRAND, etc. in app-view should consider the option listed
below.
-
Using the Makefile provided with the x86isa books: Users of these
books who wish to simulate x86 programs with non-deterministic computations
like SYSCALL (in app-view) should use the Makefile provided with
x86isa and run make with X86ISA_EXEC set to t (which is the
default value).
make JOBS=8 \
X86ISA_EXEC=t \
ACL2=/path/to/saved_acl2
in the books/projects/x86isa directory of the ACL2 source tree where
the number of jobs to be run in parallel in this example is 8. Note that we
use JOBS here instead of the -j flag.
When X86ISA_EXEC is t, some dynamic C libraries that are
used in the model for supporting the execution of SYSCALL in the
application-level view will be built. Since we rely on the foreign
function interface of Clozure
CL (CCL), full execution support is available only if you use
CCL.
Values of X86ISA_EXEC other than t will not allow the execution
of SYSCALL instructions in app-view (as may be the case with
using other Lisps as well). Note that reasoning about these instructions
will still be possible. Execution and reasoning about all other instructions
will always be possible, irrespective of X86ISA_EXEC or the underlying
Lisp.
IMPORTANT: You should do a "make clean" (or "make
execclean" if you are in a hurry) if you wish to certify the books
with a different value of X86ISA_EXEC.
-
Using the "everything" target of the ACL2 Community
Books (see acl2/books/GNUmakefile): This is essentially the same as executing
cert.pl books/projects/x86isa/top. This will build the x86 books without
full execution support in app-view, i.e., the effect will be the same
as building these books with X86ISA_EXEC=nil, even though the Makefile
provided with the x86isa books will not be used.
Suppose you had certified these books previously, but you have
since forgotten whether you built them with X86ISA_EXEC=t or not.
Here is a way of checking the certified books to see if you have full
execution support. Look at the following file:
machine/syscalls.cert.out. If this file contains the
following:
X86ISA_EXEC Warning: environment-and-syscalls-raw.lsp is not
included.
then you do not have SYSCALL execution support in app-view.
Otherwise, you do.
