pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'ec976d3be4'
${ noResults }
infer_clone/sledge/semantics/README.md

3.2 KiB
Raw Blame History

This directory contains a model of the semantics of LLVM, of LLAIR, and of the LLVM to LLAIR translation, along with some theorems about them. It is written in the HOL4 theorem prover.

Building

To build the formalisation, which just gets HOL4 to check the proofs, run the Holmake command in this directory. This requires having HOL4 installed, which itself depends on PolyML.

The directions for installing HOL4 are here https://hol-theorem-prover.org/#get, but essentially it is

git clone https://github.com/HOL-Theorem-Prover/HOL.git
cd HOL
poly < tools/smart-configure.sml
bin/build

PolyML is available here https://www.polyml.org/download.html, but it is widely available from various package managers and easiest to install that way, e.g., on MacOS brew install polyml.

This has been tested on PolyML 5.8, and on HOL4 Github commit e2d0fafdb3ccdd098d2bd6e0aaaacbc9468ae4b1.

What is modelled

The model of the translation is not complete: function calls and exceptions are two notable omissions. However, it covers the other important aspects of the translation:

  • the SSA restrictions on LLVM,

  • building compound expressions to reduce the number of temporary stores in LLAIR,

  • and how the SSA restrictions imply that a simple linear traversal of the (topologically sorted) CFG suffices for the translation,

  • the treatment of LLVM's bitwise 2s complement arithmetic on LLAIR's mathematical integers.

The semantics of LLVM and LLAIR are given as small step abstract state machines, and the translation between them as a pure recursive function.

The semantics of LLVM uses a concrete memory model, i.e., indices into an array of bytes. This means that it does not account for all possible forms of undefined behaviour that could occur with LLVM's more complicated pointer provenance model.

The proof that if an LLVM program doesn't get stuck and has a certain observable behaviour, then the translation to LLAIR also doesn't get stuck and has the same behaviour is complete, except for a few minor cheats. The proof in the other direction, from LLAIR behaviour to LLVM behaviour, is not attempted.

Contents

llairScript.sml : the syntax and semantics of LLAIR

llair_propScript.sml : theorems about various properties of LLAIR's semantics

llvmScript.sml : the syntax and semantics of LLVM

llvm_propScript.sml : theorems about various properties of LLVM's semantics

llvm_ssaScript.sml : the definition of SSA form for LLVM, along with theorems about SSA, dominance, and variable liveness

llvm_to_llairScript.sml : the translation function's definition

llvm_to_llair_propScript.sml : theorems about the LLVM to LLAIR translation that don't mention the semantics, so just those that establish invariants about the translation functions themselves.

llvm_to_llair_sem_propScript.sml : the overall correctness theorems for the translation

memory_modelScript.sml : an abstract model of memory as an array of bytes. It includes reading and writing multi-byte words in little-endian encoding

miscScript.sml : various generic theorems that could in principle be moved into HOL4's libraries

settingsScript.sml : set up HOL4, replacing many of it's ugly UPPERCASE constants with lower case ones