Refactored GPS

.gitignore

@@ -1,3 +1,4 @@
+*.install
 *.annot
 *.cmo
 *.cma

Makefile

@@ -3,13 +3,13 @@
 all: build
 
 build:
-	dune build duet
+	dune build duet 
 
 clean:
 	dune clean
 
 test:
-	dune runtest -f
+	dune runtest --profile release -f
 
 install:
 	dune build @install

duet/cmdLine.ml

@@ -27,6 +27,11 @@ let verbose_arg =
    Arg.String (fun v -> Log.set_verbosity_level v `info),
    " Raise verbosity for a particular module")
 
+let trace_arg =
+  ("-trace",
+   Arg.String (fun v -> Log.set_verbosity_level v `trace),
+   " Set verbosity for a particular module to trace")
+
 let verbose_list_arg =
   ("-verbose-list",
    Arg.Unit (fun () ->
@@ -36,7 +41,7 @@ let verbose_list_arg =
          ) Log.loggers;
        exit 0;
      ),
-   " List modules which can be used with -verbose")
+   " List modules which can be used with -verbose/-trace")
 
 let stats_arg =
   ("-stats", Arg.Set show_stats, " Display statistics")
@@ -113,6 +118,7 @@ let debug_args = ref
 let config_args = ref
     [
       verbose_arg;
+      trace_arg;
       verbose_list_arg;
       verbosity_arg;
       stats_arg;

duet/cra.ml

@@ -90,45 +90,79 @@ let map_value f = function
   | VPos v -> VPos (f v)
   | VWidth v -> VWidth (f v)
 
-module V = struct
-  module I = struct
-    type t = value [@@deriving ord]
-    let pp formatter = function
-      | VVal v -> Var.pp formatter v
-      | VWidth v -> Format.fprintf formatter "%a@@width" Var.pp v
-      | VPos v -> Format.fprintf formatter "%a@@pos" Var.pp v
-    let show = SrkUtil.mk_show pp
-    let equal x y = compare x y = 0
-    let hash = function
-      | VVal v -> Hashtbl.hash (Var.hash v, 0)
-      | VPos v -> Hashtbl.hash (Var.hash v, 1)
-      | VWidth v -> Hashtbl.hash (Var.hash v, 2)
-  end
-  include I
-
-  let sym_to_var = Hashtbl.create 991
-  let var_to_sym = ValueHT.create 991
-
-  let typ v = tr_typ (Var.get_type (var_of_value v))
-
-  let symbol_of var =
-    if ValueHT.mem var_to_sym var then
-      ValueHT.find var_to_sym var
-    else begin
-      let sym = Ctx.mk_symbol ~name:(show var) (typ var) in
-      ValueHT.add var_to_sym var sym;
-      Hashtbl.add sym_to_var sym var;
-      sym
+  module V = struct
+    module I = struct
+      type t = value [@@deriving ord]
+      let pp formatter = function
+        | VVal v -> Var.pp formatter v
+        | VWidth v -> Format.fprintf formatter "%a@@width" Var.pp v
+        | VPos v -> Format.fprintf formatter "%a@@pos" Var.pp v
+      let show = SrkUtil.mk_show pp
+      let equal x y = compare x y = 0
+      let hash = function
+        | VVal v -> Hashtbl.hash (Var.hash v, 0)
+        | VPos v -> Hashtbl.hash (Var.hash v, 1)
+        | VWidth v -> Hashtbl.hash (Var.hash v, 2)
     end
-
-  let of_symbol sym =
-    if Hashtbl.mem sym_to_var sym then
-      Some (Hashtbl.find sym_to_var sym)
-    else
-      None
-
-  let is_global = Var.is_global % var_of_value
-end
+    include I
+
+
+
+    let sym_to_var = Hashtbl.create 991
+    let var_to_sym = ValueHT.create 991
+    let prophecy_vars = ValueHT.create 991 (* var -> var mapping *)
+    let var_of_prophecy_vars = ValueHT.create 991 (* reverse mapping of prophecy_vars *)
+
+    let typ v = tr_typ (Var.get_type (var_of_value v))
+
+    let symbol_of var =
+      if ValueHT.mem var_to_sym var then
+        ValueHT.find var_to_sym var
+      else begin
+        let sym = Ctx.mk_symbol ~name:(show var) (typ var) in
+        ValueHT.add var_to_sym var sym;
+        Hashtbl.add sym_to_var sym var;
+        sym
+      end
+
+    let of_symbol sym =
+      if Hashtbl.mem sym_to_var sym then
+        Some (Hashtbl.find sym_to_var sym)
+      else
+        None
+
+    let is_global = Var.is_global % var_of_value
+
+    let make_var sym is_global =
+      let v = 
+        begin match is_global with 
+        | true ->  
+          Varinfo.mk_global (Syntax.show_symbol srk sym) (Concrete (Int 8)) 
+        | false -> 
+          Varinfo.mk_local (Syntax.show_symbol srk sym) (Concrete (Int 8))
+        end |> Var.mk 
+        in 
+      Hashtbl.add sym_to_var sym (VVal v);
+      ValueHT.add var_to_sym (VVal v) sym;
+      VVal v
+
+    let prophesize var = 
+      let sym = symbol_of var in 
+      let sym_name = (Syntax.show_symbol srk sym) ^ "_prophecy" in
+      let sym' = Syntax.mk_symbol srk ~name:sym_name (Syntax.typ_symbol srk sym) in 
+      let var' = make_var sym' false in 
+      ValueHT.add prophecy_vars var var'; 
+      ValueHT.add var_of_prophecy_vars var' var;
+      var' 
+
+    let var_of_prophecy_var var' = ValueHT.find_opt var_of_prophecy_vars var'
+    let prophecy_var_of_var var = ValueHT.find_opt prophecy_vars var 
+    let is_prophecy_var v = 
+      match var_of_prophecy_var v with 
+      | Some _ -> true 
+      | None -> false
+  end
+
 
 module K = struct
   module Tr = Transition.Make(Ctx)(V)
@@ -212,6 +246,8 @@ module K = struct
       Log.time "cra:star" star x
 
   let project = exists V.is_global
+
+  let project_custom v = exists v 
 end
 
 type ptr_term =
@@ -751,21 +787,114 @@ let decorate_transition_system predicates ts entry =
       let invariant =
         abstract_domain.formula_of (abstract_domain.exists (member live) (inv v))
       in
+      logf "loop header location: %d" v;
       logf "Found invariant at %d:@;%a" v (Syntax.Formula.pp srk) invariant;
+      logf "New ID: %d" fresh_id; 
       WG.split_vertex ts v (Weight (K.assume invariant)) fresh_id)
     ts
 
-let make_transition_system rg =
+module VSet = BatSet.Make(V)
+module ISet = BatSet.Make(Int)
+
+let create_gas_variable () = 
+  let mk_int k = Ctx.mk_real (QQ.of_int k) in 
+  let gas_var = Var.mk (Varinfo.mk_global "__duet_gas" (Concrete (Int 8))) in 
+  let gas_var_sym = Syntax.mk_symbol srk ~name:"__duet_gas" `TyInt in  
+  let gas_var_term = Syntax.mk_const srk gas_var_sym in 
+  Hashtbl.add V.sym_to_var gas_var_sym (VVal gas_var);
+  ValueHT.add V.var_to_sym (VVal gas_var) gas_var_sym;
+  let gasexpr = (Syntax.mk_lt srk (mk_int 0) gas_var_term) in 
+  let gasweight =
+    let assume_positive = K.assume gasexpr in
+    let decr_by_one = Syntax.mk_sub srk gas_var_term (mk_int 1) |> K.assign (VVal gas_var) in
+      K.mul assume_positive decr_by_one in 
+  let initial_gas = K.havoc [ VVal gas_var ] in  
+  (gasweight, gasexpr, initial_gas) 
+
+let new_vtx () = (Def.mk (Assume Bexpr.ktrue)).did 
+
+let instrument_with_gas (ts: TSG.t) gasexpr : TSG.t = 
+  let modify_pre ts u =
+    Printf.printf " --- %d is call edge\n" u;
+    let g = ref ts in 
+    (* step 1: add new in-edge to (u, v) *) 
+    let x = new_vtx () in 
+      g := WG.add_vertex !g x;
+      (* step 2: add weighted edge x-(gasexpr)->u *)
+      g := WG.add_edge !g x (Weight gasexpr) u;
+      (* step 3: redirect every p->u to be y->x->u *)
+      WG.iter_pred_e (fun (p, weight, _) -> 
+        Printf.printf "changing %d->%d to %d->%d->%d\n" p u p x u;
+        g := WG.add_edge !g p weight x;
+        g := WG.remove_edge !g p u  
+        ) ts u;
+      !g in 
+  let modify_post ts u = 
+    Printf.printf " --- %d is loop header\n" u;
+    let g = ref ts in 
+    let x = new_vtx () in 
+    (* step 1: add new out-edge from u -> x *)
+    g := WG.add_vertex !g x;
+    g := WG.add_edge !g u (Weight gasexpr) x;
+    (* step 2: for each u -> v, make it u -> x -> v *)
+    WG.iter_succ_e (fun (_, weight, v) -> 
+      Printf.printf "changing %d->%d to %d->%d->%d\n" u v u x v;
+      g := WG.add_edge !g x weight v;
+      g := WG.remove_edge !g u v
+      ) ts u; 
+      !g in
+  (* for each call-edge, u->v, add new predecessor edge x->u->v where x->u is an instrumented edge. *)
+  let loop_headers = 
+    let module L = Loop.Make(TSG) in 
+      (List.map (fun loop -> L.header loop) @@ L.all_loops (L.loop_nest ts))
+        |> List.map (fun x -> (x, true)) in 
+  let call_edge_headers, _ = 
+    WG.fold_edges (fun (u, w, _) (headers, callees) -> 
+          match w with 
+          | Call (s, _) -> ISet.add u headers, ISet.add s callees 
+          | Weight _ -> (headers, callees)) ts (ISet.empty, ISet.empty) in     
+
+    List.fold_left (fun ts (header, is_call_edge) -> 
+            if is_call_edge then 
+              modify_post ts header 
+            else 
+              modify_pre ts header) ts 
+            (loop_headers 
+              @ (List.map (fun x -> (x, false)) @@ ISet.to_list call_edge_headers))
+
+let instrument_main tg entry init_gas_expr = 
+  let post_entry = new_vtx () in 
+  (* step 1: add a vertex called post_entry *)
+  let tg = WG.add_vertex tg post_entry in 
+  (* step 2: remove each edge (entry->v) and make it (post_entry->v) *)
+  let gg = ref tg in
+  WG.iter_succ_e (fun (u, w, v) -> 
+    assert (u = entry);
+    gg := WG.remove_edge !gg entry v;
+    gg := WG.add_edge !gg post_entry w v
+    ) tg entry;
+  (* step 3: add edge from entry->post_entry labeled by init_gas_expr *)
+  WG.add_edge !gg entry (Weight init_gas_expr) post_entry 
+
+let make_transition_system ?(simplify=true) ?(instr_gas=false) (main_entry: int) rg =
+  let gasweight, gasexpr, init_gas_weight = create_gas_variable () in 
   let call_edge block =
     Call ((RG.block_entry rg block).did, (RG.block_exit rg block).did)
   in
   let assertions = ref SrkUtil.Int.Map.empty in
-  let add_assert v e =
-    assertions := SrkUtil.Int.Map.add v e (!assertions)
+  let assert_vars = ref VSet.empty in
+  let add_assert v (cond, loc, msg) =
+    assertions := SrkUtil.Int.Map.add v (cond, loc, msg) (!assertions);
+    let open Syntax in
+    Symbol.Set.iter (fun (s : Syntax.symbol) ->
+        match V.of_symbol s with
+        | Some v -> assert_vars := VSet.add v (!assert_vars)
+        | None -> ())
+      (Syntax.symbols cond)
   in
   let ts =
-    BatEnum.fold (fun ts (block, graph) ->
-        let tg =
+    BatEnum.fold (fun ts (block, graph) -> (* CFG of current function *)
+        let tg = (* TS of current CFG *)
           RG.G.fold_vertex (fun def tg ->
               let tg = WG.add_vertex tg def.did in
               let label =
@@ -820,8 +949,14 @@ let make_transition_system rg =
         let point_of_interest v =
           v = entry || v = exit || SrkUtil.Int.Map.mem v (!assertions)
         in
-        let tg = TS.simplify point_of_interest tg in
-        let tg = TS.remove_temporaries tg in
+        let elim_var v =
+          V.is_global v || VSet.mem v (!assert_vars)
+        in
+        let tg = if (instr_gas && entry = main_entry) then instrument_main tg entry init_gas_weight else tg in
+        let tg = if instr_gas then instrument_with_gas tg gasweight else tg in 
+        let predicates = if instr_gas then gasexpr :: predicates else predicates in  
+        let tg = if simplify then TS.simplify point_of_interest tg else tg in
+        let tg = TS.remove_temporaries elim_var tg in
         let tg =
           if !forward_inv_gen then
             Log.phase "Forward invariant generation"
@@ -841,7 +976,10 @@ let make_transition_system rg =
       TS.empty
       (RG.bodies rg)
   in
-  (ts, !assertions)
+  (* perform some inlining *)
+  let inlined_ts, new_assertions = 
+    TS.inline ts main_entry (fun _ -> ()) (!assertions) in 
+    (inlined_ts, new_assertions)
 
 let mk_query ts entry =
   TS.mk_query ts entry
@@ -856,7 +994,7 @@ let analyze file =
   | [main] -> begin
       let rg = Interproc.make_recgraph file in
       let entry = (RG.block_entry rg main).did in
-      let (ts, assertions) = make_transition_system rg in
+      let (ts, assertions) = make_transition_system entry rg in
       (*TSDisplay.display ts;*)
       let query = mk_query ts entry in
       assertions |> SrkUtil.Int.Map.iter (fun v (phi, loc, msg) ->
@@ -1093,7 +1231,7 @@ let prove_termination_main file =
   | [main] -> begin
       let rg = Interproc.make_recgraph file in
       let entry = (RG.block_entry rg main).did in
-      let (ts, _) = make_transition_system rg in
+      let (ts, _) = make_transition_system entry rg in
       if !CmdLine.display_graphs then
         TSDisplay.display ts;
       let query = mk_query ts entry in
@@ -1152,7 +1290,8 @@ let resource_bound_analysis file =
   match file.entry_points with
   | [main] -> begin
       let rg = Interproc.make_recgraph file in
-      let (ts, _) = make_transition_system rg in
+      let entry  = (RG.block_entry rg main).did in 
+      let (ts, _) = make_transition_system entry rg in
       let entry = (RG.block_entry rg main).did in
       let query = mk_query ts entry in
       let cost =

duet/duet.ml

@@ -11,13 +11,20 @@ open! Cra
 open! Proofspace
 open! Dependence
 open! Categorize
+open! Gps
 
 let usage_msg = "Duet program analyzer\nUsage: duet [OPTIONS] file.[c|bp]"
 
 let anon_fun s = ignore (CmdLine.parse s)
 
 let _ =
   Sys.set_signal Sys.sigtstp (Sys.Signal_handle (fun _ -> Log.print_stats ()));
+  Printexc.record_backtrace true;;
+  Sys.set_signal Sys.sigint (Sys.Signal_handle (fun _ ->
+    Printf.eprintf "SIGINT received. Backtrace:\n%!";
+    Printexc.print_backtrace stderr;
+    exit 1
+  ));;
   let spec_list = CmdLine.spec_list () in
   Arg.parse (Arg.align spec_list) anon_fun usage_msg;
   match !CfgIr.gfile with