From ac1263302b1f598d51123d123db2e602c6d7404d Mon Sep 17 00:00:00 2001 From: santiago Date: Wed, 24 Aug 2022 14:26:39 -0400 Subject: [PATCH 01/23] Add a tutorial for Heapster --- heapster-saw/doc/tutorial/tutorial.md | 594 ++++++++++++++++++++++++++ 1 file changed, 594 insertions(+) create mode 100644 heapster-saw/doc/tutorial/tutorial.md diff --git a/heapster-saw/doc/tutorial/tutorial.md b/heapster-saw/doc/tutorial/tutorial.md new file mode 100644 index 0000000000..ae40eadb64 --- /dev/null +++ b/heapster-saw/doc/tutorial/tutorial.md @@ -0,0 +1,594 @@ +# Tutorial to learn the basics of heapster-saw + +This tutorial extends the current README with enough details and +examples to get anyone up to speed with using and hacking on Heapster. + +## Building + +We'll start by building everything you need to use Heapster. All the +commands here are with respect to the top-level saw-script directory. + +### Build Saw + +You will need to follow the instructions in the top-level README to +download or build a SAW binary, of which Heapster is a part. In +particular, make sure you follow the instructions to install Z3. Once `./build.sh` +succeeds it should report + +```bash +COPIED EXECUTABLES TO /Path/To/Saw/saw-script/bin. +``` + +If everything is installed correctly you should be able to run saw + +```bash +cabal run saw +``` + +This should open the saw interactive session. It should show you a +pretty SAW logo with the version number. We will learn more about the +interactive session later. For now you can quit the session with `:quit` or +`:q` like so: + +```bash +sawscript> :quit +``` + +### Build the Coq backend for Saw + +In this tutorial we will also interact with Heapster's Coq output. So you'll need +to follow the instructions in the README in the `saw-core-coq` subdirectory. +Specifically, after installing the dependencies, you will need to run the +following (from this directory): +```bash +cd /saw-core-coq/coq +make +``` + +It is expected that you will see a large number of warnings, but the +build should complete without any errors. + +**TODO: How do we check if this is properly installed before continuing?** + +Before continuing, return to the top-level directory with `cd ..`. + +### Build all the examples + +The easiest way to verify that everything has been set up correctly is +to build all the heapser examples. Simply go to the examples folder +and build, like so + +```bash +cd /heapster-saw/examples +make +``` +You will see several files build that looks like this: +```bash +COQC global_var_gen.v +COQC global_var_proofs.v +COQC sha512_gen.v +``` + +It will take several minutes and it should complete without any +errors. Once it's done, you know you are ready to use Heapser! + +## A quick tour of SAW + +You don't need to be an expert in SAW to handle Heapster, but a little +familiarity is useful. If you want to dig deeper into SAW, there is a +dedicated [tutorial](https://saw.galois.com/tutorial.html) for +that. Here we just present the general ideas of SAW. + +### Overview + +SAWScript is a special-purpose programming language developed by +Galois to help orchestrate and track the results of the large +collection of proof tools necessary for analysis and verification of +complex software artifacts. + +In this tutorial we will overview how to use SAW to proof functional +equality different implementations. The steps are as follows: + +1. Compile the code down to llvm bitecode (i.e. `.bc` files) +2. Run the saw interpreter +3. Load the file and extract the two function specifications. +4. Define the equality theorem. +5. Call the SAT/SMT solver to prove the theorem. + +Steps 3-5 can all be written in a single `.saw` file, and batch processed by SAW. + +### Running an example + +We will use the same `ffs` example used in the [SAW +tutorial](https://saw.galois.com/tutorial.html). Head over to the +`saw-script/doc/tutorial/code` directory to find the file. + +Our aim is to prove functional equivalence of two implementatinos fo +`ffs` (there are more implementations in that file). The function is +should return the index of the first non-zero bit of it's input and +can be implemented in the follwoing two ways. + +```C +uint32_t ffs_ref(uint32_t word) { + int i = 0; + if(!word) + return 0; + for(int cnt = 0; cnt < 32; cnt++) + if(((1 << i++) & word) != 0) + return i; + return 0; // notreached +} + +uint32_t ffs_imp(uint32_t i) { + char n = 1; + if (!(i & 0xffff)) { n += 16; i >>= 16; } + if (!(i & 0x00ff)) { n += 8; i >>= 8; } + if (!(i & 0x000f)) { n += 4; i >>= 4; } + if (!(i & 0x0003)) { n += 2; i >>= 2; } + return (i) ? (n+((i+1) & 0x01)) : 0; +} +``` + +The former loops over all the bits in the input until it finds the +first 1. The later does a binary search over the input by using masks +where there is a 1. + +#### 1. Compile the code. + + We can use clang to compile our C code down + to LLVM like so: + + ```bash + clang -g -c -emit-llvm -o ffs.bc ffs.c + ``` + + Where the options mean: + * The `-g` flag instructs clang to include debugging information, which is useful in SAW to refer to variables and struct fields using the same names as in C. + * The `-c` flag asks clang to only run preprocess, compile, and assemble steps. + * `-emit-llvm` requests llvm bitecode as output. + * `-o ffs.bc` tells clang to write the output into `ffs.bc` + +Luckily, SAW has some code to do all of this for you in the `Makefile`. You can simply run +```bash +> make ffs.bc +``` +to get the same effect. + +#### 2. Run the saw interpreter + +Run `cabal run saw` to start the interpreter. You should see the SAW +logo and version number. Then you cna run your first saw command: + + ```bash + sawscript> print "Hello World" + [14:49:30.413] Hello World + ``` + +#### 3. Load the file and extract the two function specifications. + To load the file, we will use `llvm_load_module`. We can check what the function does with + + ``` bash + sawscript> :? llvm_load_module + Description + ----------- + + llvm_load_module : String -> TopLevel LLVMModule + + Load an LLVM bitcode file and return a handle to it. + ``` + + Also, if you ever forget the name of a function, you cna find it by + running `:env` which will display the current sawscript + environment. Finally you can allways type `:help` to remember these + commands. + + So, run `l <- llvm_load_module "ffs.bc"` to load the file and stored in variable `l`. If you print the environment with `:env` you will now see a new variable `l : LLVMModule`. + + Now from `l`, we want to extract the two functions + + ``` + sawscript> ffs_ref <- llvm_extract l "ffs_ref" + sawscript> ffs_imp <- llvm_extract l "ffs_imp" + ``` + + That's it! If you want, you can check again `:env` to confirm the + variables of type `Term` have been created. + +#### 4. Define the equality theorem. + + Our theorem can now refer to the two recently created terms. since + we want to prove functional equivalence, we just state that the + functions are equal for all inputs. + + ``` + sawscript> let thm1 = {{ \x -> ffs_ref x == ffs_imp x }}; + ``` + + If you check the environment (`:env`) you will see that theorems are also of type `Term`. + +#### 5. Call the SAT/SMT solver to prove the theorem. + +Let's start by checking the command we will use `prove`: + +```bash +sawscript> :? prove +Description +----------- + + prove : ProofScript () -> Term -> TopLevel ProofResult + +Use the given proof script to attempt to prove that a term is valid +(true for all inputs). Returns a proof result that can be analyzed +with 'caseProofResult' to determine whether it represents a successful +proof or a counter-example. +``` + +Notice that it takes a `ProofScript`. You can look at the +environment (`:env`) and look at all the proof scripts (searching +for `ProofScript`), such as `abc`, `cvc4`, `mathsat`, and `z3`. If +you want to play with different solvers you would have to install +them. For now, since we have `z3` installed we can call. + +```bash +sawscript> result <- prove z3 thm1 +sawscript> print result +[16:39:47.506] Valid +``` + +Which tells us that z3 managed to prove the functional equality! + +### Batch scripts + +To make things easier, you can write all the code above into a single +`.saw` file and process it in a batch. The file `ffs.saw` would look like this: + +```bash +print "Loading module ffs.bc"; +l <- llvm_load_module "ffs.bc"; + +print "Extracting reference term: ffs_ref"; +ffs_ref <- llvm_extract l "ffs_ref"; + +print "Extracting implementation term: ffs_imp"; +ffs_imp <- llvm_extract l "ffs_imp"; + +print "Proving equivalence: ffs_ref == ffs_imp"; +let thm1 = {{ \x -> ffs_ref x == ffs_imp x }}; +result <- prove z3 thm1; +print result; + +print "Done." +``` + +If you save the file in the same directory you can run: +```bash +% cabal run saw -- ffs.saw +Up to date + +[16:49:13.646] Loading file "/PATH/TO/SAW/saw-script/doc/tutorial/code/my_ffs.saw" +[16:49:13.647] Loading module ffs.bc +[16:49:13.651] Extracting reference term: ffs_ref +[16:49:13.663] Extracting implementation term: ffs_imp +[16:49:13.666] Proving equivalence: ffs_ref == ffs_imp +[16:49:13.716] Valid +[16:49:13.716] Done. +``` + +That's it! You know the basics of SAW. + +## Using Heapster + +Heapster is a, fundamentally, a type system for extracting functional +specifications from memory-safe imperative programs. The type system, +defined inside SAW, uses separation types to reason about memory +safety. Once a program is type-checked as memory-safe, it can be then +extracted as a functional program to be verified in Coq. + +**TODO: Double check this description of Heapster** + +### Overview + +Heapster allows us to (1) type check programs with respect to +types/specifications that can express separation loigc and (2) extract +the resulting functional program to Coq for further verification. + +The process will generally involve + +1. Generating LLVM bitcode from your file +2. Run the saw interpreter with Heapster +3. Load the file and extract the functions. +4. Writing heapster specifications for your functions +5. Writing a SAW script to type-check your code with respect to the + sepcification, and +6. Writing a Coq file to prove things about the generated functional + specification(s). + +Just like with SAW, Heapster can be processed in batch. To do so, you +can combine steps 2-6 in a `.saw` file and use SAW's batch processing. + +### Running an example + +This section will walk through the process of using Heapster to write +and verify some C code. Specifially, we want to verify the function +`is_elem`, which tests if a specific value is in a list. The function, +together with others, can be found in `examples/linked_list.c`. + +```C +typedef struct list64_t { + int64_t data; + struct list64_t *next; +} list64_t; + +int64_t is_elem (int64_t x, list64_t *l) { + if (l == NULL) { + return 0; + } else if (l->data == x) { + return 1; + } else { + return is_elem (x, l->next); + } +} +``` + +#### 1. Generating LLVM bitcode + +Just like with SAW, we want to work with the LLVM bitcode (`.bc`), so +you can generate it just like before. Note that we have already +included the binary for all the examples so you don't really need to +run this command. + + ```bash + clang -g -c -emit-llvm -o ffs.bc ffs.c + ``` + +(The alternative command `make examples/linked_list.bc` won't work +because the shorcut is not defined in the Makefile of heapster.) + +Be aware that the resulting bitcode may depend on your `clang` version and your +operating system. In turn, this means the Heapster commands in your SAW script +and the proofs in your Coq file may also be dependent on how and where the +bitcode is generated. If you find an incompatibility, please report it. + +#### 2. Run the SAW interpreter with Heapster + +We start by running saw with `cabal run saw`. Once SAW is loaded, you +can load all the Heapster commands with + + ```bash + sawscript> enable_experimental + ``` + +If you print the environment now (wiht `:env`) you will notice a new +set of commands, all starting with `heapster_*`. You can also start +typing the name and press tab to see all the functions those are all the Heapster commands. + +sawscript> heapster_ [TAB] +heapster_assume_fun heapster_find_symbols +heapster_assume_fun_multi heapster_find_symbols_with_type +heapster_assume_fun_rename heapster_find_trait_method_symbol +heapster_assume_fun_rename_prim heapster_gen_block_perms_hint +heapster_block_entry_hint heapster_get_cfg +heapster_define_irt_recursive_perm heapster_init_env +heapster_define_irt_recursive_shape heapster_init_env_debug +heapster_define_llvmshape heapster_init_env_for_files +heapster_define_opaque_llvmshape heapster_init_env_for_files_debug +heapster_define_opaque_perm heapster_init_env_from_file +heapster_define_perm heapster_init_env_from_file_debug +heapster_define_reachability_perm heapster_join_point_hint +heapster_define_recursive_perm heapster_parse_test +heapster_define_rust_type heapster_print_fun_trans +heapster_define_rust_type_qual heapster_set_debug_level +heapster_export_coq heapster_set_translation_checks +heapster_find_symbol heapster_typecheck_fun +heapster_find_symbol_commands heapster_typecheck_fun_rename +heapster_find_symbol_with_type heapster_typecheck_mut_funs + +You can the use `:?` to see further information for each of them. + + +#### 3. Load the file and extract the two function specifications. + +To load a file into heapster you can use `heapster_init_env`. Let's +check it's documentation first + +``` bash +sawscript> :help heapster_init_env +Description +----------- + +EXPERIMENTAL + +heapster_init_env : String -> String -> TopLevel HeapsterEnv + +Create a new Heapster environment with the given SAW module name +from the named LLVM bitcode file. +``` + +As you see it takes two names. The first, is the name of the SAW core +module where Heapster will write all the specifications we extract. If +you start with a fresh name, Heapster will autogenerate a new module +for you. We will see later how to use existisng modules. The second +name referse to the bitecode file containing the code we are +verifying. + +The function returns a Heapster environment that contains all the +definitions of the module (not to be confused with the SAW environment +that can be printed wiht `:env`). + +Let's load our module with + +``` +env <- heapster_init_env "linked_list" "examples/linked_list.bc"; +``` + +we have created a new Heapster environment that we can explore. + +``` +sawscript> print env +[20:19:48.436] Module: examples/linked_list.bc +Types: + %struct.list64_t = type { i64, %struct.list64_t* } + +Globals: + +External references: + declare default void @llvm.dbg.declare(metadata, metadata, + metadata) + declare default i8* @malloc(i64) + +Definitions: + i64 @is_head(i64 %0, %struct.list64_t* %1) + i64 @is_elem(i64 %0, %struct.list64_t* %1) + i64 @any(i64(i64)* %0, %struct.list64_t* %1) + %struct.list64_t* @find_elem(i64 %0, %struct.list64_t* %1) + %struct.list64_t* @sorted_insert(i64 %0, %struct.list64_t* %1) + %struct.list64_t* @sorted_insert_no_malloc(%struct.list64_t* %0, + %struct.list64_t* %1) +``` + +The heapster environment contains all the types, global definitions, +external references and functions from the loaded module. + + +#### 4. Writing heapster specifications for your functions + +##### Pen and paper specification + +Before we go foward using Heapster, let's think about what the +specification for `is_elem` should be. As we can check in the +environment `env`, `is_elem` takes a 64-bit integer the "element". + +```LLVM +i64 @is_elem(i64 %0, %struct.list64_t* %1) +``` + +Hence, precondition to the function should reflect these two inputs +like so `arg0:int64, arg1: list int64`, for some predicates `int64` +and `list` that express a single integer and a list of them. + +Moreover, the function returns a new i64-bit integer and, as we can +see in the code of `is_elem`, the arguments are not modified. So the +postcondition, of the function could be described by `arg0:int64, +arg1: list int64, ret:int64`. Alternatively, if we don't care about +the inputs after the call we can simplify it to `arg0:true, arg1: +true, ret:int64`, where `true` is a predicate the is always satisfied. + +Then, using the linear implication `-o` we can express the +specification of `is_elem` as + +``` +arg0:int64, arg1: list int64 -o arg0:true, arg1:true, ret:int64 +``` + +Notice that this is a memory-safety specification, not a correctness +predicate. We can reason about the correctness of the function once we +extract it as a functional program in Coq. + +In the next sections, we shall define the predicates necessary to +write this specification in Heapster. + +##### Defining permission predicates + +One of the simplest Heapster commands is `heapster_define_perm`, which defines +a new named permission which can then be used in Heapster types. As an +example, the following defines the permission which describes a 64-bit integer +value: + +``` +heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))" +``` + +The first argument is the Heapster environment, the second is its +name, the third is its arguments (of which there are none), the fourth +is the type of value that the permission applies to, and the fifth is +its definition. the new permission is created and added to the +environment. **TODO: Can I print the new permission? `print env` does +not show new permission definintions.** + +The permission predicate for lists is a little more complicated +because it requires a recursive definition. To define +[permissions](doc/Permissions.md) which can describe unbounded data +structures, you can use the `heapster_define_recursive_perm` +command. As an example, here is how to describe a linked list of +64-bit words using this command: + +``` +heapster_define_recursive_perm + env + "List64" + "rw:rwmodality" + "llvmptr 64" + ["eq(llvmword(0))", "ptr((rw,0) |-> int64<>) * ptr((rw,8) |-> List64)"] + "List (Vec 64 Bool)" + "foldList (Vec 64 Bool)" + "unfoldList (Vec 64 Bool)"; +``` + +Its first four arguments are the same as for `heapster_define_perm`, +its fifth argument contains its different inductive cases (in this +case, a `List64` is either a null pointer, or a pointer to an `Int64` +and another `List64`), and its final three arguments are its +translation into SAW core. Here the SAW core definitions used are from +the SAW core prelude which are included by default when Heapster +autogenerates a a module for you. If you need new SAW core +definitions, you will need to use the following command instead of +`heapster_init_env`: + +``` +env <- heapster_init_env_from_file "my_file.sawcore" "my_file.bc"; +``` + +See this [additional documentation](doc/Permissions.md) for a +reference on the syntax and meaning of heapster permissions. + +#### 5. Writing a SAW script to type-check your code with respect to the sepcification + +We begin by converting the pen-and-paper specification of `is_elem` +into a Heapster specification. First, every heapster type begins with +the declaration of a ghost environment. Our specification doesn't use +any ghost variable so that is `().` Moreover, for every predicate we +use, we must specify whether the location is readble-only `` or +both readable and writable `<>`. Whith this we can write our specification as + +``` +().arg0:int64<>, arg1:List64 -o arg0:true, arg1:true, +ret:int64<> +``` + +Finally, to actually type-check a function you can use +`heapster_typecheck_fun`. That takes the environment, the name of the +function to type-check and the type, like so + +``` +heapster_typecheck_fun env "is_elem" +"().arg0:int64<>, arg1:List64 -o arg0:true, arg1:true, +ret:int64<>"; +``` + +Note that for more complicated examples, usually examples involving loops, +the `heapster_block_entry_hint` command will also need to be used in order for +the `heapster_typecheck_fun` command to succeed. In the case of functions with +loops, this hint corresponds to a loop invariant. Additionally, such examples +will also often require your unbounded data structure to be defined as a +reachability permission, using `heapster_define_reachability_perm`, instead of +just as a recursive permission. See `examples/iter_linked_list.saw` for some +examples of using the commands mentioned in this paragraph. + +Once you're finished, use the following command to export all the type-checked +functions in the current environment as functional specifications in Coq. By +convention, we add a `_gen` suffix to the filename. +``` +heapster_export_coq env "my_file_gen.v"; +``` + +#### 6. Writing a Coq file to prove things about the generated functional specification(s) + +**TODO** + +## Looking under the hood + +### Heapster commands and environments + +### Permissions + +### Type-checking From 85749f6a7fad2c7ecf06b56fe3497fd2e3f9e8a7 Mon Sep 17 00:00:00 2001 From: santiago Date: Wed, 24 Aug 2022 14:46:53 -0400 Subject: [PATCH 02/23] Fix typo and missed quotations. --- heapster-saw/doc/tutorial/tutorial.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/heapster-saw/doc/tutorial/tutorial.md b/heapster-saw/doc/tutorial/tutorial.md index ae40eadb64..e47c1310f6 100644 --- a/heapster-saw/doc/tutorial/tutorial.md +++ b/heapster-saw/doc/tutorial/tutorial.md @@ -362,6 +362,7 @@ If you print the environment now (wiht `:env`) you will notice a new set of commands, all starting with `heapster_*`. You can also start typing the name and press tab to see all the functions those are all the Heapster commands. +``` sawscript> heapster_ [TAB] heapster_assume_fun heapster_find_symbols heapster_assume_fun_multi heapster_find_symbols_with_type @@ -382,8 +383,9 @@ heapster_export_coq heapster_set_translation_checks heapster_find_symbol heapster_typecheck_fun heapster_find_symbol_commands heapster_typecheck_fun_rename heapster_find_symbol_with_type heapster_typecheck_mut_funs +``` -You can the use `:?` to see further information for each of them. +You can then use `:?` to see further information for each of them. #### 3. Load the file and extract the two function specifications. From 4c1d22da54d122f06aa019e7191185d744239023 Mon Sep 17 00:00:00 2001 From: santiago Date: Wed, 24 Aug 2022 15:00:52 -0400 Subject: [PATCH 03/23] Add TOC --- heapster-saw/doc/tutorial/tutorial.md | 38 ++++++++++++++++++++++++++- 1 file changed, 37 insertions(+), 1 deletion(-) diff --git a/heapster-saw/doc/tutorial/tutorial.md b/heapster-saw/doc/tutorial/tutorial.md index e47c1310f6..08dc7e3674 100644 --- a/heapster-saw/doc/tutorial/tutorial.md +++ b/heapster-saw/doc/tutorial/tutorial.md @@ -3,12 +3,48 @@ This tutorial extends the current README with enough details and examples to get anyone up to speed with using and hacking on Heapster. + +**Table of Contents** + +- [Tutorial to learn the basics of heapster-saw](#tutorial-to-learn-the-basics-of-heapster-saw) + - [Building](#building) + - [Build Saw](#build-saw) + - [Build the Coq backend for Saw](#build-the-coq-backend-for-saw) + - [Build all the examples](#build-all-the-examples) + - [A quick tour of SAW](#a-quick-tour-of-saw) + - [Overview](#overview) + - [Running an example](#running-an-example) + - [1. Compile the code.](#1-compile-the-code) + - [2. Run the saw interpreter](#2-run-the-saw-interpreter) + - [3. Load the file and extract the two function specifications.](#3-load-the-file-and-extract-the-two-function-specifications) + - [4. Define the equality theorem.](#4-define-the-equality-theorem) + - [5. Call the SAT/SMT solver to prove the theorem.](#5-call-the-satsmt-solver-to-prove-the-theorem) + - [Batch scripts](#batch-scripts) + - [Using Heapster](#using-heapster) + - [Overview](#overview-1) + - [Running an example](#running-an-example-1) + - [1. Generating LLVM bitcode](#1-generating-llvm-bitcode) + - [2. Run the SAW interpreter with Heapster](#2-run-the-saw-interpreter-with-heapster) + - [3. Load the file and extract the two function specifications.](#3-load-the-file-and-extract-the-two-function-specifications-1) + - [4. Writing heapster specifications for your functions](#4-writing-heapster-specifications-for-your-functions) + - [Pen and paper specification](#pen-and-paper-specification) + - [Defining permission predicates](#defining-permission-predicates) + - [5. Writing a SAW script to type-check your code with respect to the sepcification](#5-writing-a-saw-script-to-type-check-your-code-with-respect-to-the-sepcification) + - [6. Writing a Coq file to prove things about the generated functional specification(s)](#6-writing-a-coq-file-to-prove-things-about-the-generated-functional-specifications) + - [Looking under the hood](#looking-under-the-hood) + - [Heapster commands and environments](#heapster-commands-and-environments) + - [Permissions](#permissions) + - [Type-checking](#type-checking) + + + + ## Building We'll start by building everything you need to use Heapster. All the commands here are with respect to the top-level saw-script directory. -### Build Saw +### Build Saw You will need to follow the instructions in the top-level README to download or build a SAW binary, of which Heapster is a part. In From 9a858c63f4a789468ba8b5c4bcf2711612856e86 Mon Sep 17 00:00:00 2001 From: santiago Date: Wed, 24 Aug 2022 15:01:56 -0400 Subject: [PATCH 04/23] Simplify TOC --- heapster-saw/doc/tutorial/tutorial.md | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/heapster-saw/doc/tutorial/tutorial.md b/heapster-saw/doc/tutorial/tutorial.md index 08dc7e3674..82d6219730 100644 --- a/heapster-saw/doc/tutorial/tutorial.md +++ b/heapster-saw/doc/tutorial/tutorial.md @@ -14,23 +14,10 @@ examples to get anyone up to speed with using and hacking on Heapster. - [A quick tour of SAW](#a-quick-tour-of-saw) - [Overview](#overview) - [Running an example](#running-an-example) - - [1. Compile the code.](#1-compile-the-code) - - [2. Run the saw interpreter](#2-run-the-saw-interpreter) - - [3. Load the file and extract the two function specifications.](#3-load-the-file-and-extract-the-two-function-specifications) - - [4. Define the equality theorem.](#4-define-the-equality-theorem) - - [5. Call the SAT/SMT solver to prove the theorem.](#5-call-the-satsmt-solver-to-prove-the-theorem) - [Batch scripts](#batch-scripts) - [Using Heapster](#using-heapster) - [Overview](#overview-1) - [Running an example](#running-an-example-1) - - [1. Generating LLVM bitcode](#1-generating-llvm-bitcode) - - [2. Run the SAW interpreter with Heapster](#2-run-the-saw-interpreter-with-heapster) - - [3. Load the file and extract the two function specifications.](#3-load-the-file-and-extract-the-two-function-specifications-1) - - [4. Writing heapster specifications for your functions](#4-writing-heapster-specifications-for-your-functions) - - [Pen and paper specification](#pen-and-paper-specification) - - [Defining permission predicates](#defining-permission-predicates) - - [5. Writing a SAW script to type-check your code with respect to the sepcification](#5-writing-a-saw-script-to-type-check-your-code-with-respect-to-the-sepcification) - - [6. Writing a Coq file to prove things about the generated functional specification(s)](#6-writing-a-coq-file-to-prove-things-about-the-generated-functional-specifications) - [Looking under the hood](#looking-under-the-hood) - [Heapster commands and environments](#heapster-commands-and-environments) - [Permissions](#permissions) From d78e61a511a7c4f52e9396a245bb53462234bb5c Mon Sep 17 00:00:00 2001 From: santiago Date: Wed, 24 Aug 2022 15:07:00 -0400 Subject: [PATCH 05/23] Clean TOCs and typo --- heapster-saw/doc/tutorial/tutorial.md | 30 +++++++++++++-------------- 1 file changed, 14 insertions(+), 16 deletions(-) diff --git a/heapster-saw/doc/tutorial/tutorial.md b/heapster-saw/doc/tutorial/tutorial.md index 82d6219730..fdd5fef53a 100644 --- a/heapster-saw/doc/tutorial/tutorial.md +++ b/heapster-saw/doc/tutorial/tutorial.md @@ -16,7 +16,7 @@ examples to get anyone up to speed with using and hacking on Heapster. - [Running an example](#running-an-example) - [Batch scripts](#batch-scripts) - [Using Heapster](#using-heapster) - - [Overview](#overview-1) + - [Heapster type-checking overview](#heapster-type-checking-overview) - [Running an example](#running-an-example-1) - [Looking under the hood](#looking-under-the-hood) - [Heapster commands and environments](#heapster-commands-and-environments) @@ -112,11 +112,11 @@ complex software artifacts. In this tutorial we will overview how to use SAW to proof functional equality different implementations. The steps are as follows: -1. Compile the code down to llvm bitecode (i.e. `.bc` files) -2. Run the saw interpreter -3. Load the file and extract the two function specifications. -4. Define the equality theorem. -5. Call the SAT/SMT solver to prove the theorem. +[1. Compile the code down to llvm bitecode (i.e. `.bc` files).](#1-compile-the-code) +[2. Run the saw interpreter](#2-run-the-saw-interpreter) +[3. Load the file and extract the two function specifications.](#3-load-the-file-and-extract-the-two-function-specifications) +[4. Define the equality theorem.](#4-define-the-equality-theorem) +[5. Call the SAT/SMT solver to prove the theorem.](#5-call-the-satsmt-solver-to-prove-the-theorem) Steps 3-5 can all be written in a single `.saw` file, and batch processed by SAW. @@ -301,7 +301,7 @@ That's it! You know the basics of SAW. ## Using Heapster -Heapster is a, fundamentally, a type system for extracting functional +Heapster is, fundamentally, a type system for extracting functional specifications from memory-safe imperative programs. The type system, defined inside SAW, uses separation types to reason about memory safety. Once a program is type-checked as memory-safe, it can be then @@ -309,7 +309,7 @@ extracted as a functional program to be verified in Coq. **TODO: Double check this description of Heapster** -### Overview +### Heapster type-checking overview Heapster allows us to (1) type check programs with respect to types/specifications that can express separation loigc and (2) extract @@ -317,14 +317,12 @@ the resulting functional program to Coq for further verification. The process will generally involve -1. Generating LLVM bitcode from your file -2. Run the saw interpreter with Heapster -3. Load the file and extract the functions. -4. Writing heapster specifications for your functions -5. Writing a SAW script to type-check your code with respect to the - sepcification, and -6. Writing a Coq file to prove things about the generated functional - specification(s). +[1. Generating LLVM bitcode](#1-generating-llvm-bitcode) +[2. Run the SAW interpreter with Heapster](#2-run-the-saw-interpreter-with-heapster) +[3. Load the file and extract the two function specifications.](#3-load-the-file-and-extract-the-two-function-specifications-1) +[4. Writing heapster specifications for your functions](#4-writing-heapster-specifications-for-your-functions) +[5. Writing a SAW script to type-check your code with respect to the sepcification](#5-writing-a-saw-script-to-type-check-your-code-with-respect-to-the-sepcification) +[6. Writing a Coq file to prove things about the generated functional specification(s)](#6-writing-a-coq-file-to-prove-things-about-the-generated-functional-specifications) Just like with SAW, Heapster can be processed in batch. To do so, you can combine steps 2-6 in a `.saw` file and use SAW's batch processing. From 963d402c8be256304555318fe6f4538c7660a8fc Mon Sep 17 00:00:00 2001 From: santiago Date: Wed, 24 Aug 2022 15:23:49 -0400 Subject: [PATCH 06/23] Minnor fixes --- heapster-saw/doc/tutorial/tutorial.md | 42 +++++++++++++++------------ 1 file changed, 23 insertions(+), 19 deletions(-) diff --git a/heapster-saw/doc/tutorial/tutorial.md b/heapster-saw/doc/tutorial/tutorial.md index fdd5fef53a..65fa250c06 100644 --- a/heapster-saw/doc/tutorial/tutorial.md +++ b/heapster-saw/doc/tutorial/tutorial.md @@ -112,11 +112,11 @@ complex software artifacts. In this tutorial we will overview how to use SAW to proof functional equality different implementations. The steps are as follows: -[1. Compile the code down to llvm bitecode (i.e. `.bc` files).](#1-compile-the-code) -[2. Run the saw interpreter](#2-run-the-saw-interpreter) -[3. Load the file and extract the two function specifications.](#3-load-the-file-and-extract-the-two-function-specifications) -[4. Define the equality theorem.](#4-define-the-equality-theorem) -[5. Call the SAT/SMT solver to prove the theorem.](#5-call-the-satsmt-solver-to-prove-the-theorem) +- [1. Compile the code down to llvm bitecode (i.e. `.bc` files).](#1-compile-the-code) +- [2. Run the saw interpreter](#2-run-the-saw-interpreter) +- [3. Load the file and extract the two function specifications.](#3-load-the-file-and-extract-the-two-function-specifications) +- [4. Define the equality theorem.](#4-define-the-equality-theorem) +- [5. Call the SAT/SMT solver to prove the theorem.](#5-call-the-satsmt-solver-to-prove-the-theorem) Steps 3-5 can all be written in a single `.saw` file, and batch processed by SAW. @@ -317,12 +317,12 @@ the resulting functional program to Coq for further verification. The process will generally involve -[1. Generating LLVM bitcode](#1-generating-llvm-bitcode) -[2. Run the SAW interpreter with Heapster](#2-run-the-saw-interpreter-with-heapster) -[3. Load the file and extract the two function specifications.](#3-load-the-file-and-extract-the-two-function-specifications-1) -[4. Writing heapster specifications for your functions](#4-writing-heapster-specifications-for-your-functions) -[5. Writing a SAW script to type-check your code with respect to the sepcification](#5-writing-a-saw-script-to-type-check-your-code-with-respect-to-the-sepcification) -[6. Writing a Coq file to prove things about the generated functional specification(s)](#6-writing-a-coq-file-to-prove-things-about-the-generated-functional-specifications) +- [1. Generating LLVM bitcode](#1-generating-llvm-bitcode) +- [2. Run the SAW interpreter with Heapster](#2-run-the-saw-interpreter-with-heapster) +- [3. Load the file and extract the two function specifications.](#3-load-the-file-and-extract-the-two-function-specifications-1) +- [4. Writing heapster specifications for your functions](#4-writing-heapster-specifications-for-your-functions) +- [5. Writing a SAW script to type-check your code with respect to the sepcification](#5-writing-a-saw-script-to-type-check-your-code-with-respect-to-the-sepcification) +- [6. Writing a Coq file to prove things about the generated functional specification(s)](#6-writing-a-coq-file-to-prove-things-about-the-generated-functional-specifications) Just like with SAW, Heapster can be processed in batch. To do so, you can combine steps 2-6 in a `.saw` file and use SAW's batch processing. @@ -358,9 +358,9 @@ you can generate it just like before. Note that we have already included the binary for all the examples so you don't really need to run this command. - ```bash - clang -g -c -emit-llvm -o ffs.bc ffs.c - ``` +```bash +clang -g -c -emit-llvm -o ffs.bc ffs.c +``` (The alternative command `make examples/linked_list.bc` won't work because the shorcut is not defined in the Makefile of heapster.) @@ -375,9 +375,9 @@ bitcode is generated. If you find an incompatibility, please report it. We start by running saw with `cabal run saw`. Once SAW is loaded, you can load all the Heapster commands with - ```bash - sawscript> enable_experimental - ``` +```bash +sawscript> enable_experimental +``` If you print the environment now (wiht `:env`) you will notice a new set of commands, all starting with `heapster_*`. You can also start @@ -525,8 +525,12 @@ The first argument is the Heapster environment, the second is its name, the third is its arguments (of which there are none), the fourth is the type of value that the permission applies to, and the fifth is its definition. the new permission is created and added to the -environment. **TODO: Can I print the new permission? `print env` does -not show new permission definintions.** +environment. + +Unfortunately, there is currently no way to print the newly defined +permissions. If you try to print the environment (`print env`) at this +point, you will only see the `llvm` definitions. We might add +functionality for showing permissions in the future. The permission predicate for lists is a little more complicated because it requires a recursive definition. To define From 70bae32847e0b8e264a76b462071ebabb24e8685 Mon Sep 17 00:00:00 2001 From: santiago Date: Wed, 24 Aug 2022 15:26:13 -0400 Subject: [PATCH 07/23] typo --- heapster-saw/doc/tutorial/tutorial.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/heapster-saw/doc/tutorial/tutorial.md b/heapster-saw/doc/tutorial/tutorial.md index 65fa250c06..216c8ea7c4 100644 --- a/heapster-saw/doc/tutorial/tutorial.md +++ b/heapster-saw/doc/tutorial/tutorial.md @@ -205,7 +205,9 @@ logo and version number. Then you cna run your first saw command: environment. Finally you can allways type `:help` to remember these commands. - So, run `l <- llvm_load_module "ffs.bc"` to load the file and stored in variable `l`. If you print the environment with `:env` you will now see a new variable `l : LLVMModule`. + Run `l <- llvm_load_module "ffs.bc"` to load the file and store it + in the variable `l`. If you print the environment with `:env` you + will now see a new variable `l : LLVMModule`. Now from `l`, we want to extract the two functions From 9df3090980303c171535c21b1e3e3b2a8e660556 Mon Sep 17 00:00:00 2001 From: santiago Date: Wed, 24 Aug 2022 15:27:11 -0400 Subject: [PATCH 08/23] typo --- heapster-saw/doc/tutorial/tutorial.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/heapster-saw/doc/tutorial/tutorial.md b/heapster-saw/doc/tutorial/tutorial.md index 216c8ea7c4..627c48919d 100644 --- a/heapster-saw/doc/tutorial/tutorial.md +++ b/heapster-saw/doc/tutorial/tutorial.md @@ -190,7 +190,7 @@ logo and version number. Then you cna run your first saw command: #### 3. Load the file and extract the two function specifications. To load the file, we will use `llvm_load_module`. We can check what the function does with - ``` bash + ``` sawscript> :? llvm_load_module Description ----------- From 097932f3ce9d44b3fde278c86cd1c6a45d45a9d7 Mon Sep 17 00:00:00 2001 From: santiago Date: Wed, 24 Aug 2022 15:28:20 -0400 Subject: [PATCH 09/23] wrong file name --- heapster-saw/doc/tutorial/tutorial.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/heapster-saw/doc/tutorial/tutorial.md b/heapster-saw/doc/tutorial/tutorial.md index 627c48919d..9eddc67ca7 100644 --- a/heapster-saw/doc/tutorial/tutorial.md +++ b/heapster-saw/doc/tutorial/tutorial.md @@ -361,7 +361,7 @@ included the binary for all the examples so you don't really need to run this command. ```bash -clang -g -c -emit-llvm -o ffs.bc ffs.c +clang -g -c -emit-llvm -o examples/linked_list.bc examples/linked_list.c ``` (The alternative command `make examples/linked_list.bc` won't work From 5c65e2b2f3bd4f46433de7e20a95e92efc7bfd43 Mon Sep 17 00:00:00 2001 From: santiago Date: Mon, 29 Aug 2022 11:35:47 -0400 Subject: [PATCH 10/23] Start intergrating Eddy's comments. --- heapster-saw/doc/tutorial/tutorial.md | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/heapster-saw/doc/tutorial/tutorial.md b/heapster-saw/doc/tutorial/tutorial.md index 9eddc67ca7..2570a9ecca 100644 --- a/heapster-saw/doc/tutorial/tutorial.md +++ b/heapster-saw/doc/tutorial/tutorial.md @@ -32,7 +32,7 @@ We'll start by building everything you need to use Heapster. All the commands here are with respect to the top-level saw-script directory. ### Build Saw - + You will need to follow the instructions in the top-level README to download or build a SAW binary, of which Heapster is a part. In particular, make sure you follow the instructions to install Z3. Once `./build.sh` @@ -62,7 +62,7 @@ sawscript> :quit In this tutorial we will also interact with Heapster's Coq output. So you'll need to follow the instructions in the README in the `saw-core-coq` subdirectory. Specifically, after installing the dependencies, you will need to run the -following (from this directory): +following (from the top level directory): ```bash cd /saw-core-coq/coq make @@ -73,7 +73,7 @@ build should complete without any errors. **TODO: How do we check if this is properly installed before continuing?** -Before continuing, return to the top-level directory with `cd ..`. +Before continuing, return to the top-level directory with `cd ../..`. ### Build all the examples @@ -85,7 +85,9 @@ and build, like so cd /heapster-saw/examples make ``` + You will see several files build that looks like this: + ```bash COQC global_var_gen.v COQC global_var_proofs.v @@ -95,6 +97,8 @@ COQC sha512_gen.v It will take several minutes and it should complete without any errors. Once it's done, you know you are ready to use Heapser! +Before continuing, return to the top-level directory with `cd ../..`. + ## A quick tour of SAW You don't need to be an expert in SAW to handle Heapster, but a little @@ -311,6 +315,14 @@ extracted as a functional program to be verified in Coq. **TODO: Double check this description of Heapster** +This section assumes you are in the `/heapster-saw/examples` +directory. If you are not, make sure to go there + +```bash +cd /heapster-saw/examples +make +``` + ### Heapster type-checking overview Heapster allows us to (1) type check programs with respect to From 1d49b86d26f95e8709c0843146885bb12706839e Mon Sep 17 00:00:00 2001 From: santiago Date: Mon, 29 Aug 2022 13:21:06 -0400 Subject: [PATCH 11/23] More integrating Eddy's comments. --- heapster-saw/doc/tutorial/tutorial.md | 38 ++++++++++++++++++++------- 1 file changed, 28 insertions(+), 10 deletions(-) diff --git a/heapster-saw/doc/tutorial/tutorial.md b/heapster-saw/doc/tutorial/tutorial.md index 2570a9ecca..c4d4aea34e 100644 --- a/heapster-saw/doc/tutorial/tutorial.md +++ b/heapster-saw/doc/tutorial/tutorial.md @@ -63,8 +63,9 @@ In this tutorial we will also interact with Heapster's Coq output. So you'll nee to follow the instructions in the README in the `saw-core-coq` subdirectory. Specifically, after installing the dependencies, you will need to run the following (from the top level directory): + ```bash -cd /saw-core-coq/coq +cd saw-core-coq/coq make ``` @@ -86,7 +87,22 @@ cd /heapster-saw/examples make ``` -You will see several files build that looks like this: +If this is the first time you run make in this folder, you will see `cabal run saw` called multiple times like so + +``` +/Path/To/Saw/ +[16:59:41.084] Loading file "/Path/To/Saw/saw-script/heapster-saw/examples/linked_list.saw" +cabal run saw xor_swap.saw +Up to date + + + +[16:59:42.974] Loading file "/Path/To/Saw/saw-script/heapster-saw/examples/xor_swap.saw" +cabal run saw xor_swap_rust.saw +Up to date +``` + +Eventually it should start making the coq files ```bash COQC global_var_gen.v @@ -94,7 +110,7 @@ COQC global_var_proofs.v COQC sha512_gen.v ``` -It will take several minutes and it should complete without any +It might take several minutes but it should complete without any errors. Once it's done, you know you are ready to use Heapser! Before continuing, return to the top-level directory with `cd ../..`. @@ -344,9 +360,11 @@ can combine steps 2-6 in a `.saw` file and use SAW's batch processing. ### Running an example This section will walk through the process of using Heapster to write -and verify some C code. Specifially, we want to verify the function +and verify some C code. + +Specifially, we want to verify the function `is_elem`, which tests if a specific value is in a list. The function, -together with others, can be found in `examples/linked_list.c`. +together with others, can be found in `linked_list.c`. ```C typedef struct list64_t { @@ -373,10 +391,10 @@ included the binary for all the examples so you don't really need to run this command. ```bash -clang -g -c -emit-llvm -o examples/linked_list.bc examples/linked_list.c +clang -g -c -emit-llvm -o linked_list.bc linked_list.c ``` -(The alternative command `make examples/linked_list.bc` won't work +(The alternative command `make linked_list.bc` won't work because the shorcut is not defined in the Makefile of heapster.) Be aware that the resulting bitcode may depend on your `clang` version and your @@ -455,14 +473,14 @@ that can be printed wiht `:env`). Let's load our module with ``` -env <- heapster_init_env "linked_list" "examples/linked_list.bc"; +env <- heapster_init_env "linked_list" "linked_list.bc"; ``` we have created a new Heapster environment that we can explore. ``` sawscript> print env -[20:19:48.436] Module: examples/linked_list.bc +[20:19:48.436] Module: linked_list.bc Types: %struct.list64_t = type { i64, %struct.list64_t* } @@ -612,7 +630,7 @@ the `heapster_typecheck_fun` command to succeed. In the case of functions with loops, this hint corresponds to a loop invariant. Additionally, such examples will also often require your unbounded data structure to be defined as a reachability permission, using `heapster_define_reachability_perm`, instead of -just as a recursive permission. See `examples/iter_linked_list.saw` for some +just as a recursive permission. See `iter_linked_list.saw` for some examples of using the commands mentioned in this paragraph. Once you're finished, use the following command to export all the type-checked From f81457b8c491a873fd04e1162e1e443f91189dbb Mon Sep 17 00:00:00 2001 From: santiago Date: Mon, 29 Aug 2022 14:58:36 -0400 Subject: [PATCH 12/23] More editing after Eddy's comments. --- heapster-saw/doc/tutorial/tutorial.md | 114 ++++++++++++++++---------- 1 file changed, 71 insertions(+), 43 deletions(-) diff --git a/heapster-saw/doc/tutorial/tutorial.md b/heapster-saw/doc/tutorial/tutorial.md index c4d4aea34e..4d0c3801c7 100644 --- a/heapster-saw/doc/tutorial/tutorial.md +++ b/heapster-saw/doc/tutorial/tutorial.md @@ -342,15 +342,15 @@ make ### Heapster type-checking overview Heapster allows us to (1) type check programs with respect to -types/specifications that can express separation loigc and (2) extract +types that can express separation loigc and (2) extract the resulting functional program to Coq for further verification. The process will generally involve - [1. Generating LLVM bitcode](#1-generating-llvm-bitcode) - [2. Run the SAW interpreter with Heapster](#2-run-the-saw-interpreter-with-heapster) -- [3. Load the file and extract the two function specifications.](#3-load-the-file-and-extract-the-two-function-specifications-1) -- [4. Writing heapster specifications for your functions](#4-writing-heapster-specifications-for-your-functions) +- [3. Load the file and extract the two function types.](#3-load-the-file-and-extract-the-two-function-types-1) +- [4. Writing heapster types for your functions](#4-writing-heapster-types-for-your-functions) - [5. Writing a SAW script to type-check your code with respect to the sepcification](#5-writing-a-saw-script-to-type-check-your-code-with-respect-to-the-sepcification) - [6. Writing a Coq file to prove things about the generated functional specification(s)](#6-writing-a-coq-file-to-prove-things-about-the-generated-functional-specifications) @@ -394,8 +394,12 @@ run this command. clang -g -c -emit-llvm -o linked_list.bc linked_list.c ``` -(The alternative command `make linked_list.bc` won't work -because the shorcut is not defined in the Makefile of heapster.) +Alternatively, as long as you are in the `heapster-saw/examples` directory, you can also run + +```bash +make linked_list.bc +``` + Be aware that the resulting bitcode may depend on your `clang` version and your operating system. In turn, this means the Heapster commands in your SAW script @@ -411,7 +415,7 @@ can load all the Heapster commands with sawscript> enable_experimental ``` -If you print the environment now (wiht `:env`) you will notice a new +If you print the environment now (with `:env`) you will notice a new set of commands, all starting with `heapster_*`. You can also start typing the name and press tab to see all the functions those are all the Heapster commands. @@ -441,39 +445,42 @@ heapster_find_symbol_with_type heapster_typecheck_mut_funs You can then use `:?` to see further information for each of them. -#### 3. Load the file and extract the two function specifications. +#### 3. Load the file and extract the two function types. -To load a file into heapster you can use `heapster_init_env`. Let's -check it's documentation first +To load a file into heapster you can use `heapster_init_env_from_file`. Let's +check its documentation first ``` bash -sawscript> :help heapster_init_env +sawscript> :? heapster_init_env_from_file Description ----------- EXPERIMENTAL -heapster_init_env : String -> String -> TopLevel HeapsterEnv + heapster_init_env_from_file : String -> String -> TopLevel HeapsterEnv -Create a new Heapster environment with the given SAW module name -from the named LLVM bitcode file. +Create a new Heapster environment from the named LLVM bitcode file, + initialized with the module in the given SAW core file. ``` -As you see it takes two names. The first, is the name of the SAW core -module where Heapster will write all the specifications we extract. If -you start with a fresh name, Heapster will autogenerate a new module -for you. We will see later how to use existisng modules. The second -name referse to the bitecode file containing the code we are -verifying. +As you see it takes two names. The second name referse to the bitecode +file containing the code we are verifying. The first, is the name of +the SAW core module that can contain extra definitions and where +Heapster will store the new definitions you provide. The function returns a Heapster environment that contains all the definitions of the module (not to be confused with the SAW environment that can be printed wiht `:env`). +Alternatively, if you don't have any extra SAW core definitions, you +can use `heapster_init_env` which does the same as +`heapster_init_env_from_file`, except it will create a fresh SAW core +module for you with the given name. + Let's load our module with ``` -env <- heapster_init_env "linked_list" "linked_list.bc"; +env <- heapster_init_env_from_file "linked_list.sawcore" "linked_list.bc"; ``` we have created a new Heapster environment that we can explore. @@ -505,12 +512,12 @@ The heapster environment contains all the types, global definitions, external references and functions from the loaded module. -#### 4. Writing heapster specifications for your functions +#### 4. Writing heapster types for your functions -##### Pen and paper specification +##### Pen and paper type Before we go foward using Heapster, let's think about what the -specification for `is_elem` should be. As we can check in the +type for `is_elem` should be. As we can check in the environment `env`, `is_elem` takes a 64-bit integer the "element". ```LLVM @@ -529,18 +536,18 @@ the inputs after the call we can simplify it to `arg0:true, arg1: true, ret:int64`, where `true` is a predicate the is always satisfied. Then, using the linear implication `-o` we can express the -specification of `is_elem` as +type of `is_elem` as ``` arg0:int64, arg1: list int64 -o arg0:true, arg1:true, ret:int64 ``` -Notice that this is a memory-safety specification, not a correctness +Notice that this is a memory-safety type, not a correctness predicate. We can reason about the correctness of the function once we extract it as a functional program in Coq. In the next sections, we shall define the predicates necessary to -write this specification in Heapster. +write this type in Heapster. ##### Defining permission predicates @@ -556,18 +563,39 @@ heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x) The first argument is the Heapster environment, the second is its name, the third is its arguments (of which there are none), the fourth is the type of value that the permission applies to, and the fifth is -its definition. the new permission is created and added to the -environment. +its permision type. The new permission is created and added to the +environment. + +Uses of this named permission are written `int64<>` where the `<>` is +the empty list of arguments. Unfortunately, there is currently no way to print the newly defined permissions. If you try to print the environment (`print env`) at this point, you will only see the `llvm` definitions. We might add functionality for showing permissions in the future. -The permission predicate for lists is a little more complicated -because it requires a recursive definition. To define -[permissions](doc/Permissions.md) which can describe unbounded data -structures, you can use the `heapster_define_recursive_perm` +Before we look at the definition of a `List64` lets focus on its +permission type. First of all, `List64` takes a single argumetn +`rw` which determines if the list is readable or writable. It's type +should look something like this + +``` +["eq(llvmword(0))", "ptr((rw,0) |-> int64<>) * ptr((rw,8) |-> List64)"] +``` + +the definition shows the diferent cases for a list, separated by a +coma. In the first case, a `List64` is can be a null pointer, +expressed with the type `eq(llvmword(0))`. In the second case, a list +is a pointer where offset 0 is the head, an `Int64`, and offset `8` +it's the tail, another `List64`, i.e., it is recursively a +`List64` . In the later case, both elements are tagged with `rw`, +describing if they are readable or writable, as determined by the +argument to `List64`. + +You might have noticed that the permission predicate for lists is +recursive, since it must refer to it's tail which is itself a list. To +define [permissions](doc/Permissions.md) which can describe unbounded +data structures, you can use the `heapster_define_recursive_perm` command. As an example, here is how to describe a linked list of 64-bit words using this command: @@ -584,14 +612,12 @@ heapster_define_recursive_perm ``` Its first four arguments are the same as for `heapster_define_perm`, -its fifth argument contains its different inductive cases (in this -case, a `List64` is either a null pointer, or a pointer to an `Int64` -and another `List64`), and its final three arguments are its -translation into SAW core. Here the SAW core definitions used are from -the SAW core prelude which are included by default when Heapster -autogenerates a a module for you. If you need new SAW core -definitions, you will need to use the following command instead of -`heapster_init_env`: +its fifth argument contains its different inductive cases which we +describe below, and its final three arguments are its translation into +SAW core. Here the SAW core definitions used are from the SAW core +prelude which are included by default when Heapster autogenerates a a +module for you. If you need new SAW core definitions, you will need to +use the following command instead of `heapster_init_env`: ``` env <- heapster_init_env_from_file "my_file.sawcore" "my_file.bc"; @@ -605,9 +631,11 @@ reference on the syntax and meaning of heapster permissions. We begin by converting the pen-and-paper specification of `is_elem` into a Heapster specification. First, every heapster type begins with the declaration of a ghost environment. Our specification doesn't use -any ghost variable so that is `().` Moreover, for every predicate we -use, we must specify whether the location is readble-only `` or -both readable and writable `<>`. Whith this we can write our specification as +any ghost variable so that is `().` Moreover, every named definition +takes it's arguments within angled braces ``. For `int64`, which +takes no arguments that is just `<>`, and for `List` which takes a an +arguments to define that it is a readable list, it is ``. Whith +this we can write our specification as ``` ().arg0:int64<>, arg1:List64 -o arg0:true, arg1:true, From 430036b9ae1eba0ae6e83abac8749ef8b796db98 Mon Sep 17 00:00:00 2001 From: santiago Date: Tue, 30 Aug 2022 11:59:40 -0400 Subject: [PATCH 13/23] Adding more details to tutorial and major cleanup --- heapster-saw/examples/tutorial_c.bc | Bin 0 -> 4336 bytes heapster-saw/examples/tutorial_c.c | 17 ++++++++++++++++ heapster-saw/examples/tutorial_c.v | 29 ++++++++++++++++++++++++++++ 3 files changed, 46 insertions(+) create mode 100644 heapster-saw/examples/tutorial_c.bc create mode 100644 heapster-saw/examples/tutorial_c.c create mode 100644 heapster-saw/examples/tutorial_c.v diff --git a/heapster-saw/examples/tutorial_c.bc b/heapster-saw/examples/tutorial_c.bc new file mode 100644 index 0000000000000000000000000000000000000000..116253b968778d6ce25c8170980a18754a82764f GIT binary patch literal 4336 zcmcIoeN0=|6~B*X{7f*mNl0VDv-2F%)oloV*o2rGR2!3)v~)E|)-tUTei##I_;}b3 zUuoB8?CjA7RZg3Atj#2QrBT{$6H)U=D&-G@38Rq{5t?>UhElT-N;8_WHQO?^T6V6D zX*yN=W74j;*XNyc?|J8UzTOqrq8qXij69gLDugJ6h$?&Z+IC<7jT+_bme*fD@%BId z@Zt*}oqp=;?k_*R{Zw|HP)i`BlOr@mB9xt>Lm9C5KA4oh@ThG{vP-HmmcL2_<@aaG z^0ks9jY8hejH*|&t437DJhM#w#2Vx7!5V%-S6IDP98%d{&1jmEoyueEj}9^)62{#@ z^+WoHLM6|SK6{ioHwAiMVh~ynzsAiqSxnPm$!nWOg0NfB^bBy7BpEf^7Mv$}oYf@5-FHZx*6J9`9=b7^qH-&?)#W zn0VmMT^Iz9vh<{t9CtDz9}*AMP(3YyzOZ;uP5J7@vSF$}B=+#4w}tEmQ9UIvqHkE_ zRaCcLEDMW#4b|Ne=#o+0PO%Tgb@UZZd!At8Htl#sb3T%jnA6ORX%-{&Jc0L6f>ZPi zi+wF*Z%Fj0u_{js=@rCo8Rhx*_*I=|Hj;BCLSF=hk({LnJ?Yn8vuUp;v@?EskK<&kIyvFV(LXyTW2m zNGwx{{Ve6xQ+*Jf8tMf-g_LMOJ8sinjL?gboJm4^lMqA?PxVbvJxJCM3eBP?ES9k% zDDOW>_30r%pE&7donlGI!33ea;siLG7HnD|u0}M=e&B1z2~9jnEJSGFFF-(TiWP!O z6Mn@kvqHnR1yG1KEhiLU(# zM(Hba*u$&ADl?DcTvZC2(2J-BWnLzxalP(>T*kGyZopZ^;9ukOQPOfJ(-IDp$*5i- znWK;vYO!aSdVY{B=SegCU2(3tF)jTfOno^mU1q>r6u8zCro0T*j+EfSt|X0_sSOO( z@1%TTs@qDnhZL~l$7$(;KtaZJF;wrg^p-&NLrtU(CZ+GID33sG)X6`ry*ytn8~tX$ zAb&^DA%rbW4Yi>A7_GM=S(<@JcI1s=goIUw6a8%OrU8VYTdfRvG;~vbpY%I>wv@^8 z+*)W*83fj4)DElib8ACGSwDDeQeyY)w00Kxv!;G-*B!HEf&3Ks?HBNCk_q(09NnBp zR1VtB!Prn$GU>d-UGfE_{6eL;EhtR#D((1~2C}S~%}j0!6vWBODSPD*SsCvgf}A}B zxmE*}MD_Dzcdy7ZVtzbVu@q9wvC0lsd3{;2>`<6g6PjyK%{t9Er)_3mvYZWArtRgY z$%?aqiXdr;FXusfIMhPzXn`D|b_lo|@lFUK)qN)u)bQKyw6xXfFIYzMrC>XtFb_|!@jE+?CGU?hwEx@hm_a@+UKom)p zbnoGSIUci&+AF~!-;7tx+bx6e7#ljbM(i6Fd%zy3U_Ip-_CI@FrC5q8Za5TQv4vwZ zHs~uGpjNJd0X6xS(Lm+tKtV8O9E60yJwZNE_+Zv+RA(al@kf}aA=CF%Kfyfh_IO)6JF0s)PxI=7 zyYb+DW>-gZXPVRFYT-N$-qwD%W0#$&b$7elds1{!By-s{KyMx412f^Un{r2 z)8O!QKIeA%yaq4Vv(4-BwDLYfi<{%UKDTEZ@C@!=uAOgldu=?djH`|7*w1vQEMZDa z#cVOl=#$)SB_9p?C`ek?{GIUu&1{Vp+eaYO9qzJg|dq!0|^G6i~|Y1 z{l`QMx*oFOj*SQgy=07`%uDjXmRgg1+IoTAJ5d^A)=yhAoit)e)-K5RBDkh~MWg)E zFruT?InI(#DFI(zP@E0g)WNaZAQ~jtea@*G=YX-%_5J~G>!HH;TwA>*u58Pj1#gcQ z7k%X6FkiRM;>~}r;Qo`llaIR!w|d_yxPK9$cc2H-pfP)mM-RP)>aXXAA)jMV#pTnn zfdzUJZVhmY8N+Fxs@eNWuR9f=IiM9N=W#<&e&$fz9u@rf(~3J)uLxC!>$ILf9y6aN zEF*!+W3d5Ji}ggb_}YTdCCG2MwIM2AF%qyGhh{`ph65GQm_jiOkz){CZs1!cu~op8 zGuikzKQQ1nbS8xRY}tw_ik zzf`MIV6U5Ug||ZEwUUH>gl)6RB*c)KMzR6h+;RL>4gCui@@xEkHAyr5za)^nKs9DX zg;EL)I34B%kUSEGD9tJ9nb1l#*oDvD%1UMVoTfI07n^Jf!lZo%*)vV&RjQ_8A z&*e&+5sFExSygm!j1U-g-YfqEl*&a|9vOw@F5sZs0f#k%F-gxIrC|RSWCZ35z~rkC zFi&A-0U#GKa>)eP|9yB(zz4iV_+yS^EqNTFzp%gqdIdWv0~%`3)4=;YDcpNztVBA_ zbz}v|IkX1WsFW}Vo(!Te!4~JnqjSehGUOaU+i|=_i1#RwE0?g1JYrvIQ(?s;w($TnZKq$phVQ0=V{QQQ{%>ktO^lu-Hi`#k7`YX@w*E4@5Zm6W zl7^80W*^xYE+>DtE5M>m2p+n^o+apsu`|^UvNW-|4Es%$^xKjD^xONmF32xoQKtP? zr#?v_$0($H?g##j$oh<(m7AnH^Qh;NPUMj46qbFQk~!5N3$DuOTr9f)GNd~KLCD<% z%6!`;YfLUj^^0L}1i`G6qHS1qNuQEkz_Jr*Sv1!VvN|lI*G56v=UAByA2|9@>cH+Y zIPlx_0rVu6)fJ^=>vw?cbXt~Dc4_OXvdF+jNGve9NeXa?l9fDWaiFHlm2N<~T zL1RI6FhLE%eFKlQ9MgC|9{XTQl2mFRMCdLKEeE_@nE0#;Cg#hE;2r`r27zl0>rU@~ z5omlT-UJiZUYb7$G~V|BO#DxSG#^N`4+J>-0Ane}1HG!Pt-HOrsd0aClN;^_9{0WN zD_zd_ltAh((Q7ViC@b9tH-$F$wsy|d>Fq5s;!DQ8cbEpO>Oa*dnd$b}kbXhKJ#WBv F{u{eXcA@|P literal 0 HcmV?d00001 diff --git a/heapster-saw/examples/tutorial_c.c b/heapster-saw/examples/tutorial_c.c new file mode 100644 index 0000000000..8d736f0c8d --- /dev/null +++ b/heapster-saw/examples/tutorial_c.c @@ -0,0 +1,17 @@ +#include + +// Simple function that adds it's two inputs. +uint64_t add (uint64_t x, uint64_t y) { return x + y; } + +// A copy of `add`, that we will use to miss-type a function +uint64_t add_mistyped (uint64_t x, uint64_t y) { return x + y; } + +// Simple function that increments the value in a pointer +void incr_ptr (uint64_t *x) { *x += 1; } + +// Struct that represents the three coordinates fora 3D vector +typedef struct { uint64_t x; uint64_t y; uint64_t z; } vector3d; + +// function that computes the norm of a 3D vector +// || (x,y,z) || = x^2+y^2+z^2 +uint64_t norm_vector (vector3d *v) { return (v->x * v->x + v->y * v->y + v->z * v->z); } diff --git a/heapster-saw/examples/tutorial_c.v b/heapster-saw/examples/tutorial_c.v new file mode 100644 index 0000000000..c854be4cf3 --- /dev/null +++ b/heapster-saw/examples/tutorial_c.v @@ -0,0 +1,29 @@ + +(** Mandatory imports from saw-core-coq *) +From Coq Require Import Lists.List. +From Coq Require Import String. +From Coq Require Import Vectors.Vector. +From CryptolToCoq Require Import SAWCoreScaffolding. +From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors. +Import ListNotations. + +(** Post-preamble section specified by you *) +From CryptolToCoq Require Import SAWCorePrelude. +From CryptolToCoq Require Import SAWCoreBitvectors. + +(** Code generated by saw-core-coq *) + +Module tutorial_c. + +Definition add__tuple_fun : CompM.lrtTupleType (CompM.LRT_Cons (CompM.LRT_Fun (SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) (fun (perm0 : SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) => let var__0 := SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool in + CompM.LRT_Fun var__0 (fun (perm1 : var__0) => CompM.LRT_Ret (SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool)))) CompM.LRT_Nil) := + @CompM.multiFixM (CompM.LRT_Cons (CompM.LRT_Fun (SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) (fun (perm0 : SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) => let var__0 := SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool in + CompM.LRT_Fun var__0 (fun (perm1 : var__0) => CompM.LRT_Ret (SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool)))) CompM.LRT_Nil) (fun (add : CompM.lrtToType (CompM.LRT_Fun (SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) (fun (perm0 : SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) => let var__0 := SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool in + CompM.LRT_Fun var__0 (fun (perm1 : var__0) => CompM.LRT_Ret (SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool))))) => pair (fun (p0 : SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) (p1 : SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) => let var__0 := SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool in + @CompM.letRecM CompM.LRT_Nil var__0 tt (@returnM CompM _ var__0 (SAWCoreVectorsAsCoqVectors.bvAdd 64 p0 p1))) tt). + +Definition add : CompM.lrtToType (CompM.LRT_Fun (SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) (fun (perm0 : SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) => let var__0 := SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool in + CompM.LRT_Fun var__0 (fun (perm1 : var__0) => CompM.LRT_Ret (SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool)))) := + SAWCoreScaffolding.fst add__tuple_fun. + +End tutorial_c. From 1c5fcfa9ad3778012dc7860f4383ef1e63bd7151 Mon Sep 17 00:00:00 2001 From: santiago Date: Tue, 30 Aug 2022 12:02:22 -0400 Subject: [PATCH 14/23] tutorial TOC --- heapster-saw/doc/tutorial/tutorial.md | 492 +++++++++++++++++++++----- 1 file changed, 410 insertions(+), 82 deletions(-) diff --git a/heapster-saw/doc/tutorial/tutorial.md b/heapster-saw/doc/tutorial/tutorial.md index 4d0c3801c7..fa34f1cdf8 100644 --- a/heapster-saw/doc/tutorial/tutorial.md +++ b/heapster-saw/doc/tutorial/tutorial.md @@ -17,7 +17,10 @@ examples to get anyone up to speed with using and hacking on Heapster. - [Batch scripts](#batch-scripts) - [Using Heapster](#using-heapster) - [Heapster type-checking overview](#heapster-type-checking-overview) - - [Running an example](#running-an-example-1) + - [First example](#first-example) + - [Pointers](#pointers) + - [Structs](#structs) + - [Recursive data structures](#recursive-data-structures) - [Looking under the hood](#looking-under-the-hood) - [Heapster commands and environments](#heapster-commands-and-environments) - [Permissions](#permissions) @@ -74,6 +77,11 @@ build should complete without any errors. **TODO: How do we check if this is properly installed before continuing?** +For the sake of this tutorial, it will also be useful to install a +[user interface](https://coq.inria.fr/user-interfaces.html) to +interact with extracted Coq code. I recomment installing [Proof +General](https://proofgeneral.github.io/). + Before continuing, return to the top-level directory with `cd ../..`. ### Build all the examples @@ -132,7 +140,7 @@ complex software artifacts. In this tutorial we will overview how to use SAW to proof functional equality different implementations. The steps are as follows: -- [1. Compile the code down to llvm bitecode (i.e. `.bc` files).](#1-compile-the-code) +- [1. Compile the code.](#1-compile-the-code) - [2. Run the saw interpreter](#2-run-the-saw-interpreter) - [3. Load the file and extract the two function specifications.](#3-load-the-file-and-extract-the-two-function-specifications) - [4. Define the equality theorem.](#4-define-the-equality-theorem) @@ -351,60 +359,48 @@ The process will generally involve - [2. Run the SAW interpreter with Heapster](#2-run-the-saw-interpreter-with-heapster) - [3. Load the file and extract the two function types.](#3-load-the-file-and-extract-the-two-function-types-1) - [4. Writing heapster types for your functions](#4-writing-heapster-types-for-your-functions) -- [5. Writing a SAW script to type-check your code with respect to the sepcification](#5-writing-a-saw-script-to-type-check-your-code-with-respect-to-the-sepcification) +- [5. Type-check your program](#5-writing-a-saw-script-to-type-check-your-code-with-respect-to-the-sepcification) - [6. Writing a Coq file to prove things about the generated functional specification(s)](#6-writing-a-coq-file-to-prove-things-about-the-generated-functional-specifications) Just like with SAW, Heapster can be processed in batch. To do so, you can combine steps 2-6 in a `.saw` file and use SAW's batch processing. -### Running an example - -This section will walk through the process of using Heapster to write -and verify some C code. +### First example -Specifially, we want to verify the function -`is_elem`, which tests if a specific value is in a list. The function, -together with others, can be found in `linked_list.c`. +This section will walk through the process of using Heapster to write, +typecheck and verify some C code. We will start by type-checking the +simple `add` function, wich you can find in `tutorial_c.c` in the +examples directory. ```C -typedef struct list64_t { - int64_t data; - struct list64_t *next; -} list64_t; - -int64_t is_elem (int64_t x, list64_t *l) { - if (l == NULL) { - return 0; - } else if (l->data == x) { - return 1; - } else { - return is_elem (x, l->next); - } -} +uint64_t add (uint64_t x, uint64_t y) { return x + y; } ``` +We will type-check the rest of the function in that file, plus some +recursive functions later in the tutorial. + + #### 1. Generating LLVM bitcode -Just like with SAW, we want to work with the LLVM bitcode (`.bc`), so -you can generate it just like before. Note that we have already -included the binary for all the examples so you don't really need to -run this command. +Just like with SAW, we want to work with the LLVM bitcode +(`.bc`). ```bash -clang -g -c -emit-llvm -o linked_list.bc linked_list.c +clang -g -c -emit-llvm -o tutorial_c.bc tutorial_c.c ``` Alternatively, as long as you are in the `heapster-saw/examples` directory, you can also run ```bash -make linked_list.bc +make tutorial_c.bc ``` - -Be aware that the resulting bitcode may depend on your `clang` version and your -operating system. In turn, this means the Heapster commands in your SAW script -and the proofs in your Coq file may also be dependent on how and where the -bitcode is generated. If you find an incompatibility, please report it. +Be aware that the resulting bitcode may depend on your `clang` version +and your operating system. In turn, this means the Heapster commands +in your SAW script and the proofs in your Coq file may also be +dependent on how and where the bitcode is generated. If you find an +incompatibility, please report it. For all other examples, the binary +code has been provided already to avoid incompatibilities. #### 2. Run the SAW interpreter with Heapster @@ -417,7 +413,8 @@ sawscript> enable_experimental If you print the environment now (with `:env`) you will notice a new set of commands, all starting with `heapster_*`. You can also start -typing the name and press tab to see all the functions those are all the Heapster commands. +typing the name and press tab to see all the functions. These are all +the Heapster commands. ``` sawscript> heapster_ [TAB] @@ -444,46 +441,393 @@ heapster_find_symbol_with_type heapster_typecheck_mut_funs You can then use `:?` to see further information for each of them. +#### 3. Load the file. -#### 3. Load the file and extract the two function types. - -To load a file into heapster you can use `heapster_init_env_from_file`. Let's +To load a file into heapster you can use `heapster_init_env`. Let's check its documentation first -``` bash -sawscript> :? heapster_init_env_from_file +``` +sawscript> :? heapster_init_env Description ----------- EXPERIMENTAL - heapster_init_env_from_file : String -> String -> TopLevel HeapsterEnv + heapster_init_env : String -> String -> TopLevel HeapsterEnv -Create a new Heapster environment from the named LLVM bitcode file, - initialized with the module in the given SAW core file. +Create a new Heapster environment with the given SAW module name + from the named LLVM bitcode file. +sawscript> ``` As you see it takes two names. The second name referse to the bitecode -file containing the code we are verifying. The first, is the name of -the SAW core module that can contain extra definitions and where -Heapster will store the new definitions you provide. +file containing the code we are verifying. The first, is the name we +want to give our SAW core module. That is the place where Heapster +will store all our type checked functions and their extracted +functional specification. By convention we use the same name as the +llvm file. The function returns a Heapster environment that contains all the definitions of the module (not to be confused with the SAW environment that can be printed wiht `:env`). -Alternatively, if you don't have any extra SAW core definitions, you -can use `heapster_init_env` which does the same as -`heapster_init_env_from_file`, except it will create a fresh SAW core -module for you with the given name. +``` +env <- heapster_init_env "tutorial_c" "tutorial_c.bc" +``` + +we have created a new Heapster environment that we can explore. + +``` +sawscript> env +[20:07:14.272] Module: tutorial_c.bc +Types: + %struct.vector3d = type { i64, i64, i64 } + +Globals: + +External references: + declare default void @llvm.dbg.declare(metadata, metadata, + metadata) + +Definitions: + i64 @add(i64 %0, i64 %1) + i64 @add_mistyped(i64 %0, i64 %1) + void @incr_ptr(i64* %0) + i64 @norm_vector(%struct.vector3d* %0) +``` + +The heapster environment contains all the types, global definitions, +external references and functions from the loaded module. In our first +example we will focus on the `add` function. + + +#### 4. Writing heapster types for your functions + +The Heapster type for the `add` function is rather simpl: + +``` +"().arg0:int64<>, arg1:int64<> -o arg0:true, arg1:true, ret:int64<>" +``` + +It starts with an empty parenthesis `().` that contains the local +ghost environment. Since this function doesn't require ghost +variables, it is empty. + +The rest of the type is composed of two parts separated by the linear +implication operator `-o`, sometimes known as lollipop. The left hand +side of the operator, refers to the state of memory before the +function executes. And it says that the two arguments passed to `add`, +`arg0` and `arg1`, are 64-bit integers. The predicate `int64`, which +we will define in a moment, takes no arguments as represented by the +empty angled brackets `<>`. + +The right hand side describes the memory after the function +executes. It says nothing about about the arguments (other than they +exists), with `true`, the predicate that is always satisfied. It also +says that the return value `ret` is another 64-bit integer. + +Notice, in particular, that the type does not assert that the return +value is the sum of the inputs. That's because Hepaster is not a +correcness logic. It is a memory safety type system. However, as you +will shortly see, after checking for memory safety, we can extract +`add` as a functional program and verify it's correctness in Coq. + +##### Defining permission predicates + +Before we tell Heapster the type of `add`, as described above, we +need to define the predicate `int64` with the following type + +``` +exists x:bv 64.eq(llvmword(x)) +``` + +It says that there exist some bit-vector of length 64 (`bv 64`) which +is equal, as an llvm word, to the "current variable". In other words, +it says that the current variable is equal to some number that can be +described as a bit-vector of size 64. + +To notify Heapster of this predicate we use the command +`heapster_define_perm`, which defines a new named permission which can +then be used in Heapster types. + +``` +heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))" +``` + +The first argument is the Heapster environment, the second is its +name, the third is its arguments (of which there are none), the fourth +is the type of value that the permission applies to, and the fifth is +its permision type. Notice how in Heapster, most of the arguments are +passed as strings. + +With this, the new permission is created and added to the +environment. Uses of this named permission are written `int64<>` where +the `<>` is the empty list of arguments, as seen in the type of `add` +above. Unfortunately, there is currently no way to print the newly defined +permissions. If you try to print the environment (`print env`) at this +point, you will only see the `llvm` definitions. We might add +functionality for showing permissions in the future. + +#### 5. Type-check your program + +Armed with the `int64` predicate, we can write the type for `add` and +ask Heapster to type check it. + +``` +heapster_typecheck_fun env "add" "().arg0:int64<>, arg1:int64<> -o arg0:true, arg1:true, ret:int64<>" +``` + +The `heapster_typecheck_fun` command takes the environment, the name +of the function to typecheck and its permision type. The command then +attempts to typecheck the function and extracts its functional +specification. The functional specification is then added to the SAW +core module `tutorial_c` with the sufix `__tuple_fun`, in this case +`add__tuple_fun`. + +The function `add_mistyped`, in the same `tutorial_bc` and already +loaded in the Heapster environment, is identical to `add` so we can +experiment with misstyping. Try running the following command + +``` +heapster_typecheck_fun env "add_mistyped" "().arg0:true, arg1:int64<> -o arg0:true, arg1:true, ret:int64<>" +``` + +The first argument is typed as `true`, but we know it is an `i64` +which can't be proven from the trivial `true`. So this type check +should fail, but it silently terminates! What gives? + +Heapster allows for the typechecker to fail in parts of +the function and the extraction will translate those parts into the +error specification. The user could then, for example, prove that +those locations are not reachable in the program, for full +correctness. Unfortunately, this means that the typechecking will fail +silently and an error won't be caught until we check the Coq +extraction, as we show in the next section. + +#### 6. Writing a Coq file to prove things about the generated functional specification(s) + +Once you're finished, use the following command to export all the +type-checked functions in the current environment as functional +specifications in Coq. By convention, we add a `_gen` suffix to the +filename. + +``` +heapster_export_coq env "tutorial_c_gen.v"; +``` + +Open up the new `tutorial_c_gen.v` file in your examples +directory. You should see a handfull of auto-generated imports and four +definitions. + +The first definition, `add__tuple_fun`, contains the tuple with the +proof the proof of correctness of the extracted code. The second +definition, `add`, is just the extracted functional specification of +the llvm function of the same name, obtained from projecting from +`add__tuple_fun`. + +The other two definitions are the equivalent definitions for the +`add_mistyped` function. However, in `add_mistyped__tuple_fun` you +will find a call to `errorM` with an error message + +``` +implUnfoldOrFail: Could not prove + top_ptr1:true -o (). is_llvmptr +``` + +explaining that, for the first pointer (that is `arg0`) it couldn't +prove that `true -o (). is_llvmptr`, as we expected. The function +couldn't be typechecked with the given type. The lack of calls to +`errorM` in `add__tuple_fun` confirms that it was correctly +typechecked. + +Notice that the converse is not true: there are some well-typed +functions that will still use `errorM` in their extracted function to, +for example, dynamically check for memory bounds. We will see those +examples in later sections. **TODO: Make sure we do this. Perhaps add +an array example?** + +**TODO: how do you interact with these coq types.** -Let's load our module with +### Pointers + +The next function we will type-check is a simple function that +increments the value in a pointer + +```C +void incr_ptr (uint64_t *x) { *x += 1; } +``` + +Assuming you completed the last section, you should have interactive +saw open, the `tutorial_c.bc` loaded in the environment `env`, so +`incr_ptr` should already be in your environment, but you can double +check by printing `env`. We can then skip the steps 1-3 and go +directly to writing heapster types for the function. + +The type for this function should be + +``` +(). arg0:ptr((W,0) |-> int64<>) -o arg0:ptr((W,0) |-> int64<>) +``` + +As before, the ghost environment is ommited and both sides of the +implication are identical, since the function doesn't change the shape +of memory. The return value is `void`, so we can omit it or add a +trivial `ret:true`. + +The permission for pointers `ptr` takes three arguments. First, it +describes the read-write modality. In this case the +pointer is writable `W`, since it will be modified. The second +argument describes the pointer offset, here `0`. Finaly, the third +argument describes the content of the pointer, in this case a 64-bit +integer `int64<>`. + +Then we can type-check the function with + +``` +heapster_typecheck_fun env "incr_ptr" "(). arg0:ptr((W,0) |-> int64<>) -o arg0:ptr((W,0) |-> int64<>)" +``` + +**TODO: How do I know if the type-checking was successful?** + +Finally we can generate the functional specification in Coq with + +``` +heapster_export_coq env "tutorial_c_gen.v"; +``` + +The old file should be overwritten and now contains the functional +specification of `add`, `add_misstyped` and `incr_ptr`. As you can see +the definition of `incr_ptr__tuple_fun` has no references to `errorM`, +so we know it was correctly type checked. + +### Structs + +The next function we will type-check deals with structs. In our +example, we defined a function that can compute the norm of a 3D +vector + +``` C +// Struct that represents the three coordinates fora 3D vector +typedef struct { uint64_t x; uint64_t y; uint64_t z; } vector3d; + +// function that computes the norm of a 3D vector +// || (x,y,z) || = x^2+y^2+z^2 +uint64_t norm_vector (vector3d *v) { return (v->x * v->x + v->y * v->y + v->z * v->z); } +``` + +Again, we assume that you still have the definitions from the previous +sections so we can start defining the type for the function. + +Let's start by defining a predicate for `vector3d` like so + +``` +heapster_define_perm env "vec3d" "rw:rwmodality" "llvmptr 64" "ptr((rw,0) |-> int64<>) * ptr((rw,8) |-> int64<>) * ptr((rw,16) |-> int64<>)" +``` + +First, notice that we added an arguments `rw` of type +`rwmodality`. This is such that we can control if the vector is +readable or writable. Second, notice that the predicate still applies +to 64-bit pointers. Finally, the type describes three integers, all +with the read-write modality given by the argument `rw`, at offsets +`0`, `8` and `16` and each with an `int64`. + +Then we can define the type of `norm_vector` as + +``` +(). arg0:vec3d -o arg0:vec3d, ret:int64<> +``` + +which says that the function takes a readable 3d vector, and returns +an integer. Notice that the `arg0` on the right hand side could also +be written as `arg0:true`. However, we still want to express that the +function does change that memory so we make it explicit. + +Then we can type-check the function with + +``` +heapster_typecheck_fun env "norm_vector" "(). arg0:vec3d -o arg0:vec3d, ret:int64<>" +``` + +Finally we can generate the functional specification in Coq with + +``` +heapster_export_coq env "tutorial_c_gen.v"; +``` + +The functional specification of `norm_vector` should have been added +to the `tutorial_c_gen.v` file. + + +### Recursive data structures + +We will now typecheck a function over lists, a recursive data +structure. You can start a fresh SAW session with `cabal run saw` +(quit any current session with `:q`), but make sure you do so from the +`heapster-saw/examples` directory. + +Specifically, we want to verify the function `is_elem`, +which tests if a specific value is in a list. The function, together +with others, can be found in `linked_list.c`, in the examples +directory. + +```C +typedef struct list64_t { + int64_t data; + struct list64_t *next; +} list64_t; + +int64_t is_elem (int64_t x, list64_t *l) { + if (l == NULL) { + return 0; + } else if (l->data == x) { + return 1; + } else { + return is_elem (x, l->next); + } +} +``` + +#### 1. Generating LLVM bitcode + +We have already included the binary for all the examples, but if you +want to generate it yourself, you can run + +```bash +make linked_list.bc +``` + +#### 2. Run the SAW interpreter with Heapster + +Load the Heapster commands + +```bash +sawscript> enable_experimental +``` + +#### 3. Load the file and extract the function types. + +To work with lists, we need add the SAW core definition of lists to +our SAW core module. The definition is + +``` +List_def : (a:sort 0) -> sort 0; +List_def a = List a; +``` + +**TODO: what is this definition? Why can't we just use `List a`** + +We can add such definitions to a SAW core file. One has already been +created for you at `linked_list.sawcore`. Then we start our environment with ``` env <- heapster_init_env_from_file "linked_list.sawcore" "linked_list.bc"; ``` -we have created a new Heapster environment that we can explore. +Very much like `heapster_init_env`, `heapster_init_env_from_file` +creates a new environment but, instead of creating a fresh SAW core +module, it initialises the module with the given file, here +`linked_list.sawcore`. Just as before, this creates a new Heapster +environment that we can explore. ``` sawscript> print env @@ -508,48 +852,32 @@ Definitions: %struct.list64_t* %1) ``` -The heapster environment contains all the types, global definitions, -external references and functions from the loaded module. - - #### 4. Writing heapster types for your functions -##### Pen and paper type - -Before we go foward using Heapster, let's think about what the -type for `is_elem` should be. As we can check in the -environment `env`, `is_elem` takes a 64-bit integer the "element". +We can check in the environment `env` for the LLVM type of the function we +are type checkingt. ```LLVM i64 @is_elem(i64 %0, %struct.list64_t* %1) ``` -Hence, precondition to the function should reflect these two inputs -like so `arg0:int64, arg1: list int64`, for some predicates `int64` -and `list` that express a single integer and a list of them. - -Moreover, the function returns a new i64-bit integer and, as we can -see in the code of `is_elem`, the arguments are not modified. So the -postcondition, of the function could be described by `arg0:int64, -arg1: list int64, ret:int64`. Alternatively, if we don't care about -the inputs after the call we can simplify it to `arg0:true, arg1: -true, ret:int64`, where `true` is a predicate the is always satisfied. - -Then, using the linear implication `-o` we can express the -type of `is_elem` as +The function `is_elem` takes a 64-bit integer and a list of 64-bit +integers, and returns another 64-bit integer. After the return, we +don't care about the inputs, so we can write the type like this ``` -arg0:int64, arg1: list int64 -o arg0:true, arg1:true, ret:int64 +().arg0:int64<>, arg1:List64 -o arg0:true, arg1:true, ret:int64<> ``` -Notice that this is a memory-safety type, not a correctness -predicate. We can reason about the correctness of the function once we -extract it as a functional program in Coq. +We know how to define `int64`, as we did before, + +``` +sawscript> heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))" +``` -In the next sections, we shall define the predicates necessary to -write this type in Heapster. +but we need a new predicate for lists. -##### Defining permission predicates +##### Defining list permissions One of the simplest Heapster commands is `heapster_define_perm`, which defines a new named permission which can then be used in Heapster types. As an From a7487bb36d5376f6734330ed79b21e3a638901f1 Mon Sep 17 00:00:00 2001 From: santiago Date: Tue, 30 Aug 2022 15:14:19 -0400 Subject: [PATCH 15/23] First sketch of the tutorial after adding simpler examples. --- heapster-saw/doc/tutorial/tutorial.md | 206 ++++++++++++++------------ heapster-saw/examples/tutorial_c.saw | 23 +++ 2 files changed, 138 insertions(+), 91 deletions(-) create mode 100644 heapster-saw/examples/tutorial_c.saw diff --git a/heapster-saw/doc/tutorial/tutorial.md b/heapster-saw/doc/tutorial/tutorial.md index fa34f1cdf8..0d3e6682cf 100644 --- a/heapster-saw/doc/tutorial/tutorial.md +++ b/heapster-saw/doc/tutorial/tutorial.md @@ -20,6 +20,7 @@ examples to get anyone up to speed with using and hacking on Heapster. - [First example](#first-example) - [Pointers](#pointers) - [Structs](#structs) + - [Batch scripts](#batch-scripts-1) - [Recursive data structures](#recursive-data-structures) - [Looking under the hood](#looking-under-the-hood) - [Heapster commands and environments](#heapster-commands-and-environments) @@ -36,7 +37,7 @@ commands here are with respect to the top-level saw-script directory. ### Build Saw -You will need to follow the instructions in the top-level README to +You will need to follow the instructions in the top-level [README](../../README.md) to download or build a SAW binary, of which Heapster is a part. In particular, make sure you follow the instructions to install Z3. Once `./build.sh` succeeds it should report @@ -62,10 +63,11 @@ sawscript> :quit ### Build the Coq backend for Saw -In this tutorial we will also interact with Heapster's Coq output. So you'll need -to follow the instructions in the README in the `saw-core-coq` subdirectory. -Specifically, after installing the dependencies, you will need to run the -following (from the top level directory): +In this tutorial we will also interact with Heapster's Coq output. So +you'll need to follow the instructions in the +[README](../../../saw-core-coq/README.md) in the `saw-core-coq` +subdirectory. Specifically, after installing the dependencies, you +will need to run the following (from the top level directory): ```bash cd saw-core-coq/coq @@ -407,7 +409,7 @@ code has been provided already to avoid incompatibilities. We start by running saw with `cabal run saw`. Once SAW is loaded, you can load all the Heapster commands with -```bash +``` sawscript> enable_experimental ``` @@ -737,7 +739,7 @@ Then we can define the type of `norm_vector` as (). arg0:vec3d -o arg0:vec3d, ret:int64<> ``` -which says that the function takes a readable 3d vector, and returns +which says that the function takes a readable 3D vector, and returns an integer. Notice that the `arg0` on the right hand side could also be written as `arg0:true`. However, we still want to express that the function does change that memory so we make it explicit. @@ -758,6 +760,58 @@ The functional specification of `norm_vector` should have been added to the `tutorial_c_gen.v` file. +### Batch scripts + +Notice that, just like in saw, Heapster scripts can be processed in +batch. You can create a file `tutorial_c.saw` with all the commands so +far. It should look something like this + +``` +enable_experimental +env <- heapster_init_env "tutorial_c" "tutorial_c.bc" +print "File loaded" + +heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))" +print "Defined an 64-bit integer." + +heapster_typecheck_fun env "add" "().arg0:int64<>, arg1:int64<> -o arg0:true, arg1:true, ret:int64<>" +print "Type checked add." + +heapster_typecheck_fun env "add_mistyped" "().arg0:true, arg1:int64<> -o arg0:true, arg1:true, ret:int64<>" +print "Type checked add_mistyped. This will produce an error in the output." + +heapster_typecheck_fun env "incr_ptr" "(). arg0:ptr((W,0) |-> int64<>) -o arg0:ptr((W,0) |-> int64<>)" +print "Type checked incr_ptr." + + +heapster_define_perm env "vec3d" "rw:rwmodality" "llvmptr 64" "ptr((rw,0) |-> int64<>) * ptr((rw,8) |-> int64<>) * ptr((rw,16) |-> int64<>)" +heapster_typecheck_fun env "norm_vector" "(). arg0:vec3d -o arg0:vec3d, ret:int64<>" +print "Type checked incr_ptr." + +heapster_export_coq env "tutorial_c_gen.v"; +print "Export to Coq." + +print "Done." +``` + +then you can process it with just + +``` +% cabal run saw -- tutorial_c.saw +Up to date + + + +[16:41:49.222] Loading file "/Users/Santiago/Projects/saw-script/heapster-saw/examples/tutorial_c.saw" +[16:41:49.230] File loaded +[16:41:49.245] Type checked add. +[16:41:49.249] Type checked add_mistyped. This will produce an error in the output. +[16:41:49.257] Type checked incr_ptr. +[16:41:49.312] Type checked norm_vector. +[16:41:49.329] Export to Coq. +[16:41:49.329] Done. +``` + ### Recursive data structures We will now typecheck a function over lists, a recursive data @@ -817,17 +871,26 @@ List_def a = List a; **TODO: what is this definition? Why can't we just use `List a`** We can add such definitions to a SAW core file. One has already been -created for you at `linked_list.sawcore`. Then we start our environment with +created for you at `linked_list.sawcore`. Every SAW core file starts +with the declaration of the module name and, most files, import the +Prelude. + +``` +module linked_list where + +import Prelude; +``` + +With this file created, we start our environment with ``` env <- heapster_init_env_from_file "linked_list.sawcore" "linked_list.bc"; ``` -Very much like `heapster_init_env`, `heapster_init_env_from_file` -creates a new environment but, instead of creating a fresh SAW core -module, it initialises the module with the given file, here -`linked_list.sawcore`. Just as before, this creates a new Heapster -environment that we can explore. +which, much like `heapster_init_env`, creates a new environment but, +instead of creating a fresh SAW core module, it initialises the module +with the given file, here `linked_list.sawcore`. Just as before, this +creates a new Heapster environment that we can explore. ``` sawscript> print env @@ -855,7 +918,7 @@ Definitions: #### 4. Writing heapster types for your functions We can check in the environment `env` for the LLVM type of the function we -are type checkingt. +are type checking. ```LLVM i64 @is_elem(i64 %0, %struct.list64_t* %1) @@ -869,63 +932,38 @@ don't care about the inputs, so we can write the type like this ().arg0:int64<>, arg1:List64 -o arg0:true, arg1:true, ret:int64<> ``` -We know how to define `int64`, as we did before, - -``` -sawscript> heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))" -``` - -but we need a new predicate for lists. +But we will need to define the predicates for `int64` and `List64` ##### Defining list permissions -One of the simplest Heapster commands is `heapster_define_perm`, which defines -a new named permission which can then be used in Heapster types. As an -example, the following defines the permission which describes a 64-bit integer -value: +We know how to define `int64`, as we did before, ``` -heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))" +sawscript> heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))" ``` -The first argument is the Heapster environment, the second is its -name, the third is its arguments (of which there are none), the fourth -is the type of value that the permission applies to, and the fifth is -its permision type. The new permission is created and added to the -environment. - -Uses of this named permission are written `int64<>` where the `<>` is -the empty list of arguments. - -Unfortunately, there is currently no way to print the newly defined -permissions. If you try to print the environment (`print env`) at this -point, you will only see the `llvm` definitions. We might add -functionality for showing permissions in the future. - -Before we look at the definition of a `List64` lets focus on its -permission type. First of all, `List64` takes a single argumetn -`rw` which determines if the list is readable or writable. It's type -should look something like this +but we need a new predicate for lists. Before we look at the +definition of a `List64` lets focus on its permission type. First +of all, `List64` takes a single argument `rw:rwmodality` which +determines if the list is readable or writable, jus like 3D +vectors. It's type should look something like this ``` ["eq(llvmword(0))", "ptr((rw,0) |-> int64<>) * ptr((rw,8) |-> List64)"] ``` the definition shows the diferent cases for a list, separated by a -coma. In the first case, a `List64` is can be a null pointer, -expressed with the type `eq(llvmword(0))`. In the second case, a list -is a pointer where offset 0 is the head, an `Int64`, and offset `8` -it's the tail, another `List64`, i.e., it is recursively a -`List64` . In the later case, both elements are tagged with `rw`, -describing if they are readable or writable, as determined by the -argument to `List64`. - -You might have noticed that the permission predicate for lists is -recursive, since it must refer to it's tail which is itself a list. To -define [permissions](doc/Permissions.md) which can describe unbounded -data structures, you can use the `heapster_define_recursive_perm` -command. As an example, here is how to describe a linked list of -64-bit words using this command: +coma. In the first case, a `List64` can be a null pointer, expressed +with the type `eq(llvmword(0))`. In the second case, a list is a +pointer where offset `0` is the head, an `Int64`, and offset `8` it's +the tail, is recursively a `List64`. In the later case, +both elements are tagged with `rw`, describing if they are readable or +writable, as determined by the argument to `List64`. + +To define [permissions](doc/Permissions.md) which can describe +unbounded data structures, you can use the +`heapster_define_recursive_perm` command. here is how to use the +command to define lists. ``` heapster_define_recursive_perm @@ -934,45 +972,23 @@ heapster_define_recursive_perm "rw:rwmodality" "llvmptr 64" ["eq(llvmword(0))", "ptr((rw,0) |-> int64<>) * ptr((rw,8) |-> List64)"] - "List (Vec 64 Bool)" - "foldList (Vec 64 Bool)" - "unfoldList (Vec 64 Bool)"; + "List_def" "foldList" "unfoldList"; ``` Its first four arguments are the same as for `heapster_define_perm`, -its fifth argument contains its different inductive cases which we -describe below, and its final three arguments are its translation into -SAW core. Here the SAW core definitions used are from the SAW core -prelude which are included by default when Heapster autogenerates a a -module for you. If you need new SAW core definitions, you will need to -use the following command instead of `heapster_init_env`: - -``` -env <- heapster_init_env_from_file "my_file.sawcore" "my_file.bc"; -``` - -See this [additional documentation](doc/Permissions.md) for a +namely the environment, the name, the arguments and the type of value +that the permission applies to. The fifth argument is its permision +type. The final three arguments are its translation into SAW core. As +you might remember, this is the `List_def` we defined in our SAW core +file which is now loaded in the module. The other two `foldList` and +`unfoldList` are **TODO: What are these???** + +See this [additional documentation](../Permissions.md) for a reference on the syntax and meaning of heapster permissions. -#### 5. Writing a SAW script to type-check your code with respect to the sepcification - -We begin by converting the pen-and-paper specification of `is_elem` -into a Heapster specification. First, every heapster type begins with -the declaration of a ghost environment. Our specification doesn't use -any ghost variable so that is `().` Moreover, every named definition -takes it's arguments within angled braces ``. For `int64`, which -takes no arguments that is just `<>`, and for `List` which takes a an -arguments to define that it is a readable list, it is ``. Whith -this we can write our specification as - -``` -().arg0:int64<>, arg1:List64 -o arg0:true, arg1:true, -ret:int64<> -``` +#### 5. Type-check your program -Finally, to actually type-check a function you can use -`heapster_typecheck_fun`. That takes the environment, the name of the -function to type-check and the type, like so +Just as before you only need to run ``` heapster_typecheck_fun env "is_elem" @@ -1002,8 +1018,16 @@ heapster_export_coq env "my_file_gen.v"; ## Looking under the hood +**TODO** + ### Heapster commands and environments +**TODO** + ### Permissions +**TODO** + ### Type-checking + +**TODO** diff --git a/heapster-saw/examples/tutorial_c.saw b/heapster-saw/examples/tutorial_c.saw new file mode 100644 index 0000000000..32a1c47454 --- /dev/null +++ b/heapster-saw/examples/tutorial_c.saw @@ -0,0 +1,23 @@ +enable_experimental; +env <- heapster_init_env "tutorial_c" "tutorial_c.bc"; +print "File loaded"; + +heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))"; +heapster_typecheck_fun env "add" "().arg0:int64<>, arg1:int64<> -o arg0:true, arg1:true, ret:int64<>"; +print "Type checked add."; + +heapster_typecheck_fun env "add_mistyped" "().arg0:true, arg1:int64<> -o arg0:true, arg1:true, ret:int64<>"; +print "Type checked add_mistyped. This will produce an error in the output."; + +heapster_typecheck_fun env "incr_ptr" "(). arg0:ptr((W,0) |-> int64<>) -o arg0:ptr((W,0) |-> int64<>)"; +print "Type checked incr_ptr."; + +heapster_define_perm env "vec3d" "rw:rwmodality" "llvmptr 64" "ptr((rw,0) |-> int64<>) * ptr((rw,8) |-> int64<>) * ptr((rw,16) |-> int64<>)"; +heapster_typecheck_fun env "norm_vector" "(). arg0:vec3d -o arg0:vec3d, ret:int64<>"; +print "Type checked norm_vector."; + +heapster_export_coq env "tutorial_c_gen.v"; +print "Export to Coq."; + +print "Done."; + From d4a8391864b97ddf9a0902bdc3a48f864772e970 Mon Sep 17 00:00:00 2001 From: santiago Date: Tue, 30 Aug 2022 16:51:50 -0400 Subject: [PATCH 16/23] Added some detail for Coq files. --- heapster-saw/doc/tutorial/tutorial.md | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/heapster-saw/doc/tutorial/tutorial.md b/heapster-saw/doc/tutorial/tutorial.md index 0d3e6682cf..984b51aa8f 100644 --- a/heapster-saw/doc/tutorial/tutorial.md +++ b/heapster-saw/doc/tutorial/tutorial.md @@ -621,11 +621,18 @@ Open up the new `tutorial_c_gen.v` file in your examples directory. You should see a handfull of auto-generated imports and four definitions. -The first definition, `add__tuple_fun`, contains the tuple with the -proof the proof of correctness of the extracted code. The second -definition, `add`, is just the extracted functional specification of -the llvm function of the same name, obtained from projecting from -`add__tuple_fun`. +The first two definitions `add__tuple_fun` and `add` might have a +scary looking types, but they simplify to + +``` +add__tuple_fun : (bitvector 64 -> bitvector 64 -> CompM (bitvector 64)) * unit +add : bitvector 64 -> bitvector 64 -> CompM (bitvector 64) +``` + +That is, `add__tuple_fun` if a pair containing the `add` function and +a unit `()`. The `add` function takes two integers (as 64-bit +vectors) and returns another one (under the `CompM` monoid that +accepts failure). The other two definitions are the equivalent definitions for the `add_mistyped` function. However, in `add_mistyped__tuple_fun` you From a3608865a39c8652e5a026d109722559597f882c Mon Sep 17 00:00:00 2001 From: santiago Date: Wed, 14 Sep 2022 14:20:06 -0400 Subject: [PATCH 17/23] Add the cow proofs and documentation for the array examples. --- heapster-saw/doc/tutorial/tutorial.md | 274 +++++++++++++++++++--- heapster-saw/examples/tutorial_c_proofs.v | 89 +++++++ 2 files changed, 332 insertions(+), 31 deletions(-) create mode 100644 heapster-saw/examples/tutorial_c_proofs.v diff --git a/heapster-saw/doc/tutorial/tutorial.md b/heapster-saw/doc/tutorial/tutorial.md index 984b51aa8f..651a11f950 100644 --- a/heapster-saw/doc/tutorial/tutorial.md +++ b/heapster-saw/doc/tutorial/tutorial.md @@ -629,10 +629,13 @@ add__tuple_fun : (bitvector 64 -> bitvector 64 -> CompM (bitvector 64)) * unit add : bitvector 64 -> bitvector 64 -> CompM (bitvector 64) ``` -That is, `add__tuple_fun` if a pair containing the `add` function and -a unit `()`. The `add` function takes two integers (as 64-bit -vectors) and returns another one (under the `CompM` monoid that -accepts failure). +That is, `add__tuple_fun` if a list of definitions, encoded as a +tuple. Saw uses these heterogeneous lists to encode functions, or +parts of them, that depend on each other. In this case, there is only +the function `add` function and a unit `()`, representing the end of +the list (similar to `nil`). The `add` function takes two integers +(as 64-bit vectors) and returns another one (under the `CompM` monoid +that accepts failure). The other two definitions are the equivalent definitions for the `add_mistyped` function. However, in `add_mistyped__tuple_fun` you @@ -655,7 +658,75 @@ for example, dynamically check for memory bounds. We will see those examples in later sections. **TODO: Make sure we do this. Perhaps add an array example?** -**TODO: how do you interact with these coq types.** +Before we continue, make sure to build the `.vo` file, so we can +import the definitions in `tutorial_c_gen.v` from other files. Do so with + +``` +make tutorial_c_gen.vo +``` + +This should produce a new file `tutorial_c_gen.vo`. + + +##### Writting your own proofs + +Open a new coq file `tutorial_c_proofs.v` in the same folder +(i.e. `heapster-saw/examples/`) and the following preamble + +``` +From CryptolToCoq Require Import SAWCoreScaffolding. +From CryptolToCoq Require Import SAWCorePrelude. +From CryptolToCoq Require Import CompMExtra. + +(* The following line enables pretty printing*) +Import CompMExtraNotation. Open Scope fun_syntax. + +Require Import Examples.tutorial_c_gen. +Import tutorial_c. +``` + +It first imports all the SAW functionality we need and enables pretty +printing. Then it imports our new definitions (e.g. `add`). + +Our first proof, will claim that the function `add`, produces no +errors. Morr specifically, it says that for all inputs (that's what +`refinesFun` quantifies) `add` allways refines to `noErrorsSpec`, that +is it returns a pure value. + +``` +Lemma no_errors_add + : refinesFun add (fun _ _ => noErrorsSpec). +Proof. +``` + +We will use our automation to quickly prove the lemma, but we must +first unfold those definitions the the automation is unfamiliar with. + +``` +unfold add, add__tuple_fun, noErrorsSpec. +``` + +Then our function `prove_refinement` will deal with the proof. + +``` + prove_refinement. +Qed. +``` + +You can also attempt the same proof with `add_mistyped`, which +obviously will fail, since `add_mistyped` has an error. + +``` +Lemma no_errors_add_mistyped + : refinesFun add_mistyped (fun _ => noErrorsSpec). +Proof. + unfold add_mistyped, add_mistyped__tuple_fun, noErrorsSpec. + prove_refinement. + (* Fails to solve the goal. *) +Abort. +``` + +Congratulations you have written your first Coq proofs with Heapster! ### Pointers @@ -696,8 +767,6 @@ Then we can type-check the function with heapster_typecheck_fun env "incr_ptr" "(). arg0:ptr((W,0) |-> int64<>) -o arg0:ptr((W,0) |-> int64<>)" ``` -**TODO: How do I know if the type-checking was successful?** - Finally we can generate the functional specification in Coq with ``` @@ -709,6 +778,19 @@ specification of `add`, `add_misstyped` and `incr_ptr`. As you can see the definition of `incr_ptr__tuple_fun` has no references to `errorM`, so we know it was correctly type checked. +You will have to generate the `.vo` again to write proofs about +`incr_ptr`. After you do so, we can easily prove that `incr_ptr` +produces no errors. + +``` +Lemma no_errors_incr_ptr + : refinesFun incr_ptr (fun _ => noErrorsSpec). +Proof. + unfold incr_ptr, incr_ptr__tuple_fun. + prove_refinement. +Qed. +``` + ### Structs The next function we will type-check deals with structs. In our @@ -764,8 +846,10 @@ heapster_export_coq env "tutorial_c_gen.v"; ``` The functional specification of `norm_vector` should have been added -to the `tutorial_c_gen.v` file. - +to the `tutorial_c_gen.v` file. You will have to generate the `.vo` +again to write proofs about `norm_vector`. After you do so, we can +easily prove that `norm_vector` produces no errors. The statement and +the proof, follow exactly the last two lemmas. ### Batch scripts @@ -819,12 +903,160 @@ Up to date [16:41:49.329] Done. ``` + +### Arrays + +We will briefly explore arrays, which have slightly more intersting +memory restrictions. Namely, array access must be in bounds. The code +in this section are already generated for you and you can find them, +together with more examples in the files `arrays.c`, `arrays.saw`, +`arrays_gen.v` and `arrays_proofs.v`. + +We will consider the function `zero_array` which rewrite all the +values in an array to be `0`, by looking over the length of the array +(see code in `arrays.c`). + +```C +void zero_array (int64_t *arr, uint64_t len) { + for (uint64_t i = 0; i < len; ++i) { + arr[i] = 0; + } +} +``` + +The type for this function is relatively simple, it only assumes that +`len` is actually the length for the given array `arr`. This is +achieved by used a shared or ghost variable `len` which is both the +lenght of the array and equal to the second argument (see the code in `arrays.saw`) + +``` +heapster_typecheck_fun env "zero_array" + "(len:bv 64). arg0:int64array, arg1:eq(llvmword(len)) -o \ + \ arg0:int64array, arg1:true, ret:true"; +``` + +Heapster also expects a loop invariant hint for every loop. Loop +invariants look just like function types, taking the loop variables as +arguments. In this case the loop introduces a new variable `i` which +is the ofset into the array. We represent that with a new ghost +variable + +``` +heapster_typecheck_fun env "zero_array_from" + "(len:bv 64, off:bv 64). arg0:int64array, arg1:eq(llvmword(len)), arg2:eq(llvmword(off)) -o \ + \ arg0:int64array, arg1:true, arg2:true, ret:true"; +``` + +Certainly function correctness must ensure that all the writes to the +array (i.e. `arr[i] = 0`) happen within bounds. However this is a +dynamic property which is not part of type-checking. Instead, Heapster +adds dynamic checks on the extracted code which we will see in the coq +code. + +Let's go to `arrays_gen.v` and look for the definition of +`zero_array__tuple_fun`. You will notice that it calls `errorM` but, +in this case that's not a sign of a typing error! This error call +corresponds to the case where the array is accessed out of bounds. The +code below is a simplification of the `zero_array__tuple_fun` with +some notation for readability (see below for how to enable such pritty printing). + +``` +zero_array__tuple_fun = + (* ... Some ommited code ... *) + LetRec f:= + (fun (e1 e2 : int64) (p1 : Vector int64 e1) + (_ _ _ : unit : Type) => + (* ... Some ommited code ... *) + let var__4 := (0)[1] in + let var__6 := e2 < e1 in + (*... Some ommited code ...*) + if + not + ((if var__6 then 1 else var__4) == + var__4) + then + if + ((17293822569102704640)[64] <= e2) && + (e2 <= (1152921504606846975)[64]) + then + If e2

assumingM (zero_array_precond x) noErrorsSpec). +Proof +``` + +It claims that, assuming the precondition `zero_array_precond` is +satisfied, then the function `zero_array` produces no errors. The +precondition simply says that the length of the array is within +computable integers. + +``` +Definition zero_array_precond x + := 64 <= x /\ x <= bvMem_hi. +``` + + +We will not go into detail about the proof, but notice that the +important steps are handled by custom automation. Namely we use the +commands `prove_refinement_match_letRecM_l` and `prove_refinement` to +handle refinments with and without recursion (respectively). The rest +of the proof, consists of discharging simple inequalities and a couple +of trivial entailments, where the left hand side is an error (and thus +entails anything). + ### Recursive data structures We will now typecheck a function over lists, a recursive data structure. You can start a fresh SAW session with `cabal run saw` -(quit any current session with `:q`), but make sure you do so from the -`heapster-saw/examples` directory. +(quit any current session with `:q` if you are in one), but make sure +you do so from the `heapster-saw/examples` directory. Specifically, we want to verify the function `is_elem`, which tests if a specific value is in a list. The function, together @@ -1018,23 +1250,3 @@ convention, we add a `_gen` suffix to the filename. ``` heapster_export_coq env "my_file_gen.v"; ``` - -#### 6. Writing a Coq file to prove things about the generated functional specification(s) - -**TODO** - -## Looking under the hood - -**TODO** - -### Heapster commands and environments - -**TODO** - -### Permissions - -**TODO** - -### Type-checking - -**TODO** diff --git a/heapster-saw/examples/tutorial_c_proofs.v b/heapster-saw/examples/tutorial_c_proofs.v new file mode 100644 index 0000000000..2e6c5be7cb --- /dev/null +++ b/heapster-saw/examples/tutorial_c_proofs.v @@ -0,0 +1,89 @@ +From CryptolToCoq Require Import SAWCoreScaffolding. +From CryptolToCoq Require Import SAWCorePrelude. +From CryptolToCoq Require Import CompMExtra. +Import CompMExtraNotation. (*Open Scope fun_syntax2.*) + +Declare Scope fun_syntax2. + + + + + Infix "&&" := SAWCoreScaffolding.and : fun_syntax2. + Infix "<=" := (SAWCoreVectorsAsCoqVectors.bvsle _) : fun_syntax2. + Notation " a

f) m) (at level 100) : fun_syntax2. + Notation "'If' m 'Then' f 'Else' default " := (SAWCorePrelude.maybe _ _ default (fun _ => f) m) (at level 99) : fun_syntax2. + Notation "v [ ix <- elem ]" := (SAWCorePrelude.updBVVec _ _ _ v ix elem) (at level 100) : fun_syntax2. + Infix "+" := (SAWCoreVectorsAsCoqVectors.bvAdd _) : fun_syntax2. + Notation "'Forall' x : T , f" := (LRT_Fun T (fun x => f)) (at level 100, format " 'Forall' x : T , '/ ' f") : fun_syntax2. + Notation "T ->> f" := (LRT_Fun T (fun _ => f)) (at level 99, right associativity, format "T '/' ->> '/' f") : fun_syntax2. + Notation "x" := (LRT_Ret x) (at level 99, only printing) : fun_syntax2. + Notation "'Vector' T len":= (SAWCorePrelude.BVVec _ len T) (at level 98) : fun_syntax2. + Notation "[[ x1 ]]":= ((LRT_Cons x1 LRT_Nil )) (at level 7, format "[[ '[' x1 ']' ]]") : fun_syntax2. + Notation "[[ x1 ; x2 ; .. ; xn ]]":= ((LRT_Cons x1 (LRT_Cons x2 .. (LRT_Cons xn LRT_Nil) .. ))) + (at level 7, format "[[ '[' x1 ; '/' x2 ; '/' .. ; '/' xn ']' ]]") : fun_syntax2. + Notation "[ x1 ]__lrt":= (lrtTupleType (LRT_Cons x1 LRT_Nil )) (at level 7, format "[ '[' x1 ']' ]__lrt") : fun_syntax2. + Notation "[ x1 ; x2 ; .. ; xn ]__lrt":= (lrtTupleType (LRT_Cons x1 (LRT_Cons x2 .. (LRT_Cons xn LRT_Nil) .. ))) + (at level 7, format "[ '[' x1 ; '/' x2 ; '/' .. ; '/' xn ']' ]__lrt") : fun_syntax2. + Notation "'int64'" := (SAWCoreVectorsAsCoqVectors.bitvector 64) (at level 97) : fun_syntax2. + Notation "'int32'" := (SAWCoreVectorsAsCoqVectors.bitvector 32) (at level 97) : fun_syntax2. + Notation "'bool'" := (SAWCoreVectorsAsCoqVectors.bitvector 1) (at level 97) : fun_syntax2. + Notation "[ x ]__ty" := (lrtToType x) (only printing) : fun_syntax2. + Notation "'LetRec' x := f 'InBody' ( body )" := (letRecM _ (fun x => f) (fun x => body)) + (at level 0, only printing, + format "'[ ' 'LetRec' x := '//' '[' f ']' '//' 'InBody' '/' ( '[' body ']' ) ']'") : fun_syntax2. +Notation "x" := (letRecM LRT_Nil tt x) + (at level 99, only printing) : fun_syntax2. + Notation "[Functions: f1 := f1_body ]" := (multiFixM (fun f1 => (f1_body, tt))) + (at level 100, only printing, format "[Functions: '//' f1 := '[' f1_body ']' ]") : fun_syntax2. + Notation "[Functions: f1 := f1_body f2 := f2_body ]" := (multiFixM (fun f1 f2 => (f1_body, f2_body, tt))) + (at level 100, only printing, format "[Functions: '//' f1 := '[' f1_body ']' '//' f2 := '[' f2_body ']' ]") : fun_syntax2. + +Delimit Scope fun_syntax2 with sytx. + +Require Import Examples.tutorial_c_gen. +Import tutorial_c. + +Lemma no_errors_add + : refinesFun add (fun _ _ => noErrorsSpec). +Proof. + + unfold add, add__tuple_fun. + Open Scope fun_syntax2. + (* Visually simplifies trivial letRecM*) + + + simpl. + Notation + + noErrorsSpec. + + prove_refinement. +Qed. + +Lemma no_errors_add_mistyped + : refinesFun add_mistyped (fun _ => noErrorsSpec). +Proof. + unfold add_mistyped, add_mistyped__tuple_fun, noErrorsSpec. + prove_refinement. + (* Fails to solve the goal. *) +Abort. + + +Lemma no_errors_incr_ptr + : refinesFun incr_ptr (fun _ => noErrorsSpec). +Proof. + unfold incr_ptr, incr_ptr__tuple_fun, noErrorsSpec. + prove_refinement. +Qed. + +Lemma no_errors_norm_vector + : refinesFun norm_vector (fun _ _ _ => noErrorsSpec). +Proof. + unfold norm_vector, norm_vector__tuple_fun, noErrorsSpec. + prove_refinement. +Qed. From 3d2d398525a1b54014006c6e794a88095ab41573 Mon Sep 17 00:00:00 2001 From: santiago Date: Wed, 14 Sep 2022 14:20:33 -0400 Subject: [PATCH 18/23] Add notations. --- .../coq/handwritten/CryptolToCoq/CompMExtra.v | 247 +++++++++++------- 1 file changed, 148 insertions(+), 99 deletions(-) diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v b/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v index ce8aece388..581843c983 100644 --- a/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v +++ b/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v @@ -36,21 +36,21 @@ Tactic Notation "unfold_projs" "in" "*" := Ltac split_prod_hyps := repeat match goal with - | H: _ /\ _ |- _ => destruct H as [?H ?H] - | p: { _ : _ & _ } |- _ => destruct p as [?p ?p] - | p: _ * _ |- _ => destruct p as [?p ?p] - | u: unit |- _ => destruct u - | u: True |- _ => destruct u - end. + | H: _ /\ _ |- _ => destruct H as [?H ?H] + | p: { _ : _ & _ } |- _ => destruct p as [?p ?p] + | p: _ * _ |- _ => destruct p as [?p ?p] + | u: unit |- _ => destruct u + | u: True |- _ => destruct u + end. Ltac split_prod_goal := repeat match goal with - | |- _ /\ _ => split - | |- { _ : _ & _ } => split - | |- _ * _ => split - | |- unit => exact tt - | |- True => trivial - end. + | |- _ /\ _ => split + | |- { _ : _ & _ } => split + | |- _ * _ => split + | |- unit => exact tt + | |- True => trivial + end. (*** @@ -112,7 +112,7 @@ Proof. Qed. Lemma refinesM_eithers_cons_l - {A B C} (f:A -> CompM C) (g:B -> CompM C) elims eith P : + {A B C} (f:A -> CompM C) (g:B -> CompM C) elims eith P : (forall a, eith = SAWCorePrelude.Left _ _ a -> f a |= P) -> (forall eith', eith = SAWCorePrelude.Right _ _ eith' -> @@ -129,13 +129,13 @@ Proof. Qed. Lemma refinesM_eithers_cons_r - {A B C} (f:A -> CompM C) (g:B -> CompM C) elims eith P : + {A B C} (f:A -> CompM C) (g:B -> CompM C) elims eith P : (forall a, eith = SAWCorePrelude.Left _ _ a -> P |= f a) -> (forall eith', eith = SAWCorePrelude.Right _ _ eith' -> P |= SAWCorePrelude.eithers _ (SAWCorePrelude.FunsTo_Cons _ _ g elims) eith') -> P |= - SAWCorePrelude.eithers + SAWCorePrelude.eithers (CompM C) (SAWCorePrelude.FunsTo_Cons _ _ f (SAWCorePrelude.FunsTo_Cons _ _ g elims)) eith. @@ -200,12 +200,12 @@ Hint Extern 999 (_ |= _) => shelve : refinesM. Hint Resolve refinesM_letRecM_Nil_l : refinesM. Hint Extern 1 (@letRecM ?lrts _ _ _ |= @letRecM ?lrts _ (lrtLambda (fun _ => _)) _) => - apply refinesM_letRecM_const_r; try apply ProperLRTFun_any; - try (apply refinesFunTuple_multiFixM; unfold refinesFunTuple; split_prod_goal); - unfold lrtApply, lrtLambda; unfold_projs : refinesM. + apply refinesM_letRecM_const_r; try apply ProperLRTFun_any; +try (apply refinesFunTuple_multiFixM; unfold refinesFunTuple; split_prod_goal); +unfold lrtApply, lrtLambda; unfold_projs : refinesM. Inductive ArgName := Any | SAWLet | Either | Maybe | SigT | If | If0 | - Assert | Assuming | Exists | Forall. + Assert | Assuming | Exists | Forall. Ltac argName n := match n with | Any => fresh "a" @@ -310,7 +310,7 @@ Proof. intros eq; discriminate eq. Qed. Ltac IntroArg_intro_dependent_destruction n := let e := argName n in - IntroArg_intro e; dependent destruction e. + IntroArg_intro e; dependent destruction e. (* Hint Extern 1 (IntroArg ?n (eq (SAWCorePrelude.Nothing _) (SAWCorePrelude.Nothing _)) _) => *) (* IntroArg_forget : refinesFun. *) @@ -354,19 +354,19 @@ Hint Extern 1 (IntroArg ?n ?A ?g) => IntroArg_base_tac n A g : refinesFun. Ltac IntroArg_rewrite_bool_eq n := let e := fresh in - IntroArg_intro e; repeat rewrite e in *; - apply (IntroArg_fold n _ _ e); clear e. + IntroArg_intro e; repeat rewrite e in *; + apply (IntroArg_fold n _ _ e); clear e. Hint Extern 2 (IntroArg ?n (@eq bool _ _) _) => - progress (IntroArg_rewrite_bool_eq n) : refinesFun. + progress (IntroArg_rewrite_bool_eq n) : refinesFun. Hint Extern 4 (IntroArg SAWLet _ _) => - let e := argName SAWLet in IntroArg_intro e : refinesFun. + let e := argName SAWLet in IntroArg_intro e : refinesFun. Hint Extern 5 (IntroArg ?n (?x = ?y) _) => - let e := argName n in IntroArg_intro e; - try first [ is_var x; subst x | is_var y; subst y ] : refinesFun. + let e := argName n in IntroArg_intro e; +try first [ is_var x; subst x | is_var y; subst y ] : refinesFun. Hint Extern 6 (IntroArg ?n _ _) => - let e := argName n in IntroArg_intro e : refinesFun. + let e := argName n in IntroArg_intro e : refinesFun. Definition refinesM_sawLet_const_l {A B} (x : A) (m : CompM B) P : m |= P -> sawLet_def _ _ x (fun _ => m) |= P := fun pf => pf. @@ -375,12 +375,12 @@ Definition refinesM_sawLet_const_r {A B} (x : A) (m : CompM B) P : Definition refinesM_sawLet_bv_l_IntroArg {w B} x (m : bitvector w -> CompM B) P : (FreshIntroArg Any _ (fun a => - FreshIntroArg SAWLet (a = x) (fun _ => m a |= P))) -> + FreshIntroArg SAWLet (a = x) (fun _ => m a |= P))) -> sawLet_def _ _ x m |= P. Proof. do 3 intro; eapply H; eauto. Qed. Definition refinesM_sawLet_bv_r_IntroArg {w B} x (m : bitvector w -> CompM B) P : (FreshIntroArg Any _ (fun a => - FreshIntroArg SAWLet (a = x) (fun _ => P |= m a))) -> + FreshIntroArg SAWLet (a = x) (fun _ => P |= m a))) -> P |= sawLet_def _ _ x m. Proof. do 3 intro; eapply H; eauto. Qed. @@ -403,30 +403,30 @@ Hint Extern 1 (_ |= sawLet_def _ _ _ _ ) => refinesM_sawLet_r : refinesM. Definition refinesM_either_l_IntroArg {A B C} (f:A -> CompM C) (g:B -> CompM C) eith P : (FreshIntroArg Any _ (fun a => - FreshIntroArg Either (eith = SAWCorePrelude.Left _ _ a) (fun _ => f a |= P))) -> + FreshIntroArg Either (eith = SAWCorePrelude.Left _ _ a) (fun _ => f a |= P))) -> (FreshIntroArg Any _ (fun b => - FreshIntroArg Either (eith = SAWCorePrelude.Right _ _ b) (fun _ => g b |= P))) -> + FreshIntroArg Either (eith = SAWCorePrelude.Right _ _ b) (fun _ => g b |= P))) -> SAWCorePrelude.either _ _ _ f g eith |= P := refinesM_either_l f g eith P. Definition refinesM_either_r_IntroArg {A B C} (f:A -> CompM C) (g:B -> CompM C) eith P : (FreshIntroArg Any _ (fun a => - FreshIntroArg Either (eith = SAWCorePrelude.Left _ _ a) (fun _ => P |= f a))) -> + FreshIntroArg Either (eith = SAWCorePrelude.Left _ _ a) (fun _ => P |= f a))) -> (FreshIntroArg Any _ (fun b => - FreshIntroArg Either (eith = SAWCorePrelude.Right _ _ b) (fun _ => P |= g b))) -> + FreshIntroArg Either (eith = SAWCorePrelude.Right _ _ b) (fun _ => P |= g b))) -> P |= SAWCorePrelude.either _ _ _ f g eith := refinesM_either_r f g eith P. Hint Extern 1 (SAWCorePrelude.either _ _ _ _ _ _ |= _) => - simple apply refinesM_either_l_IntroArg : refinesM. + simple apply refinesM_either_l_IntroArg : refinesM. Hint Extern 1 (_ |= SAWCorePrelude.either _ _ _ _ _ _) => - simple apply refinesM_either_r_IntroArg : refinesM. + simple apply refinesM_either_r_IntroArg : refinesM. Definition refinesM_eithers_cons_l_IntroArg - {A B C} (f:A -> CompM C) (g:B -> CompM C) elims eith P : + {A B C} (f:A -> CompM C) (g:B -> CompM C) elims eith P : (FreshIntroArg Any _ (fun a => - FreshIntroArg Either (eith = SAWCorePrelude.Left _ _ a) (fun _ => f a |= P))) -> + FreshIntroArg Either (eith = SAWCorePrelude.Left _ _ a) (fun _ => f a |= P))) -> (FreshIntroArg Any _ (fun eith' => - FreshIntroArg Either (eith = SAWCorePrelude.Right _ _ eith') - (fun _ => SAWCorePrelude.eithers _ (SAWCorePrelude.FunsTo_Cons _ _ g elims) eith' |= P))) -> + FreshIntroArg Either (eith = SAWCorePrelude.Right _ _ eith') + (fun _ => SAWCorePrelude.eithers _ (SAWCorePrelude.FunsTo_Cons _ _ g elims) eith' |= P))) -> SAWCorePrelude.eithers (CompM C) (SAWCorePrelude.FunsTo_Cons _ _ f (SAWCorePrelude.FunsTo_Cons _ _ g elims)) @@ -435,12 +435,12 @@ Definition refinesM_eithers_cons_l_IntroArg refinesM_eithers_cons_l f g elims eith P. Definition refinesM_eithers_cons_r_IntroArg - {A B C} (f:A -> CompM C) (g:B -> CompM C) elims eith P : + {A B C} (f:A -> CompM C) (g:B -> CompM C) elims eith P : (FreshIntroArg Any _ (fun a => - FreshIntroArg Either (eith = SAWCorePrelude.Left _ _ a) (fun _ => P |= f a))) -> + FreshIntroArg Either (eith = SAWCorePrelude.Left _ _ a) (fun _ => P |= f a))) -> (FreshIntroArg Any _ (fun eith' => - FreshIntroArg Either (eith = SAWCorePrelude.Right _ _ eith') - (fun _ => P |= SAWCorePrelude.eithers _ (SAWCorePrelude.FunsTo_Cons _ _ g elims) eith'))) -> + FreshIntroArg Either (eith = SAWCorePrelude.Right _ _ eith') + (fun _ => P |= SAWCorePrelude.eithers _ (SAWCorePrelude.FunsTo_Cons _ _ g elims) eith'))) -> P |= SAWCorePrelude.eithers (CompM C) @@ -449,59 +449,59 @@ Definition refinesM_eithers_cons_r_IntroArg refinesM_eithers_cons_r f g elims eith P. Hint Extern 1 (SAWCorePrelude.eithers _ (SAWCorePrelude.FunsTo_Nil _) _ |= _) => - simple apply refinesM_eithers_nil_l : refinesM. + simple apply refinesM_eithers_nil_l : refinesM. Hint Extern 1 (_ |= SAWCorePrelude.eithers _ (SAWCorePrelude.FunsTo_Nil _) _) => - simple apply refinesM_eithers_nil_r : refinesM. + simple apply refinesM_eithers_nil_r : refinesM. Hint Extern 1 (SAWCorePrelude.eithers _ (SAWCorePrelude.FunsTo_Cons _ _ _ (SAWCorePrelude.FunsTo_Nil _)) _ |= _) => - simple apply refinesM_eithers_one_l : refinesM. + simple apply refinesM_eithers_one_l : refinesM. Hint Extern 1 (_ |= SAWCorePrelude.eithers - _ (SAWCorePrelude.FunsTo_Cons - _ _ _ (SAWCorePrelude.FunsTo_Nil _)) _) => - simple apply refinesM_eithers_one_r : refinesM. + _ (SAWCorePrelude.FunsTo_Cons + _ _ _ (SAWCorePrelude.FunsTo_Nil _)) _) => + simple apply refinesM_eithers_one_r : refinesM. Hint Extern 3 (SAWCorePrelude.eithers _ (SAWCorePrelude.FunsTo_Cons _ _ _ (SAWCorePrelude.FunsTo_Cons _ _ _ (SAWCorePrelude.FunsTo_Nil _))) _ |= _) => - simple apply refinesM_eithers_cons_l_IntroArg : refinesM. + simple apply refinesM_eithers_cons_l_IntroArg : refinesM. Hint Extern 3 (_ |= SAWCorePrelude.eithers - _ (SAWCorePrelude.FunsTo_Cons - _ _ _ (SAWCorePrelude.FunsTo_Cons - _ _ _ (SAWCorePrelude.FunsTo_Nil _))) _) => - simple apply refinesM_eithers_cons_r_IntroArg : refinesM. + _ (SAWCorePrelude.FunsTo_Cons + _ _ _ (SAWCorePrelude.FunsTo_Cons + _ _ _ (SAWCorePrelude.FunsTo_Nil _))) _) => + simple apply refinesM_eithers_cons_r_IntroArg : refinesM. Definition refinesM_maybe_l_IntroArg {A B} (x : CompM B) (f : A -> CompM B) mb P : (FreshIntroArg Maybe (mb = SAWCorePrelude.Nothing _) (fun _ => x |= P)) -> (FreshIntroArg Any _ (fun a => - FreshIntroArg Maybe (mb = SAWCorePrelude.Just _ a) (fun _ => f a |= P))) -> + FreshIntroArg Maybe (mb = SAWCorePrelude.Just _ a) (fun _ => f a |= P))) -> SAWCorePrelude.maybe _ _ x f mb |= P := refinesM_maybe_l x f mb P. Definition refinesM_maybe_r_IntroArg {A B} (x : CompM B) (f : A -> CompM B) mb P : (FreshIntroArg Maybe (mb = SAWCorePrelude.Nothing _) (fun _ => P |= x)) -> (FreshIntroArg Any _ (fun a => - FreshIntroArg Maybe (mb = SAWCorePrelude.Just _ a) (fun _ => P |= f a))) -> + FreshIntroArg Maybe (mb = SAWCorePrelude.Just _ a) (fun _ => P |= f a))) -> P |= SAWCorePrelude.maybe _ _ x f mb := refinesM_maybe_r x f mb P. Hint Extern 2 (SAWCorePrelude.maybe _ _ _ _ _ |= _) => - simple apply refinesM_maybe_l_IntroArg : refinesM. + simple apply refinesM_maybe_l_IntroArg : refinesM. Hint Extern 2 (_ |= SAWCorePrelude.maybe _ _ _ _ _) => - simple apply refinesM_maybe_r_IntroArg : refinesM. + simple apply refinesM_maybe_r_IntroArg : refinesM. Definition refinesM_sigT_rect_l_IntroArg {A1 A2 B} F P (s: {x:A1 & A2 x}) : (FreshIntroArg Any _ (fun a1 => FreshIntroArg Any _ (fun a2 => - FreshIntroArg SigT (s = existT _ a1 a2) (fun _ => F a1 a2 |= P)))) -> + FreshIntroArg SigT (s = existT _ a1 a2) (fun _ => F a1 a2 |= P)))) -> sigT_rect (fun _ => CompM B) F s |= P := refinesM_sigT_rect_l F P s. Definition refinesM_sigT_rect_r_IntroArg {A1 A2 B} F P (s: {x:A1 & A2 x}) : (FreshIntroArg Any _ (fun a1 => FreshIntroArg Any _ (fun a2 => - FreshIntroArg SigT (s = existT _ a1 a2) (fun _ => P |= F a1 a2)))) -> + FreshIntroArg SigT (s = existT _ a1 a2) (fun _ => P |= F a1 a2)))) -> P |= sigT_rect (fun _ => CompM B) F s := refinesM_sigT_rect_r F P s. Hint Extern 2 (sigT_rect (fun _ => CompM _) _ _ |= _) => - simple apply refinesM_sigT_rect_l_IntroArg : refinesM. + simple apply refinesM_sigT_rect_l_IntroArg : refinesM. Hint Extern 2 (_ |= sigT_rect (fun _ => CompM _) _ _) => - simple apply refinesM_sigT_rect_r_IntroArg : refinesM. + simple apply refinesM_sigT_rect_r_IntroArg : refinesM. Definition refinesM_if_l_IntroArg {A} (m1 m2:CompM A) b P : (FreshIntroArg If (b = true) (fun _ => m1 |= P)) -> @@ -513,14 +513,14 @@ Definition refinesM_if_r_IntroArg {A} (m1 m2:CompM A) b P : P |= (if b then m1 else m2) := refinesM_if_r m1 m2 b P. Hint Extern 2 ((if _ then _ else _) |= _) => - apply refinesM_if_l_IntroArg : refinesM. + apply refinesM_if_l_IntroArg : refinesM. Hint Extern 2 (_ |= (if _ then _ else _)) => - apply refinesM_if_r_IntroArg : refinesM. + apply refinesM_if_r_IntroArg : refinesM. Hint Extern 1 (returnM (if _ then _ else _) |= _) => - simple apply refinesM_returnM_if_l : refinesM. + simple apply refinesM_returnM_if_l : refinesM. Hint Extern 1 (_ |= returnM (if _ then _ else _)) => - simple apply refinesM_returnM_if_r : refinesM. + simple apply refinesM_returnM_if_r : refinesM. Definition refinesM_bindM_assertM_l_IntroArg {A} (P:Prop) (m1 m2: CompM A) : (FreshIntroArg Assert P (fun _ => m1 |= m2)) -> assertM P >> m1 |= m2 := @@ -530,14 +530,14 @@ Definition refinesM_assumingM_r_IntroArg {A} (P:Prop) (m1 m2: CompM A) : refinesM_assumingM_r P m1 m2. Hint Extern 1 (assertM _ >> _ |= _) => - simple eapply refinesM_bindM_assertM_l_IntroArg : refinesM. + simple eapply refinesM_bindM_assertM_l_IntroArg : refinesM. Hint Extern 1 (_ |= assumingM _ _) => - simple eapply refinesM_assumingM_r_IntroArg : refinesM. + simple eapply refinesM_assumingM_r_IntroArg : refinesM. Hint Extern 3 (_ |= assertM _ >> _) => - simple eapply refinesM_bindM_assertM_r; shelve : refinesM. + simple eapply refinesM_bindM_assertM_r; shelve : refinesM. Hint Extern 3 (assumingM _ _ |= _) => - simple eapply refinesM_assumingM_l; shelve : refinesM. + simple eapply refinesM_assumingM_l; shelve : refinesM. Definition refinesM_existsM_l_IntroArg A B (P: A -> CompM B) Q : (FreshIntroArg Exists _ (fun a => P a |= Q)) -> existsM P |= Q := @@ -547,17 +547,17 @@ Definition refinesM_forallM_r_IntroArg {A B} P (Q: A -> CompM B) : refinesM_forallM_r P Q. Hint Extern 3 (existsM _ |= _) => - simple apply refinesM_existsM_l_IntroArg : refinesM. + simple apply refinesM_existsM_l_IntroArg : refinesM. Hint Extern 3 (_ |= forallM _) => - simple apply refinesM_forallM_r_IntroArg : refinesM. + simple apply refinesM_forallM_r_IntroArg : refinesM. Hint Extern 4 (_ |= existsM _) => - simple eapply refinesM_existsM_r; shelve : refinesM. + simple eapply refinesM_existsM_r; shelve : refinesM. Hint Extern 4 (forallM _ |= _) => - simple eapply refinesM_forallM_l; shelve : refinesM. + simple eapply refinesM_forallM_l; shelve : refinesM. Hint Extern 4 (returnM _ |= returnM _) => - apply refinesM_returnM; (reflexivity || shelve) : refinesM. + apply refinesM_returnM; (reflexivity || shelve) : refinesM. Hint Extern 2 (orM _ _ |= _) => simple apply refinesM_orM_l : refinesM. Hint Extern 2 (_ |= andM _ _) => simple apply refinesM_andM_r : refinesM. @@ -643,9 +643,9 @@ Lemma refinesM_bindM_returnM_sigT_unit_r A P (m:CompM {_:A & unit}) : Proof. rewrite bindM_returnM_sigT_unit; eauto. Qed. Hint Extern 1 ((_ >>= (fun _ => returnM (existT _ (projT1 _) _))) |= _) => - simple apply refinesM_bindM_returnM_sigT_unit_l : refinesM. + simple apply refinesM_bindM_returnM_sigT_unit_l : refinesM. Hint Extern 1 (_ |= (_ >>= (fun _ => returnM (existT _ (projT1 _) _)))) => - simple apply refinesM_bindM_returnM_sigT_unit_r : refinesM. + simple apply refinesM_bindM_returnM_sigT_unit_r : refinesM. Lemma refinesM_forallM_bindM_l A B C (P: A -> CompM B) (Q: B -> CompM C) (R : CompM C) : forallM (fun a => P a >>= Q) |= R -> (forallM P) >>= Q |= R. @@ -659,7 +659,7 @@ Hint Extern 1 (((assumingM _ _) >>= _) |= _) => simple apply refinesM_assumingM_ Create HintDb refinement_proofs. Hint Extern 1 (_ _ >>= _ |= _) => - progress (try (rewrite_strat (outermost (hints refinement_proofs)))) : refinesM. + progress (try (rewrite_strat (outermost (hints refinement_proofs)))) : refinesM. Definition DidInduction {A} (a : A) : Type := unit. @@ -681,16 +681,16 @@ Ltac list_induction l l' := induction l as [| ? l']. Ltac list_simpl := simpl SAWCorePrelude.unfoldList in *; simpl list_rect in *. Hint Extern 2 (IntroArg ?n (eq (SAWCorePrelude.unfoldList _ ?l) - (SAWCorePrelude.Left _ _ _)) _) => - doDestruction (list_destruct) (list_simpl) l : refinesFun. + (SAWCorePrelude.Left _ _ _)) _) => + doDestruction (list_destruct) (list_simpl) l : refinesFun. Hint Extern 2 (IntroArg ?n (eq (SAWCorePrelude.unfoldList _ ?l) - (SAWCorePrelude.Right _ _ _)) _) => - doDestruction (list_destruct) (list_simpl) l : refinesFun. + (SAWCorePrelude.Right _ _ _)) _) => + doDestruction (list_destruct) (list_simpl) l : refinesFun. Hint Extern 9 (list_rect _ _ _ ?l |= _) => - doInduction (list_induction) (list_simpl) l : refinesM. + doInduction (list_induction) (list_simpl) l : refinesM. Hint Extern 9 (_ |= list_rect _ _ _ ?l) => - doInduction (list_induction) (list_simpl) l : refinesM. + doInduction (list_induction) (list_simpl) l : refinesM. (*** *** Rewriting rules @@ -714,7 +714,7 @@ Lemma function_eta A B (f:A -> B) : pointwise_relation A eq (fun x => f x) f. Proof. intro; reflexivity. Qed. -*) + *) (* Specialized versions of monad laws for CompM to make rewriting faster, probably because Coq doesn't have to search for the instances...? *) @@ -746,7 +746,7 @@ From Coq Require Import Nat. Lemma bvEq_eqb n x y : bvEq n (bvNat n x) (bvNat n y) = eqb x y. admit. Admitted. -*) + *) (*** @@ -768,8 +768,8 @@ Hint Extern 999 (refinesFun _ _) => shelve : refinesFun. (* Definition noDestructArg A a (goal:Prop) : goal -> MaybeDestructArg A a goal := fun g => g. *) Definition refinesFun_multiFixM_fst' lrt (F:lrtPi (LRT_Cons lrt LRT_Nil) - (lrtTupleType (LRT_Cons lrt LRT_Nil))) f - (ref_f:refinesFun (SAWCoreScaffolding.fst (F f)) f) : + (lrtTupleType (LRT_Cons lrt LRT_Nil))) f + (ref_f:refinesFun (SAWCoreScaffolding.fst (F f)) f) : refinesFun (fst (multiFixM F)) f := refinesFun_multiFixM_fst lrt F f ref_f. Definition refinesFun_fst lrt B f1 (fs:B) f2 (r:@refinesFun lrt f1 f2) : @@ -807,14 +807,14 @@ Hint Resolve refinesFun_multiFixM_fst' | 1 : refinesFun. Definition refinesFunBase B m1 m2 (r: m1 |= m2) : @refinesFun (LRT_Ret B) m1 m2 := r. Definition refinesFunStep A lrtF f1 f2 - (r: IntroArg Any _ (fun a => @refinesFun (lrtF a) (f1 a) (f2 a))) : + (r: IntroArg Any _ (fun a => @refinesFun (lrtF a) (f1 a) (f2 a))) : @refinesFun (LRT_Fun A lrtF) f1 f2 := r. Hint Extern 5 (@refinesFun (LRT_Ret _) _ _) => - simple apply refinesFunBase; unfold_projs : refinesFun. + simple apply refinesFunBase; unfold_projs : refinesFun. Hint Extern 5 (@refinesFun (LRT_Fun _ _) _ _) => - simple apply refinesFunStep : refinesFun. + simple apply refinesFunStep : refinesFun. (*** @@ -894,7 +894,7 @@ Hint Opaque letRecM : refinesM refinesFun. Ltac rewrite_refinesM := try ((rewrite returnM_bindM || rewrite bindM_returnM || rewrite bindM_bindM || rewrite errorM_bindM || rewrite existsM_bindM); rewrite_refinesM). -*) + *) (*** FIXME: old stuff below ***) @@ -916,21 +916,21 @@ Ltac old_prove_refinesM := (* either *) | |- SAWCorePrelude.either _ _ _ _ _ _ |= _ => - apply refinesM_either_l; intros; old_prove_refinesM + apply refinesM_either_l; intros; old_prove_refinesM | |- _ |= SAWCorePrelude.either _ _ _ _ _ _ => - apply refinesM_either_r; intros; old_prove_refinesM + apply refinesM_either_r; intros; old_prove_refinesM | |- sigT_rect _ _ _ |= _ => - (* sigT_rect *) - apply refinesM_sigT_rect_l; intros; old_prove_refinesM + (* sigT_rect *) + apply refinesM_sigT_rect_l; intros; old_prove_refinesM | |- _ |= sigT_rect _ _ _ => - apply refinesM_sigT_rect_r; intros; old_prove_refinesM + apply refinesM_sigT_rect_r; intros; old_prove_refinesM (* if *) | |- (if _ then _ else _) |= _ => - apply refinesM_if_l; intros; old_prove_refinesM + apply refinesM_if_l; intros; old_prove_refinesM | |- _ |= (if _ then _ else _) => - apply refinesM_if_r; intros; old_prove_refinesM + apply refinesM_if_r; intros; old_prove_refinesM (* quantifiers *) | |- existsM _ |= _ => apply refinesM_existsM_l; intros; old_prove_refinesM @@ -945,3 +945,52 @@ Ltac old_prove_refinesM := Ltac old_prove_refinesFun := apply refinesFun_multiFixM_fst; simpl; intros; old_prove_refinesM. + + +Module CompMExtraNotation. + Declare Scope fun_syntax. + + + Infix "&&" := SAWCoreScaffolding.and : fun_syntax. + Infix "<=" := (SAWCoreVectorsAsCoqVectors.bvsle _) : fun_syntax. + Notation " a

f) m) (at level 100) : fun_syntax. + Notation "'If' m 'Then' f 'Else' default " := (SAWCorePrelude.maybe _ _ default (fun _ => f) m) (at level 99) : fun_syntax. + Notation "v [ ix <- elem ]" := (SAWCorePrelude.updBVVec _ _ _ v ix elem) (at level 100) : fun_syntax. + Infix "+" := (SAWCoreVectorsAsCoqVectors.bvAdd _) : fun_syntax. + Notation "'Forall' x : T , f" := (LRT_Fun T (fun x => f)) (at level 100, format " 'Forall' x : T , '/ ' f") : fun_syntax. + Notation "T ->> f" := (LRT_Fun T (fun _ => f)) (at level 99, right associativity, format "T '/' ->> '/' f") : fun_syntax. + Notation "x" := (LRT_Ret x) (at level 99, only printing) : fun_syntax. + Notation "'Vector' T len":= (SAWCorePrelude.BVVec _ len T) (at level 98) : fun_syntax. + Notation "[[ x1 ]]":= ((LRT_Cons x1 LRT_Nil )) (at level 7, format "[[ '[' x1 ']' ]]") : fun_syntax. + Notation "[[ x1 ; x2 ; .. ; xn ]]":= ((LRT_Cons x1 (LRT_Cons x2 .. (LRT_Cons xn LRT_Nil) .. ))) + (at level 7, format "[[ '[' x1 ; '/' x2 ; '/' .. ; '/' xn ']' ]]") : fun_syntax. + Notation "[ x1 ]__lrt":= (lrtTupleType (LRT_Cons x1 LRT_Nil )) (at level 7, format "[ '[' x1 ']' ]__lrt") : fun_syntax. + Notation "[ x1 ; x2 ; .. ; xn ]__lrt":= (lrtTupleType (LRT_Cons x1 (LRT_Cons x2 .. (LRT_Cons xn LRT_Nil) .. ))) + (at level 7, format "[ '[' x1 ; '/' x2 ; '/' .. ; '/' xn ']' ]__lrt") : fun_syntax. + Notation "'int64'" := (SAWCoreVectorsAsCoqVectors.bitvector 64) (at level 97) : fun_syntax. + Notation "'int32'" := (SAWCoreVectorsAsCoqVectors.bitvector 32) (at level 97) : fun_syntax. + Notation "'bool'" := (SAWCoreVectorsAsCoqVectors.bitvector 1) (at level 97) : fun_syntax. + Notation "[ x ]__ty" := (lrtToType x) (only printing) : fun_syntax. + Notation "'LetRec' x := f 'InBody' ( body )" := + (letRecM _ (fun x => f) (fun x => body)) + (at level 0, only printing, + format "'[ ' 'LetRec' x := '//' '[' f ']' '//' 'InBody' '/' ( '[' body ']' ) ']'") : fun_syntax. + (* Visualy simplifies trivial `letRecM`*) + Notation "x" := (letRecM LRT_Nil tt x) + (at level 99, only printing) : fun_syntax. + (* Notation "[Functions: f1 := f1_body ]" := + (multiFixM (fun f1 => (f1_body, tt))) + (at level 100, only printing, format "[Functions: '//' f1 := '[' f1_body ']' ]") : fun_syntax. + Notation "[Functions: f1 := f1_body f2 := f2_body ]" := + (multiFixM (fun f1 f2 => (f1_body, f2_body, tt))) + (at level 100, only printing, + format "[Functions: '//' f1 := '[' f1_body ']' '//' f2 := '[' f2_body ']' ]") : fun_syntax. + *) + Delimit Scope fun_syntax with sytx. + +End CompMExtraNotation. From 737fbfeabce7d5a858873b7c09ae9203884cf756 Mon Sep 17 00:00:00 2001 From: santiago Date: Wed, 14 Sep 2022 15:24:49 -0400 Subject: [PATCH 19/23] Typos --- heapster-saw/doc/tutorial/tutorial.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/heapster-saw/doc/tutorial/tutorial.md b/heapster-saw/doc/tutorial/tutorial.md index 651a11f950..853a064d22 100644 --- a/heapster-saw/doc/tutorial/tutorial.md +++ b/heapster-saw/doc/tutorial/tutorial.md @@ -359,7 +359,7 @@ The process will generally involve - [1. Generating LLVM bitcode](#1-generating-llvm-bitcode) - [2. Run the SAW interpreter with Heapster](#2-run-the-saw-interpreter-with-heapster) -- [3. Load the file and extract the two function types.](#3-load-the-file-and-extract-the-two-function-types-1) +- [3. Load the file and extract the function types.](#3-load-the-file-and-extract-the-two-function-types-1) - [4. Writing heapster types for your functions](#4-writing-heapster-types-for-your-functions) - [5. Type-check your program](#5-writing-a-saw-script-to-type-check-your-code-with-respect-to-the-sepcification) - [6. Writing a Coq file to prove things about the generated functional specification(s)](#6-writing-a-coq-file-to-prove-things-about-the-generated-functional-specifications) @@ -378,7 +378,7 @@ examples directory. uint64_t add (uint64_t x, uint64_t y) { return x + y; } ``` -We will type-check the rest of the function in that file, plus some +We will type-check the rest of the functions in that file, plus some recursive functions later in the tutorial. From ca5c8c3b81c851e76521d7061a35f0541acf50ca Mon Sep 17 00:00:00 2001 From: santiago Date: Wed, 14 Sep 2022 15:38:31 -0400 Subject: [PATCH 20/23] Typos and details --- heapster-saw/doc/tutorial/tutorial.md | 38 +++++++++++++++------------ 1 file changed, 21 insertions(+), 17 deletions(-) diff --git a/heapster-saw/doc/tutorial/tutorial.md b/heapster-saw/doc/tutorial/tutorial.md index 853a064d22..df2691c45c 100644 --- a/heapster-saw/doc/tutorial/tutorial.md +++ b/heapster-saw/doc/tutorial/tutorial.md @@ -401,8 +401,9 @@ Be aware that the resulting bitcode may depend on your `clang` version and your operating system. In turn, this means the Heapster commands in your SAW script and the proofs in your Coq file may also be dependent on how and where the bitcode is generated. If you find an -incompatibility, please report it. For all other examples, the binary -code has been provided already to avoid incompatibilities. +incompatibility, please report it. For all other examples byond this +simple tuorial file, the binary code has been provided already to +avoid incompatibilities. #### 2. Run the SAW interpreter with Heapster @@ -516,7 +517,7 @@ ghost environment. Since this function doesn't require ghost variables, it is empty. The rest of the type is composed of two parts separated by the linear -implication operator `-o`, sometimes known as lollipop. The left hand +implication operator `-o`, sometimes known as "lollipop". The left hand side of the operator, refers to the state of memory before the function executes. And it says that the two arguments passed to `add`, `arg0` and `arg1`, are 64-bit integers. The predicate `int64`, which @@ -912,9 +913,8 @@ in this section are already generated for you and you can find them, together with more examples in the files `arrays.c`, `arrays.saw`, `arrays_gen.v` and `arrays_proofs.v`. -We will consider the function `zero_array` which rewrite all the -values in an array to be `0`, by looking over the length of the array -(see code in `arrays.c`). +We will consider the function `zero_array` which zero's out all the +values in an array (see code in `arrays.c`). ```C void zero_array (int64_t *arr, uint64_t len) { @@ -953,12 +953,14 @@ dynamic property which is not part of type-checking. Instead, Heapster adds dynamic checks on the extracted code which we will see in the coq code. -Let's go to `arrays_gen.v` and look for the definition of -`zero_array__tuple_fun`. You will notice that it calls `errorM` but, -in this case that's not a sign of a typing error! This error call -corresponds to the case where the array is accessed out of bounds. The -code below is a simplification of the `zero_array__tuple_fun` with -some notation for readability (see below for how to enable such pritty printing). +Let's go to `arrays_gen.v` (which has already been generatred for you) +and look for the definition of `zero_array__tuple_fun`. You will +notice that it calls `errorM` twice but, in this case that's not a +sign of a typing error! Heapster includes these errors to catch +out-of-bounds array accesses and a unrepresentable indices (i.e. index +that can't be written as a machine integer). The code below is a +simplification of the `zero_array__tuple_fun` with some notation for +readability (see below for how to enable such pritty printing). ``` zero_array__tuple_fun = @@ -990,11 +992,13 @@ zero_array__tuple_fun = ``` The arguments `e1`, `e2` and `p1` correspond to the length `len`, the -offset `i`, and the array `arr`. You can see there are several tests -done before any computation. The first two tests, which are within `if -then else`, checks that the offset is less than the array length `e2 < -e1`, and that the index `i` is within the bounds -of machine integers. +offset `i`, and the array `arr`. Notice most of that the function +performs several tests before executing any computation. The first two +tests, which are within `if then else` blocks, check that the offset +is less than the array length `e2 < e1`, and that the index `i` is +within the bounds of machine integers. The former is part of the loop +condition, the second is added by heapster to ensure the ghost +variable represents a machine integer. The last check, which is within uppercase `If Then Else` (which handles option types) is not part of the original function but From a21b98c0ecf0ea69098b702e6291c958caf816ed Mon Sep 17 00:00:00 2001 From: santiago Date: Wed, 21 Sep 2022 11:13:09 -0400 Subject: [PATCH 21/23] fix table of content --- heapster-saw/doc/tutorial/tutorial.md | 25 +++++++++++++++++-------- 1 file changed, 17 insertions(+), 8 deletions(-) diff --git a/heapster-saw/doc/tutorial/tutorial.md b/heapster-saw/doc/tutorial/tutorial.md index df2691c45c..3b61f6d4b7 100644 --- a/heapster-saw/doc/tutorial/tutorial.md +++ b/heapster-saw/doc/tutorial/tutorial.md @@ -14,6 +14,11 @@ examples to get anyone up to speed with using and hacking on Heapster. - [A quick tour of SAW](#a-quick-tour-of-saw) - [Overview](#overview) - [Running an example](#running-an-example) + - [1. Compile the code.](#1-compile-the-code) + - [2. Run the saw interpreter](#2-run-the-saw-interpreter) + - [3. Load the file and extract the two function specifications.](#3-load-the-file-and-extract-the-two-function-specifications) + - [4. Define the equality theorem.](#4-define-the-equality-theorem) + - [5. Call the SAT/SMT solver to prove the theorem.](#5-call-the-satsmt-solver-to-prove-the-theorem) - [Batch scripts](#batch-scripts) - [Using Heapster](#using-heapster) - [Heapster type-checking overview](#heapster-type-checking-overview) @@ -21,11 +26,14 @@ examples to get anyone up to speed with using and hacking on Heapster. - [Pointers](#pointers) - [Structs](#structs) - [Batch scripts](#batch-scripts-1) + - [Arrays](#arrays) - [Recursive data structures](#recursive-data-structures) - - [Looking under the hood](#looking-under-the-hood) - - [Heapster commands and environments](#heapster-commands-and-environments) - - [Permissions](#permissions) - - [Type-checking](#type-checking) + - [1. Generating LLVM bitcode](#1-generating-llvm-bitcode-1) + - [2. Run the SAW interpreter with Heapster](#2-run-the-saw-interpreter-with-heapster-1) + - [3. Load the file and extract the function types.](#3-load-the-file-and-extract-the-function-types) + - [4. Writing heapster types for your functions](#4-writing-heapster-types-for-your-functions-1) + - [Defining list permissions](#defining-list-permissions) + - [5. Type-check your program](#5-type-check-your-program-1) @@ -357,13 +365,14 @@ the resulting functional program to Coq for further verification. The process will generally involve + - [1. Generating LLVM bitcode](#1-generating-llvm-bitcode) - [2. Run the SAW interpreter with Heapster](#2-run-the-saw-interpreter-with-heapster) -- [3. Load the file and extract the function types.](#3-load-the-file-and-extract-the-two-function-types-1) +- [3. Load the file.](#3-load-the-file) - [4. Writing heapster types for your functions](#4-writing-heapster-types-for-your-functions) -- [5. Type-check your program](#5-writing-a-saw-script-to-type-check-your-code-with-respect-to-the-sepcification) -- [6. Writing a Coq file to prove things about the generated functional specification(s)](#6-writing-a-coq-file-to-prove-things-about-the-generated-functional-specifications) - +- [5. Type-check your program](#5-type-check-your-program) +- [6. Extract Coq specifications and write proofs](#6-writing-a-coq-file-to-prove-things-about-the-generated-functional-specifications) + Just like with SAW, Heapster can be processed in batch. To do so, you can combine steps 2-6 in a `.saw` file and use SAW's batch processing. From 901440898c0f7bc639fba9dd1bb0a398c6ffea7d Mon Sep 17 00:00:00 2001 From: santiago Date: Wed, 21 Sep 2022 11:14:48 -0400 Subject: [PATCH 22/23] Moving notation to it's own module. --- heapster-saw/examples/tutorial_c_proofs.v | 55 ++--------------------- 1 file changed, 3 insertions(+), 52 deletions(-) diff --git a/heapster-saw/examples/tutorial_c_proofs.v b/heapster-saw/examples/tutorial_c_proofs.v index 2e6c5be7cb..ebb55b0e8d 100644 --- a/heapster-saw/examples/tutorial_c_proofs.v +++ b/heapster-saw/examples/tutorial_c_proofs.v @@ -1,67 +1,18 @@ From CryptolToCoq Require Import SAWCoreScaffolding. From CryptolToCoq Require Import SAWCorePrelude. From CryptolToCoq Require Import CompMExtra. -Import CompMExtraNotation. (*Open Scope fun_syntax2.*) -Declare Scope fun_syntax2. - - - - - Infix "&&" := SAWCoreScaffolding.and : fun_syntax2. - Infix "<=" := (SAWCoreVectorsAsCoqVectors.bvsle _) : fun_syntax2. - Notation " a

f) m) (at level 100) : fun_syntax2. - Notation "'If' m 'Then' f 'Else' default " := (SAWCorePrelude.maybe _ _ default (fun _ => f) m) (at level 99) : fun_syntax2. - Notation "v [ ix <- elem ]" := (SAWCorePrelude.updBVVec _ _ _ v ix elem) (at level 100) : fun_syntax2. - Infix "+" := (SAWCoreVectorsAsCoqVectors.bvAdd _) : fun_syntax2. - Notation "'Forall' x : T , f" := (LRT_Fun T (fun x => f)) (at level 100, format " 'Forall' x : T , '/ ' f") : fun_syntax2. - Notation "T ->> f" := (LRT_Fun T (fun _ => f)) (at level 99, right associativity, format "T '/' ->> '/' f") : fun_syntax2. - Notation "x" := (LRT_Ret x) (at level 99, only printing) : fun_syntax2. - Notation "'Vector' T len":= (SAWCorePrelude.BVVec _ len T) (at level 98) : fun_syntax2. - Notation "[[ x1 ]]":= ((LRT_Cons x1 LRT_Nil )) (at level 7, format "[[ '[' x1 ']' ]]") : fun_syntax2. - Notation "[[ x1 ; x2 ; .. ; xn ]]":= ((LRT_Cons x1 (LRT_Cons x2 .. (LRT_Cons xn LRT_Nil) .. ))) - (at level 7, format "[[ '[' x1 ; '/' x2 ; '/' .. ; '/' xn ']' ]]") : fun_syntax2. - Notation "[ x1 ]__lrt":= (lrtTupleType (LRT_Cons x1 LRT_Nil )) (at level 7, format "[ '[' x1 ']' ]__lrt") : fun_syntax2. - Notation "[ x1 ; x2 ; .. ; xn ]__lrt":= (lrtTupleType (LRT_Cons x1 (LRT_Cons x2 .. (LRT_Cons xn LRT_Nil) .. ))) - (at level 7, format "[ '[' x1 ; '/' x2 ; '/' .. ; '/' xn ']' ]__lrt") : fun_syntax2. - Notation "'int64'" := (SAWCoreVectorsAsCoqVectors.bitvector 64) (at level 97) : fun_syntax2. - Notation "'int32'" := (SAWCoreVectorsAsCoqVectors.bitvector 32) (at level 97) : fun_syntax2. - Notation "'bool'" := (SAWCoreVectorsAsCoqVectors.bitvector 1) (at level 97) : fun_syntax2. - Notation "[ x ]__ty" := (lrtToType x) (only printing) : fun_syntax2. - Notation "'LetRec' x := f 'InBody' ( body )" := (letRecM _ (fun x => f) (fun x => body)) - (at level 0, only printing, - format "'[ ' 'LetRec' x := '//' '[' f ']' '//' 'InBody' '/' ( '[' body ']' ) ']'") : fun_syntax2. -Notation "x" := (letRecM LRT_Nil tt x) - (at level 99, only printing) : fun_syntax2. - Notation "[Functions: f1 := f1_body ]" := (multiFixM (fun f1 => (f1_body, tt))) - (at level 100, only printing, format "[Functions: '//' f1 := '[' f1_body ']' ]") : fun_syntax2. - Notation "[Functions: f1 := f1_body f2 := f2_body ]" := (multiFixM (fun f1 f2 => (f1_body, f2_body, tt))) - (at level 100, only printing, format "[Functions: '//' f1 := '[' f1_body ']' '//' f2 := '[' f2_body ']' ]") : fun_syntax2. - -Delimit Scope fun_syntax2 with sytx. +(* The following line enables pretty printing*) +Import CompMExtraNotation. Open Scope fun_syntax. Require Import Examples.tutorial_c_gen. Import tutorial_c. + Lemma no_errors_add : refinesFun add (fun _ _ => noErrorsSpec). Proof. - unfold add, add__tuple_fun. - Open Scope fun_syntax2. - (* Visually simplifies trivial letRecM*) - - - simpl. - Notation - - noErrorsSpec. - prove_refinement. Qed. From 2ce6913826d26cb258f4919fe774cd5f3ee27242 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Tue, 4 Oct 2022 16:43:34 -0700 Subject: [PATCH 23/23] Apply suggestions from code review Typo, spelling, and grammar corrections from Ryan Co-authored-by: Ryan Scott --- heapster-saw/doc/tutorial/tutorial.md | 114 +++++++++++++------------- heapster-saw/examples/tutorial_c.c | 2 +- 2 files changed, 58 insertions(+), 58 deletions(-) diff --git a/heapster-saw/doc/tutorial/tutorial.md b/heapster-saw/doc/tutorial/tutorial.md index 3b61f6d4b7..dd1113996c 100644 --- a/heapster-saw/doc/tutorial/tutorial.md +++ b/heapster-saw/doc/tutorial/tutorial.md @@ -41,7 +41,7 @@ examples to get anyone up to speed with using and hacking on Heapster. ## Building We'll start by building everything you need to use Heapster. All the -commands here are with respect to the top-level saw-script directory. +commands here are with respect to the top-level `saw-script` directory. ### Build Saw @@ -129,7 +129,7 @@ COQC sha512_gen.v ``` It might take several minutes but it should complete without any -errors. Once it's done, you know you are ready to use Heapser! +errors. Once it's done, you know you are ready to use Heapster! Before continuing, return to the top-level directory with `cd ../..`. @@ -147,8 +147,8 @@ Galois to help orchestrate and track the results of the large collection of proof tools necessary for analysis and verification of complex software artifacts. -In this tutorial we will overview how to use SAW to proof functional -equality different implementations. The steps are as follows: +In this tutorial we will overview how to use SAW to prove the functional +equality of different implementations. The steps are as follows: - [1. Compile the code.](#1-compile-the-code) - [2. Run the saw interpreter](#2-run-the-saw-interpreter) @@ -164,10 +164,10 @@ We will use the same `ffs` example used in the [SAW tutorial](https://saw.galois.com/tutorial.html). Head over to the `saw-script/doc/tutorial/code` directory to find the file. -Our aim is to prove functional equivalence of two implementatinos fo -`ffs` (there are more implementations in that file). The function is -should return the index of the first non-zero bit of it's input and -can be implemented in the follwoing two ways. +Our aim is to prove functional equivalence of two implementations of +`ffs` (there are more implementations in that file). The function +should return the index of the first non-zero bit of its input and +can be implemented in the following two ways. ```C uint32_t ffs_ref(uint32_t word) { @@ -205,8 +205,8 @@ where there is a 1. Where the options mean: * The `-g` flag instructs clang to include debugging information, which is useful in SAW to refer to variables and struct fields using the same names as in C. - * The `-c` flag asks clang to only run preprocess, compile, and assemble steps. - * `-emit-llvm` requests llvm bitecode as output. + * The `-c` flag asks clang to only run the preprocess, compile, and assemble steps. + * `-emit-llvm` requests LLVM bitcode as output. * `-o ffs.bc` tells clang to write the output into `ffs.bc` Luckily, SAW has some code to do all of this for you in the `Makefile`. You can simply run @@ -218,7 +218,7 @@ to get the same effect. #### 2. Run the saw interpreter Run `cabal run saw` to start the interpreter. You should see the SAW -logo and version number. Then you cna run your first saw command: +logo and version number. Then you can run your first saw command: ```bash sawscript> print "Hello World" @@ -238,9 +238,9 @@ logo and version number. Then you cna run your first saw command: Load an LLVM bitcode file and return a handle to it. ``` - Also, if you ever forget the name of a function, you cna find it by + Also, if you ever forget the name of a function, you can find it by running `:env` which will display the current sawscript - environment. Finally you can allways type `:help` to remember these + environment. Finally you can always type `:help` to remember these commands. Run `l <- llvm_load_module "ffs.bc"` to load the file and store it @@ -259,7 +259,7 @@ logo and version number. Then you cna run your first saw command: #### 4. Define the equality theorem. - Our theorem can now refer to the two recently created terms. since + Our theorem can now refer to the two recently created terms. Since we want to prove functional equivalence, we just state that the functions are equal for all inputs. @@ -290,7 +290,7 @@ Notice that it takes a `ProofScript`. You can look at the environment (`:env`) and look at all the proof scripts (searching for `ProofScript`), such as `abc`, `cvc4`, `mathsat`, and `z3`. If you want to play with different solvers you would have to install -them. For now, since we have `z3` installed we can call. +them. For now, since we have `z3` installed we can use it: ```bash sawscript> result <- prove z3 thm1 @@ -298,7 +298,7 @@ sawscript> print result [16:39:47.506] Valid ``` -Which tells us that z3 managed to prove the functional equality! +Which tells us that `z3` managed to prove the functional equality! ### Batch scripts @@ -410,8 +410,8 @@ Be aware that the resulting bitcode may depend on your `clang` version and your operating system. In turn, this means the Heapster commands in your SAW script and the proofs in your Coq file may also be dependent on how and where the bitcode is generated. If you find an -incompatibility, please report it. For all other examples byond this -simple tuorial file, the binary code has been provided already to +incompatibility, please report it. For all other examples beyond this +simple tutorial file, the binary code has been provided already to avoid incompatibilities. #### 2. Run the SAW interpreter with Heapster @@ -472,12 +472,12 @@ Create a new Heapster environment with the given SAW module name sawscript> ``` -As you see it takes two names. The second name referse to the bitecode -file containing the code we are verifying. The first, is the name we +As you see it takes two names. The second name refers to the bitcode +file containing the code we are verifying. The first is the name we want to give our SAW core module. That is the place where Heapster will store all our type checked functions and their extracted functional specification. By convention we use the same name as the -llvm file. +LLVM file. The function returns a Heapster environment that contains all the definitions of the module (not to be confused with the SAW environment @@ -508,14 +508,14 @@ Definitions: i64 @norm_vector(%struct.vector3d* %0) ``` -The heapster environment contains all the types, global definitions, +The Heapster environment contains all the types, global definitions, external references and functions from the loaded module. In our first example we will focus on the `add` function. #### 4. Writing heapster types for your functions -The Heapster type for the `add` function is rather simpl: +The Heapster type for the `add` function is rather simple: ``` "().arg0:int64<>, arg1:int64<> -o arg0:true, arg1:true, ret:int64<>" @@ -535,14 +535,14 @@ empty angled brackets `<>`. The right hand side describes the memory after the function executes. It says nothing about about the arguments (other than they -exists), with `true`, the predicate that is always satisfied. It also +exist), with `true`, the predicate that is always satisfied. It also says that the return value `ret` is another 64-bit integer. Notice, in particular, that the type does not assert that the return value is the sum of the inputs. That's because Hepaster is not a -correcness logic. It is a memory safety type system. However, as you +correctness logic. It is a memory safety type system. However, as you will shortly see, after checking for memory safety, we can extract -`add` as a functional program and verify it's correctness in Coq. +`add` as a functional program and verify its correctness in Coq. ##### Defining permission predicates @@ -554,7 +554,7 @@ exists x:bv 64.eq(llvmword(x)) ``` It says that there exist some bit-vector of length 64 (`bv 64`) which -is equal, as an llvm word, to the "current variable". In other words, +is equal, as an LLVM word, to the "current variable". In other words, it says that the current variable is equal to some number that can be described as a bit-vector of size 64. @@ -590,7 +590,7 @@ heapster_typecheck_fun env "add" "().arg0:int64<>, arg1:int64<> -o arg0:true, ar ``` The `heapster_typecheck_fun` command takes the environment, the name -of the function to typecheck and its permision type. The command then +of the function to typecheck and its permission type. The command then attempts to typecheck the function and extracts its functional specification. The functional specification is then added to the SAW core module `tutorial_c` with the sufix `__tuple_fun`, in this case @@ -598,7 +598,7 @@ core module `tutorial_c` with the sufix `__tuple_fun`, in this case The function `add_mistyped`, in the same `tutorial_bc` and already loaded in the Heapster environment, is identical to `add` so we can -experiment with misstyping. Try running the following command +experiment with mistyping. Try running the following command ``` heapster_typecheck_fun env "add_mistyped" "().arg0:true, arg1:int64<> -o arg0:true, arg1:true, ret:int64<>" @@ -628,7 +628,7 @@ heapster_export_coq env "tutorial_c_gen.v"; ``` Open up the new `tutorial_c_gen.v` file in your examples -directory. You should see a handfull of auto-generated imports and four +directory. You should see a handful of auto-generated imports and four definitions. The first two definitions `add__tuple_fun` and `add` might have a @@ -642,7 +642,7 @@ add : bitvector 64 -> bitvector 64 -> CompM (bitvector 64) That is, `add__tuple_fun` if a list of definitions, encoded as a tuple. Saw uses these heterogeneous lists to encode functions, or parts of them, that depend on each other. In this case, there is only -the function `add` function and a unit `()`, representing the end of +the `add` function and a unit `()`, representing the end of the list (similar to `nil`). The `add` function takes two integers (as 64-bit vectors) and returns another one (under the `CompM` monoid that accepts failure). @@ -698,10 +698,10 @@ Import tutorial_c. It first imports all the SAW functionality we need and enables pretty printing. Then it imports our new definitions (e.g. `add`). -Our first proof, will claim that the function `add`, produces no -errors. Morr specifically, it says that for all inputs (that's what -`refinesFun` quantifies) `add` allways refines to `noErrorsSpec`, that -is it returns a pure value. +Our first proof will claim that the function `add` produces no +errors. More specifically, it says that for all inputs (that's what +`refinesFun` quantifies) `add` always refines to `noErrorsSpec`. That +is, it returns a pure value. ``` Lemma no_errors_add @@ -759,7 +759,7 @@ The type for this function should be (). arg0:ptr((W,0) |-> int64<>) -o arg0:ptr((W,0) |-> int64<>) ``` -As before, the ghost environment is ommited and both sides of the +As before, the ghost environment is omitted and both sides of the implication are identical, since the function doesn't change the shape of memory. The return value is `void`, so we can omit it or add a trivial `ret:true`. @@ -767,7 +767,7 @@ trivial `ret:true`. The permission for pointers `ptr` takes three arguments. First, it describes the read-write modality. In this case the pointer is writable `W`, since it will be modified. The second -argument describes the pointer offset, here `0`. Finaly, the third +argument describes the pointer offset, here `0`. Finally, the third argument describes the content of the pointer, in this case a 64-bit integer `int64<>`. @@ -784,7 +784,7 @@ heapster_export_coq env "tutorial_c_gen.v"; ``` The old file should be overwritten and now contains the functional -specification of `add`, `add_misstyped` and `incr_ptr`. As you can see +specification of `add`, `add_mistyped` and `incr_ptr`. As you can see the definition of `incr_ptr__tuple_fun` has no references to `errorM`, so we know it was correctly type checked. @@ -808,7 +808,7 @@ example, we defined a function that can compute the norm of a 3D vector ``` C -// Struct that represents the three coordinates fora 3D vector +// Struct that represents the three coordinates for a 3D vector typedef struct { uint64_t x; uint64_t y; uint64_t z; } vector3d; // function that computes the norm of a 3D vector @@ -916,13 +916,13 @@ Up to date ### Arrays -We will briefly explore arrays, which have slightly more intersting +We will briefly explore arrays, which have slightly more interesting memory restrictions. Namely, array access must be in bounds. The code in this section are already generated for you and you can find them, together with more examples in the files `arrays.c`, `arrays.saw`, `arrays_gen.v` and `arrays_proofs.v`. -We will consider the function `zero_array` which zero's out all the +We will consider the function `zero_array` which zeroes out all the values in an array (see code in `arrays.c`). ```C @@ -936,7 +936,7 @@ void zero_array (int64_t *arr, uint64_t len) { The type for this function is relatively simple, it only assumes that `len` is actually the length for the given array `arr`. This is achieved by used a shared or ghost variable `len` which is both the -lenght of the array and equal to the second argument (see the code in `arrays.saw`) +length of the array and equal to the second argument (see the code in `arrays.saw`) ``` heapster_typecheck_fun env "zero_array" @@ -947,7 +947,7 @@ heapster_typecheck_fun env "zero_array" Heapster also expects a loop invariant hint for every loop. Loop invariants look just like function types, taking the loop variables as arguments. In this case the loop introduces a new variable `i` which -is the ofset into the array. We represent that with a new ghost +is the offset into the array. We represent that with a new ghost variable ``` @@ -959,14 +959,14 @@ heapster_typecheck_fun env "zero_array_from" Certainly function correctness must ensure that all the writes to the array (i.e. `arr[i] = 0`) happen within bounds. However this is a dynamic property which is not part of type-checking. Instead, Heapster -adds dynamic checks on the extracted code which we will see in the coq +adds dynamic checks on the extracted code which we will see in the Coq code. -Let's go to `arrays_gen.v` (which has already been generatred for you) +Let's go to `arrays_gen.v` (which has already been generated for you) and look for the definition of `zero_array__tuple_fun`. You will notice that it calls `errorM` twice but, in this case that's not a sign of a typing error! Heapster includes these errors to catch -out-of-bounds array accesses and a unrepresentable indices (i.e. index +out-of-bounds array accesses and unrepresentable indices (i.e. index that can't be written as a machine integer). The code below is a simplification of the `zero_array__tuple_fun` with some notation for readability (see below for how to enable such pritty printing). @@ -1006,7 +1006,7 @@ performs several tests before executing any computation. The first two tests, which are within `if then else` blocks, check that the offset is less than the array length `e2 < e1`, and that the index `i` is within the bounds of machine integers. The former is part of the loop -condition, the second is added by heapster to ensure the ghost +condition, the second is added by Heapster to ensure the ghost variable represents a machine integer. The last check, which is within uppercase `If Then Else` (which @@ -1016,15 +1016,15 @@ inserted by Heapster. It checks that the array access is within bounds access being safe. If the check fails, the function reports a runtime error `errorM "ghost_bv heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq( but we need a new predicate for lists. Before we look at the definition of a `List64` lets focus on its permission type. First of all, `List64` takes a single argument `rw:rwmodality` which -determines if the list is readable or writable, jus like 3D +determines if the list is readable or writable, just like 3D vectors. It's type should look something like this ``` ["eq(llvmword(0))", "ptr((rw,0) |-> int64<>) * ptr((rw,8) |-> List64)"] ``` -the definition shows the diferent cases for a list, separated by a -coma. In the first case, a `List64` can be a null pointer, expressed +The definition shows the diferent cases for a list, separated by a +comma. In the first case, a `List64` can be a null pointer, expressed with the type `eq(llvmword(0))`. In the second case, a list is a -pointer where offset `0` is the head, an `Int64`, and offset `8` it's +pointer where offset `0` is the head, an `Int64`, and offset `8` is the tail, is recursively a `List64`. In the later case, both elements are tagged with `rw`, describing if they are readable or writable, as determined by the argument to `List64`. To define [permissions](doc/Permissions.md) which can describe unbounded data structures, you can use the -`heapster_define_recursive_perm` command. here is how to use the +`heapster_define_recursive_perm` command. Here is how to use the command to define lists. ``` @@ -1229,7 +1229,7 @@ heapster_define_recursive_perm Its first four arguments are the same as for `heapster_define_perm`, namely the environment, the name, the arguments and the type of value -that the permission applies to. The fifth argument is its permision +that the permission applies to. The fifth argument is its permission type. The final three arguments are its translation into SAW core. As you might remember, this is the `List_def` we defined in our SAW core file which is now loaded in the module. The other two `foldList` and diff --git a/heapster-saw/examples/tutorial_c.c b/heapster-saw/examples/tutorial_c.c index 8d736f0c8d..02e4f6d750 100644 --- a/heapster-saw/examples/tutorial_c.c +++ b/heapster-saw/examples/tutorial_c.c @@ -9,7 +9,7 @@ uint64_t add_mistyped (uint64_t x, uint64_t y) { return x + y; } // Simple function that increments the value in a pointer void incr_ptr (uint64_t *x) { *x += 1; } -// Struct that represents the three coordinates fora 3D vector +// Struct that represents the three coordinates for a 3D vector typedef struct { uint64_t x; uint64_t y; uint64_t z; } vector3d; // function that computes the norm of a 3D vector