Strongest Postcondition

examples/memory/memory_interproc.il

@@ -0,0 +1,40 @@
+memory shared $mem : (bv64 -> bv8);
+memory $stack : (bv64 -> bv8);
+
+prog entry @main;
+
+proc @malloc(R0_in:bv64) -> (R0_out:bv64);
+proc @free(R0_in:bv64) -> ();
+
+// In future, realloc should actually copy the byte accross.
+// For now that is ommitted from this test as the store expression
+// locks up the interprocedural redundancy check forever.
+proc @realloc(ptr_in:bv64) -> (ptr_out:bv64)
+[
+    block %realloc [
+        // var x:bv8 := load le $mem ptr_in 8;
+        call @free(ptr_in);
+        var size: bv64 := 1:bv64;
+        var (ptr_out:bv64) := call @malloc(size);
+        // store le $mem ptr_out x 8;
+        goto(%realloc_return);
+    ];
+    block %realloc_return [
+        return;
+    ];
+];
+
+proc @main () -> ()
+[
+    block %main_entry [
+        var size: bv64 := 1:bv64;
+        var (addr:bv64) := call @malloc(size);
+        var (addr_2:bv64) := call @realloc(addr);
+        goto(%main_return);
+    ];
+    block %main_return [
+        assert neq(addr, addr_2);
+        call @free(addr_2);
+        return;
+    ];
+];

examples/memory/memory_safety.il

@@ -0,0 +1,121 @@
+memory shared $mem : (bv64 -> bv8);
+memory $stack : (bv64 -> bv8);
+
+prog entry @main;
+
+// Unspecified malloc/free procedures. Specified by
+// memory specification + encoding transform.
+proc @malloc(R0_in:bv64) -> (R0_out:bv64);
+proc @free(R0_in:bv64) -> ();
+
+// Valid memory operations. Allocates 2 bytes,
+// stores/loads to the allocated space, and frees.
+proc @main () -> () { .entrypoint=true; }
+[
+    block %main_entry [
+        var size:bv64 := 2:bv64;
+        var (addr:bv64) := call @malloc(size);
+
+        store le $mem bvadd(addr,0:bv64) 0xff:bv8 8;
+        var temp:bv8 := load le $mem bvadd(addr,0:bv64) 8;
+
+        call @free(addr);
+
+        goto(%main_return);
+    ];
+    block %main_return [
+        return ();
+    ];
+];
+
+// Double free example. Calls free on address twice.
+proc @double_free () -> () { .entrypoint=true; }
+[
+    block %main_entry [
+        var size:bv64 := 2:bv64;
+        var (addr:bv64) := call @malloc(size);
+
+        store le $mem bvadd(addr,0:bv64) 0xff:bv8 8;
+        var temp:bv8 := load le $mem bvadd(addr,0:bv64) 8;
+
+        call @free(addr);
+        call @free(addr);
+
+        goto(%main_return);
+    ];
+    block %main_return [
+        return ();
+    ];
+];
+
+// Example of freeing a valid address which is not at the
+// base of an allocation.
+proc @invalid_free () -> () { .entrypoint=true; }
+[
+    block %main_entry [
+        var size:bv64 := 2:bv64;
+        var (addr:bv64) := call @malloc(size);
+
+        call @free(bvadd(addr,1:bv64));
+
+        goto(%main_return);
+    ];
+    block %main_return [
+        return ();
+    ];
+];
+
+// Example of loading memory after free.
+proc @use_after_free () -> () { .entrypoint=true; }
+[
+    block %main_entry [
+        var size:bv64 := 2:bv64;
+        var (addr:bv64) := call @malloc(size);
+
+        store le $mem bvadd(addr,0:bv64) 0xff:bv8 8;
+        call @free(addr);
+        var temp:bv8 := load le $mem bvadd(addr,0:bv64) 8;
+
+        goto(%main_return);
+    ];
+    block %main_return [
+        return ();
+    ];
+];
+
+// Example reading at offset 4 of a 2 byte allocation.
+proc @out_of_bounds () -> () { .entrypoint=true; }
+[
+    block %main_entry [
+        var size:bv64 := 2:bv64;
+        var (addr:bv64) := call @malloc(size);
+
+        store le $mem bvadd(addr,4:bv64) 0xff:bv8 8;
+        var temp:bv8 := load le $mem bvadd(addr,4:bv64) 8;
+
+        call @free(addr);
+
+        goto(%main_return);
+    ];
+    block %main_return [
+        return ();
+    ];
+];
+
+// Example of catching a memory leak (unfreed addr).
+proc @memory_leak () -> () { .entrypoint=true; }
+[
+    block %main_entry [
+        var size:bv64 := 2:bv64;
+        var (addr:bv64) := call @malloc(size);
+
+        store le $mem bvadd(addr,0:bv64) 0xff:bv8 8;
+        var temp:bv8 := load le $mem bvadd(addr,0:bv64) 8;
+
+        goto(%main_return);
+    ];
+    block %main_return [
+        return ();
+    ];
+];
+

flake.nix

@@ -90,8 +90,14 @@
 
           devShells = {
             default = self.devShells.fp;
-            fp = fpOcamlPackages.callPackage ./nix/shell.nix { inherit bnfc-treesitter; };
-            no-fp = selfOcamlPackages.callPackage ./nix/shell.nix { inherit bnfc-treesitter; };
+            fp = fpOcamlPackages.callPackage ./nix/shell.nix {
+              inherit bnfc-treesitter;
+              z3 = pkgs.z3.out;
+            };
+            no-fp = selfOcamlPackages.callPackage ./nix/shell.nix {
+              inherit bnfc-treesitter;
+              z3 = pkgs.z3.out;
+            };
           };
         };
     };

lib/analysis/dataflow_graph.ml

@@ -540,7 +540,7 @@ struct
 
     include SV
 
-    let init p =
+    let init ?(vertex = None) p =
       let vs = Lang.Procedure.formal_in_params p |> StringMap.values in
       vs
       |> Iter.map (fun v -> (v, top_val))

lib/analysis/dune

@@ -18,6 +18,7 @@
   tnum_wint_reduced_product
   known_bits
   wp_dual
+  sp
   sva)
  (libraries
   intPQueue

lib/analysis/gamma_domain.ml

@@ -22,7 +22,7 @@ module Domain = struct
 
   let name = "Gamma domain"
 
-  let init proc =
+  let init ?(vertex = None) proc =
     Procedure.formal_in_params proc
     |> StringMap.values
     |> Iter.append

lib/analysis/intra_analysis.ml

@@ -169,7 +169,7 @@ module Forwards (D : IntraDomain) = struct
         Procedure.graph p
         |> Option.map (fun g ->
             A.recurse g (Procedure.topo_fwd p)
-              (fun v -> D.init p)
+              (fun v -> D.init ~vertex:(Some v) p)
               widening_set widening_delay))
     |> Option.get_or ~default:A.M.empty
 

lib/analysis/known_bits.ml

@@ -274,7 +274,7 @@ module Domain = struct
 
   include StateAbstraction
 
-  let init p =
+  let init ?(vertex = None) p =
     let vs = Lang.Procedure.formal_in_params p |> StringMap.values in
     vs
     |> Iter.map (fun v -> (v, top_val))

lib/analysis/lattice_types.ml

@@ -85,15 +85,15 @@ end
 module type StateDomain = sig
   include StateAbstraction
 
-  val init : Program.proc -> t
+  val init : ?vertex:Procedure.Vert.t Option.t -> Program.proc -> t
   val transfer_state : (Var.t -> V.t) -> Program.stmt -> (Var.t * V.t) Iter.t
 end
 
 module type Domain = sig
   include Lattice
 
   val transfer : t -> Program.stmt -> t
-  val init : Program.proc -> t
+  val init : ?vertex:Procedure.Vert.t Option.t -> Program.proc -> t
 end
 
 module FlatLattice (L : sig