search

kframework / X86-64-semantics

Semantics of x86-64 in K
Other
134 stars 11 forks source link
k-framework semantics x86-64

readme

X86-64 Semantics

The project presents the most complete and thoroughly tested formal semantics of x86-64 to date. Our semantics faithfully formalizes all the non-deprecated, sequential user-level instructions of the x86-64 Haswell instruction set architecture. This totals 3155 instruction variants, corresponding to 774 mnemonics. The semantics is fully executable and has been tested against more than 7,000 instruction-level test cases and the GCC torture test suite.

User Guide

Prerequisites

NOTE Due to polymorphic sort support, the syntax of machine integers aka MInt has changed a bit and the current x86-64 semantics is not responsive to that. Hence compiling x86-64 semantics using the master k will issue compilation error. Before the x86-64 semantics is ported to the new MInt syntax, it is recommended to

To compile the x86-64 semantics

  cd X86-semantics/semantics
  ../scripts/kompile.pl --backend java

A simple test run -- Concrete execution of a binary (compiled from a C program)

../scripts/run-single-c-file.sh ../tests/program-tests/bubblesort/test.c java |& tee /tmp/run.log

Testing the semantics

Empowered by the fact that we can directly execute the semantics using the K framework, we validated our model by co-simulating it against a real machine. During co-simulation, we execute a machine program on the processor as well as on our K model and compare the execution results after every instruction. The co-simulation experiments are done in the following two phases:

  1. Instruction level validation: Testing individual instructions

    • Batch testing: All the tests in a directory are fired in parallel. The test-cases are specified in a file named filelist.txt 
      cd tests/single-instruction-tests
./run-tests.sh --all [--jobs 5]
// Which subsumes the following sequence of commands
// ./run-tests.sh --cleankstate // Remove the old krun output logs.
// ./run-tests.sh --cleanxstate // Remove the old gdb script output logs.
// ./run-tests.sh --cleancstate //  Remove the old compare logs
// ./run-tests.sh --kstate      // Collect the semantics of all the
                              // instructions composing all the
                              // test-cases, Compile the X86 semantics
                              // using the collected instruction
                              // semnatics, and Execute krun on each of
                              // the test-case.
// ./run-tests.sh --xstate      // Execute dn script and generate logs.
// ./run-tests.sh --compare     // Compare the krun ad gdb script logs.
    • Individual testing: Running each test in isolation. 
      cd tests/single-instruction-tests/adc
make collect  // Collect semantic rules of all the instructions composing
          // the test-case
make kompile  // Compile the X86 semantics using the collected instruction
          // semnatics.
make cleanktest   //  Remove the old krun output logs.
make cleanxstate  //  Remove the old gdb script output logs.
make cleancstate  //  Remove the old compare logs
make ktest        //  Execute krun on the test-case and generate krun logs.
make xstate       //  Execute dn script and generate logs.
make comapre      //  Compare the krun ad gdb script logs.

  2. Program level validation: Testing combination of instructions as a part of real-world programs.

    cd tests/program-tests
./run-tests.sh --cleankstate
./run-tests.sh --kstate

Developer Guide

Dependency tree of Source Code

Directory structure