minimal proc SMT extraction

lib/analysis/irreducible_loops.ml

@@ -459,13 +459,12 @@ module ProcIntra = struct
 
     let find_edge p src dest : edge =
       let open Option in
-      Procedure.blocks_succ p src |> Iter.find_pred (fst %> ID.equal dest)
-      |> function
+      Procedure.blocks_succ p src |> Iter.find_pred (ID.equal dest) |> function
       | Some _ -> (src, dest)
       | _ -> raise Not_found
 
-    let succ p v = Procedure.blocks_succ p v |> Iter.map fst |> Iter.to_list
-    let pred p v = Procedure.blocks_pred p v |> Iter.map fst |> Iter.to_list
+    let succ p v = Procedure.blocks_succ p v |> Iter.to_list
+    let pred p v = Procedure.blocks_pred p v |> Iter.to_list
   end
 
   include Make (BlockGraph)

lib/lang/dune

@@ -14,6 +14,7 @@
   block
   procedure
   interp
+  reduction
   program)
  (flags -w -27) ; unused var
  (libraries

lib/lang/expr_smt.ml

@@ -88,6 +88,35 @@ module SMTLib2 = struct
 
   let run (e : 'e t) = e empty
 
+  let smt_norm_rewriter e =
+    let open AbstractExpr in
+    let open BasilExpr in
+    let open Bitvec in
+    let e = AbstractExpr.map fst e in
+    match e with
+    | ApplyIntrin { op = `AND; args = [] } ->
+        replace [%here] @@ BasilExpr.boolconst true
+    | ApplyIntrin { op = `OR; args = [] } ->
+        replace [%here] @@ BasilExpr.boolconst false
+    | ApplyIntrin { op = `Cases; args } -> (
+        match List.rev args with
+        | [ a ] -> replace [%here] (BasilExpr.fix a)
+        | h :: tl ->
+            replace [%here]
+              (List.fold_left
+                 (fun acc b ->
+                   match b with
+                   | BinaryExpr { op = `IfThen; arg1; arg2 } ->
+                       BasilExpr.ifthenelse arg1 arg2 acc
+                   | o ->
+                       (* all other functions are total*)
+                       fix o)
+                 (BasilExpr.fix h) tl)
+        | _ -> Keep)
+    | _ -> Keep
+
+  let norm_expr e = BasilExpr.rewrite_typed_two smt_norm_rewriter e
+
   let extract s =
     let* b = get s in
     return @@ to_sexp b
@@ -174,6 +203,7 @@ module SMTLib2 = struct
     | `BoolNOT -> atom "not"
     | `NEQ -> failwith "undef"
     | `AND -> atom "and"
+    | `IMPLIES -> atom "=>"
     | `OR -> atom "or"
     | #Ops.AllOps.unary as o -> atom @@ Ops.AllOps.to_string o
     | #Ops.AllOps.const as o -> atom @@ Ops.AllOps.to_string o
@@ -250,6 +280,16 @@ module SMTLib2 = struct
         let* l = l in
         let* r = r in
         return @@ list [ of_op o; l; r ]
+    | ApplyIntrin { op = `Cases; args } ->
+        let* args = sequence args in
+        let cond, thn, els =
+          match args with
+          | [ condition; `List [ `Atom "case"; arg ]; els ] ->
+              (condition, arg, els)
+          | _ -> failwith "unsupp cases"
+        in
+        return @@ Bincaml_util.Smt.Expr.ite cond thn els
+    (* TODO: bool2bv1 *)
     | ApplyIntrin { op = o; args } ->
         let* args = sequence args in
         return (list (of_op o :: args))
@@ -259,8 +299,13 @@ module SMTLib2 = struct
         let* func = func in
         return @@ list (func :: args)
 
-  let of_bexpr e = fst @@ (BasilExpr.cata smt_alg e) empty
-  let bind_of_bexpr e b = BasilExpr.cata smt_alg e b
+  let of_bexpr e =
+    let e = norm_expr e in
+    fst @@ (BasilExpr.cata smt_alg e) empty
+
+  let bind_of_bexpr e b =
+    let e = norm_expr e in
+    BasilExpr.cata smt_alg e b
 
   let trans_decl (decl : Program.declaration) =
     let* x = return () in
@@ -304,7 +349,7 @@ module SMTLib2 = struct
     | Variable v -> failwith "mutable"
 
   let assert_bexpr e =
-    let* s = BasilExpr.cata smt_alg e in
+    let* s = bind_of_bexpr e in
     add_assert s
 
   let push = add_command (list [ atom "push" ])

lib/lang/procedure.ml

@@ -274,7 +274,7 @@ end
 
 include PG
 
-let add_goto p ~(from : ID.t) ~(targets : ID.t list) =
+let add_goto ~(from : ID.t) ~(targets : ID.t list) p =
   let open Vert in
   p
   |> map_graph (fun g ->
@@ -338,6 +338,17 @@ let get_entry_block p =
         Some (List.hd id))
   with Not_found -> None
 
+let get_returning_blocks p =
+  let open Edge in
+  let open G in
+  graph p |> Option.to_list
+  |> List.flat_map (fun g ->
+      G.pred g Return
+      |> List.filter_map (function
+        | Vert.Begin id -> Some id
+        | End id -> Some id
+        | _ -> None))
+
 (** Get the block for an id
 
     @raise Not_found when the block does not exist. *)
@@ -513,23 +524,19 @@ let blocks_succ p i =
   |> Iter.flat_map (fun graph ->
       Iter.from_iter (fun f -> G.iter_succ f graph (End i))
       |> Iter.flat_map (function
-        | Vert.Begin i ->
-            Iter.singleton
-              (i, get_block p i |> Option.get_exn_or "bad cfg sturcture")
+        | Vert.Begin i -> Iter.singleton i
         | Return -> Iter.empty
         | Exit -> Iter.empty
-        | v -> failwith @@ "bad graph structure " ^ Vert.show v))
+        | v -> Iter.empty))
 
 let blocks_pred p i =
   Option.to_iter (graph p)
   |> Iter.flat_map (fun graph ->
       Iter.from_iter (fun f -> G.iter_pred f graph (Begin i))
       |> Iter.flat_map (function
-        | Vert.End i ->
-            Iter.singleton
-              (i, get_block p i |> Option.get_exn_or "bad cfg sturcture")
+        | Vert.End i -> Iter.singleton i
         | Entry -> Iter.empty
-        | v -> failwith @@ "bad graph structure  " ^ Vert.show v))
+        | v -> Iter.empty))
 
 let iter_blocks_topo_fwd p =
   Iter.from_iter (fun f -> fold_blocks_topo_fwd (fun acc a b -> f (a, b)) () p)

lib/passes.ml

@@ -133,7 +133,7 @@ module PassManager = struct
   let sssa =
     {
       name = "simple-ssa";
-      apply = Proc Transforms.Ssa.ssa;
+      apply = Proc (Transforms.Ssa.ssa %> snd);
       doc =
         "Naive SSA transform assuming all variable uses are dominated by \
          definitions from parameters";
@@ -153,6 +153,13 @@ module PassManager = struct
       doc = "Remove blocks unreachable from entry";
     }
 
+  let verify_smt =
+    {
+      name = "verify-procs-smt";
+      apply = Prog Transforms.Verif_smt.check;
+      doc = "Simple smt verification";
+    }
+
   let full_ssa =
     {
       name = "ssa";
@@ -189,7 +196,7 @@ module PassManager = struct
       apply = Prog Transforms.Memory_specification.transform;
       doc = "Specifies programs for memory safety";
     }
-  
+
   let intra_function_summaries =
     {
       name = "intra-function-summaries";
@@ -230,6 +237,7 @@ module PassManager = struct
       read_uninit true;
       sssa;
       full_ssa;
+      verify_smt;
       type_check;
       split_memory_encoding;
       memory_specification;
@@ -275,9 +283,9 @@ module PassManager = struct
         doc = "Replaces captured global variables with explicit parameters";
       };
       {
-          name = "gamma-vars";
-          apply = Prog Transforms.Gamma_vars.transform;
-          doc = "Replace gamma expressions with gamma variables";
+        name = "gamma-vars";
+        apply = Prog Transforms.Gamma_vars.transform;
+        doc = "Replace gamma expressions with gamma variables";
       };
     ]
 

lib/transforms/dune

@@ -14,7 +14,8 @@
   memory_specification
   function_summaries
   boogie_prepass
-  gamma_vars)
+  gamma_vars
+  verif_smt)
  (libraries
   bincaml.analysis
   patricia-tree

lib/transforms/ssa.ml

@@ -433,7 +433,11 @@ let set_params ?(skip_observable = true) ?(skip_maps = true) (p : Program.t) =
   in
   { p with procs; globals }
 
-let ssa ?(skip_observable = true) ?(skip_maps = true) (in_proc : Program.proc) =
+let ssa ?blocks ?(skip_observable = true) ?(skip_maps = true)
+    (in_proc : Program.proc) =
+  let blocks =
+    Option.get_or ~default:(Procedure.iter_blocks_topo_fwd in_proc)
+  in
   let in_proc = intro_ssi_assigns in_proc in
   let lives = Livevars.run in_proc in
   let rename r v : Var.t =
@@ -537,10 +541,10 @@ let ssa ?(skip_observable = true) ?(skip_maps = true) (in_proc : Program.proc) =
       | [] ->
           Hashtbl.add phis block_id VarMap.empty;
           (VarMap.empty, [])
-      | [ (id, _) ] -> (Hashtbl.find st id, [])
+      | [ id ] -> (Hashtbl.find st id, [])
       | inc ->
           let joined_phis =
-            List.map (fun (id, _) -> (id, get_st_pred id)) inc
+            List.map (fun id -> (id, get_st_pred id)) inc
             |> List.fold_left
                  (fun phim (block, rn) ->
                    let rn =
@@ -578,15 +582,15 @@ let ssa ?(skip_observable = true) ?(skip_maps = true) (in_proc : Program.proc) =
     let renames = Hashtbl.find st block_id in
     if IDSet.mem block_id !delayed_phis then
       Procedure.blocks_succ proc block_id
-      |> Iter.filter (fun (bid, _) ->
+      |> Iter.filter (fun bid ->
           let pred =
             Procedure.G.pred
               (Option.get_exn_or "unreachable" @@ Procedure.graph proc)
               (Begin bid)
           in
           List.length pred > 1)
       |> Iter.fold
-           (fun proc (succ_bid, _) ->
+           (fun proc succ_bid ->
              let eblock =
                Procedure.get_block proc succ_bid
                |> Option.get_exn_or "block not exist"
@@ -627,9 +631,7 @@ let ssa ?(skip_observable = true) ?(skip_maps = true) (in_proc : Program.proc) =
   in
   let proc = IDSet.fold fixup_delayed !delayed_phis proc in
   let check_bl (block_id, (block : Program.bloc)) =
-    let pred =
-      Procedure.blocks_pred proc block_id |> Iter.map (fun (i, _) -> i)
-    in
+    let pred = Procedure.blocks_pred proc block_id |> Iter.map (fun i -> i) in
     let npred = Iter.length pred in
     block.phis
     |> List.map (fun (p : Var.t Block.phi) ->
@@ -643,7 +645,7 @@ let ssa ?(skip_observable = true) ?(skip_maps = true) (in_proc : Program.proc) =
   in
   assert (Procedure.iter_blocks_topo_fwd proc |> Iter.for_all check_bl);
   check_ssa ~skip_observable ~skip_maps proc;
-  proc
+  (st, proc)
 
 let ssa_prog ?(skip_observable = true) ?(skip_maps = true) (p : Program.t) =
-  { p with procs = IDMap.map (ssa ~skip_observable ~skip_maps) p.procs }
+  { p with procs = IDMap.map (ssa ~skip_observable ~skip_maps %> snd) p.procs }