		Search-engine friendly clone of the ACL2 documentation.

X86isa

X86isa-build-instructions

Building books related to the x86 ISA and the machine-code analysis framework.

Some ways of building the x86isa books are:

Using cert.pl top: This build::cert.pl option should work well for most users. Users who want to execute programs that utilize SYSCALL, RDRAND, etc. 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=/Users/shilpi/acl2/saved_acl2 
```
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 (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, 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. Otherwise, you do.