Bi-abduction transfomer

GillianCore/GIL_Syntax/Gil_syntax.mli

@@ -1154,6 +1154,8 @@ module Prog : sig
 
   (** Print indexed *)
   val pp_indexed : Format.formatter -> ?pp_annot:'a Fmt.t -> ('a, int) t -> unit
+
+  val make_callgraph : ('a, 'b) t -> Call_graph.t
 end
 
 (** @canonical Gillian.Gil_syntax.Visitors *)

GillianCore/GIL_Syntax/Prog.ml

@@ -253,3 +253,27 @@ let add_macro (prog : ('a, 'b) t) (macro : Macro.t) : ('a, 'b) t =
 let add_bispec (prog : ('a, 'b) t) (bi_spec : BiSpec.t) : ('a, 'b) t =
   Hashtbl.add prog.bi_specs bi_spec.bispec_name bi_spec;
   prog
+
+let make_callgraph (prog : ('a, 'b) t) =
+  let fcalls =
+    Hashtbl.fold
+      (fun _ proc acc ->
+        Proc.(proc.proc_name, proc.proc_aliases, proc.proc_calls) :: acc)
+      prog.procs []
+  in
+  let call_graph = Call_graph.make () in
+  let fnames = Hashtbl.create (List.length fcalls * 2) in
+  fcalls
+  |> List.iter (fun (sym, aliases, _) ->
+         Call_graph.add_proc call_graph sym;
+         Hashtbl.add fnames sym sym;
+         aliases |> List.iter (fun alias -> Hashtbl.add fnames alias sym));
+  fcalls
+  |> List.iter (fun (caller, _, callees) ->
+         callees
+         |> List.iter (fun callee ->
+                match Hashtbl.find_opt fnames callee with
+                | Some callee ->
+                    Call_graph.add_proc_call call_graph caller callee
+                | None -> ()));
+  call_graph

GillianCore/command_line/act_console.ml

@@ -23,6 +23,10 @@ struct
     let doc = "Emit specs to stdout, useful for testing." in
     Arg.(value & flag & info [ "specs-to-stdout" ] ~doc)
 
+  let ignored_procs =
+    let doc = "Procs to ignore" in
+    Arg.(value & opt_all string [] & info [ "ignore" ] ~doc)
+
   let parse_eprog file files already_compiled =
     if not already_compiled then
       let () =
@@ -64,30 +68,6 @@ struct
     let out_path = Filename.concat dirname (fname ^ "_bi.gil") in
     Io_utils.save_file_pp out_path (Prog.pp_labeled ~pp_annot) e_prog
 
-  let make_callgraph (prog : ('a, 'b) Prog.t) =
-    let fcalls =
-      Hashtbl.fold
-        (fun _ proc acc ->
-          Proc.(proc.proc_name, proc.proc_aliases, proc.proc_calls) :: acc)
-        prog.procs []
-    in
-    let call_graph = Call_graph.make () in
-    let fnames = Hashtbl.create (List.length fcalls * 2) in
-    fcalls
-    |> List.iter (fun (sym, aliases, _) ->
-           Call_graph.add_proc call_graph sym;
-           Hashtbl.add fnames sym sym;
-           aliases |> List.iter (fun alias -> Hashtbl.add fnames alias sym));
-    fcalls
-    |> List.iter (fun (caller, _, callees) ->
-           callees
-           |> List.iter (fun callee ->
-                  match Hashtbl.find_opt fnames callee with
-                  | Some callee ->
-                      Call_graph.add_proc_call call_graph caller callee
-                  | None -> ()));
-    call_graph
-
   let process_files
       files
       already_compiled
@@ -109,7 +89,7 @@ struct
     let+ prog =
       Gil_parsing.eprog_to_prog ~other_imports:PC.other_imports e_prog
     in
-    let call_graph = make_callgraph prog in
+    let call_graph = Prog.make_callgraph prog in
     let () =
       L.normal (fun m -> m "@\n*** Stage 2: DONE transforming the program.@\n")
     in
@@ -134,6 +114,7 @@ struct
       incremental
       bi_unroll_depth
       bi_no_spec_depth
+      ignored_specs
       () =
     let () = Config.current_exec_mode := BiAbduction in
     let () = PC.initialize BiAbduction in
@@ -143,6 +124,7 @@ struct
     let () = Config.bi_no_spec_depth := bi_no_spec_depth in
     let () = Config.specs_to_stdout := specs_to_stdout in
     let () = Config.max_branching := bi_unroll_depth in
+    let () = Config.bi_ignore_procs := ignored_specs in
     let () = Config.under_approximation := true in
     let r =
       process_files files already_compiled outfile_opt should_emit_specs
@@ -156,7 +138,7 @@ struct
     Term.(
       const act $ files $ already_compiled $ output_gil $ no_heap $ stats
       $ should_emit_specs $ specs_to_stdout $ incremental $ bi_unroll_depth
-      $ bi_no_spec_depth)
+      $ bi_no_spec_depth $ ignored_procs)
 
   let act_info =
     let doc =

GillianCore/command_line/command_line.ml

@@ -1,5 +1,6 @@
 open Cmdliner
 module ParserAndCompiler = ParserAndCompiler
+module Act_console = Act_console
 
 module Make
     (ID : Init_data.S)

GillianCore/command_line/command_line.mli

@@ -2,6 +2,15 @@
 
 module ParserAndCompiler = ParserAndCompiler
 
+module Act_console : sig
+  module Make
+      (ID : Init_data.S)
+      (PC : ParserAndCompiler.S with type init_data = ID.t)
+      (Abductor :
+        Abductor.S with type init_data = ID.t and type annot = PC.Annot.t)
+      (Gil_parsing : Gil_parsing.S with type annot = PC.Annot.t) : Console.S
+end
+
 module Make
     (ID : Init_data.S)
     (CMemory : CMemory.S with type init_data = ID.t)

GillianCore/engine/Abstraction/Matcher.ml

@@ -1508,8 +1508,6 @@ module Make (State : SState.S) :
             let successes, errors = Res_list.split res_list in
             match (!Config.under_approximation, successes, errors) with
             (* We start by handling the crash cases that should never happen *)
-            | true, _, _ :: _ ->
-                L.fail "ERROR: IMPOSSIBLE! MATCHING ERRORS IN UX MODE!!!!"
             | true, [], _ ->
                 (* Vanished in UX *)
                 match_mp' (rest_search_states, errs_so_far)
@@ -1556,7 +1554,7 @@ module Make (State : SState.S) :
                 | Ok res -> Ok res
                 | Error errs ->
                     match_mp' (rest_search_states, errs @ errs_so_far))
-            | true, first :: rem, [] ->
+            | true, first :: rem, _ ->
                 let rem =
                   List.map
                     (fun state ->

GillianCore/engine/Abstraction/PState.ml

@@ -1,12 +1,19 @@
 (** Interface for GIL Predicate States. They are considered to be mutable. *)
 module type S = sig
-  include SState.S
-
   type state_t
-  type abs_t = string * vt list
+  type abs_t = string * SVal.M.t list
 
   module SMatcher : Matcher.S with type state_t = state_t
 
+  type t = SMatcher.t = {
+    state : state_t;
+    preds : Preds.t;
+    wands : Wands.t;
+    pred_defs : MP.preds_tbl_t;
+  }
+
+  include SState.S with type t := t
+
   val make_p :
     preds:MP.preds_tbl_t ->
     init_data:init_data ->
@@ -17,6 +24,17 @@ module type S = sig
     unit ->
     t
 
+  val make_p_from_heap :
+    pred_defs:MP.preds_tbl_t ->
+    store:store_t ->
+    heap:heap_t ->
+    spec_vars:SS.t ->
+    wands:Wands.t ->
+    preds:Preds.t ->
+    pfs:PFS.t ->
+    gamma:Type_env.t ->
+    t
+
   val init_with_pred_table : MP.preds_tbl_t -> init_data -> t
 
   (** Get preds of given symbolic state *)
@@ -25,6 +43,8 @@ module type S = sig
   (** Set preds of given symbolic state *)
   val set_preds : t -> Preds.t -> t
 
+  val get_wands : t -> Wands.t
+
   (** Set preds of given symbolic state *)
   val set_wands : t -> Wands.t -> t
 
@@ -115,6 +135,21 @@ module Make (State : SState.S) :
     let state = State.make_s ~init_data ~store ~pfs ~gamma ~spec_vars in
     { state; preds = Preds.init []; wands = Wands.init []; pred_defs = preds }
 
+  let make_s_from_heap ~heap:_ ~store:_ ~pfs:_ ~gamma:_ ~spec_vars:_ =
+    failwith "Calling make_s_from_heap on SState"
+
+  let make_p_from_heap
+      ~pred_defs
+      ~store
+      ~heap
+      ~spec_vars
+      ~wands
+      ~preds
+      ~pfs
+      ~gamma =
+    let sstate = State.make_s_from_heap ~store ~heap ~spec_vars ~pfs ~gamma in
+    { state = sstate; preds; wands; pred_defs }
+
   let make_s ~init_data:_ ~store:_ ~pfs:_ ~gamma:_ ~spec_vars:_ : t =
     failwith "Calling make_s on a PState"
 
@@ -146,6 +181,7 @@ module Make (State : SState.S) :
   let get_preds (astate : t) : Preds.t = astate.preds
   let set_preds (astate : t) (preds : Preds.t) : t = { astate with preds }
   let set_wands astate wands = { astate with wands }
+  let get_wands (astate : t) : Wands.t = astate.wands
 
   let assume ?(unfold = false) (astate : t) (v : Expr.t) : t list =
     let open Syntaxes.List in

GillianCore/engine/Abstraction/PState.mli

@@ -1,12 +1,19 @@
 (** Interface for GIL General States. They are considered to be mutable. *)
 module type S = sig
-  include SState.S
-
   type state_t
-  type abs_t = string * vt list
+  type abs_t = string * SVal.M.t list
 
   module SMatcher : Matcher.S with type state_t = state_t
 
+  type t = SMatcher.t = {
+    state : state_t;
+    preds : Preds.t;
+    wands : Wands.t;
+    pred_defs : MP.preds_tbl_t;
+  }
+
+  include SState.S with type t := t
+
   val make_p :
     preds:MP.preds_tbl_t ->
     init_data:init_data ->
@@ -17,6 +24,17 @@ module type S = sig
     unit ->
     t
 
+  val make_p_from_heap :
+    pred_defs:MP.preds_tbl_t ->
+    store:store_t ->
+    heap:heap_t ->
+    spec_vars:SS.t ->
+    wands:Wands.t ->
+    preds:Preds.t ->
+    pfs:PFS.t ->
+    gamma:Type_env.t ->
+    t
+
   val init_with_pred_table : MP.preds_tbl_t -> init_data -> t
 
   (** Get preds of given symbolic state *)
@@ -25,6 +43,8 @@ module type S = sig
   (** Set preds of given symbolic state *)
   val set_preds : t -> Preds.t -> t
 
+  val get_wands : t -> Wands.t
+
   (** Set wands of given symbolic state *)
   val set_wands : t -> Wands.t -> t
 

GillianCore/engine/Abstraction/Verifier.ml

@@ -4,15 +4,12 @@ module DL = Debugger_log
 
 module type S = sig
   type heap_t
-  type state
   type m_err
   type annot
 
-  module SPState :
-    PState.S
-      with type t = state
-       and type heap_t = heap_t
-       and type m_err_t = m_err
+  module SPState : PState.S with type heap_t = heap_t and type m_err_t = m_err
+
+  type state = SPState.t
 
   module SState :
     SState.S with type t = SPState.state_t and type heap_t = heap_t

GillianCore/engine/Abstraction/Verifier.mli

@@ -1,14 +1,11 @@
 module type S = sig
   type heap_t
-  type state
   type m_err
   type annot
 
-  module SPState :
-    PState.S
-      with type t = state
-       and type heap_t = heap_t
-       and type m_err_t = m_err
+  module SPState : PState.S with type heap_t = heap_t and type m_err_t = m_err
+
+  type state = SPState.t
 
   module SState :
     SState.S with type t = SPState.state_t and type heap_t = heap_t
@@ -71,7 +68,6 @@ module Make
   S
     with type heap_t = SPState.heap_t
      and type m_err = SPState.m_err_t
-     and type state = SPState.t
      and module SPState = SPState
      and module SState = SState
      and type annot = PC.Annot.t