Soundness check

lib/analysis/analysis_check.ml

@@ -0,0 +1,92 @@
+(** Soundness check for analysis results, implemented by ensuring the abstract
+    state (returned by analysis) is compatible with the concrete state (returned
+    by evaluation). *)
+
+open Bincaml_util.Common
+
+type check_err =
+  | InterpreterCheckError of {
+      message : string;
+      stmt : (Var.t, Var.t, Lang.Ops.AllOps.const) Lang.Stmt.t; [@opaque]
+      loc : Lang.Interp.IState.loc;
+    }
+[@@deriving show]
+
+let check_soundness_of_istate
+    (check_predicate : 'a -> 'b -> (unit, string) Result.t) absstate
+    (event : Lang.Interp.IState.event) =
+  let merge k conc abs =
+    match (conc, abs) with
+    | Some a, Some b -> Some (Result.Ok (a, b))
+    | None, Some _ ->
+        Some
+          (Result.fail
+             "abstract variable exists with no corresponding concrete variable")
+    | Some _, None | None, None -> None
+  in
+
+  match event with
+  | TraceVariables { vars; stmt; loc } ->
+      VarMap.merge merge absstate vars
+      |> VarMap.filter_map (fun k result ->
+          result
+          |> Result.flat_map (Fun.uncurry check_predicate)
+          |> Result.map_err (fun message ->
+              InterpreterCheckError { stmt; loc; message })
+          |> Result.fold ~ok:(fun _ -> None) ~error:Option.some)
+  | _ -> VarMap.empty
+
+let go () =
+  let loaded = Loader.Loadir.ast_of_fname "examples/cat.il" in
+  let prog = loaded.prog in
+
+  let id = prog.proc_names.get_id "@p9main_4198208" in
+  let proc = ID.Map.find id prog.procs in
+
+  Containers_pp.pp Format.std_formatter @@ Lang.Program.prog_pretty prog;
+
+  let abs_result =
+    Defuse_bool.analyse proc
+    |> Option.get_exn_or "defuse_bool analyse"
+    |> Defuse_bool.Domain.to_iter |> VarMap.of_iter
+  in
+
+  let pc_var = Var.Decls.find prog.globals "$_PC" in
+  let istate =
+    Lang.Interp.IState.create
+      ~events_filter:(function TraceVariables _ -> true | _ -> false)
+      prog
+    |> Lang.Interp.IState.write_var pc_var
+         (`Bitvector (Bitvec.of_int ~size:64 0x400f40))
+  in
+  let conc_state, _final_vars =
+    Lang.Interp.IState.call_proc istate proc
+    @@ StringMap.singleton "_PC" (`Bitvector (Bitvec.of_int ~size:64 0x400f40))
+  in
+  let check_predicate abs conc =
+    let open Defuse_bool.IsZeroValueAbstraction in
+    (match (abs, conc) with
+      | Top, _ -> true
+      | Bot, _ -> false
+      (* kinda lazy to re-use the domain eval functions here. *)
+      | Zero, x -> equal (eval_const x) Zero
+      | NonZero, x -> equal (eval_const x) NonZero)
+    |> function
+    | true -> Ok ()
+    | false -> Error "blahpsie"
+  in
+
+  let check_errs =
+    List.concat_map
+      (fun event ->
+        check_soundness_of_istate check_predicate abs_result event
+        |> VarMap.to_list)
+      conc_state.events
+  in
+
+  print_endline "errors:";
+  List.iter
+    (fun (var, err) ->
+      Var.pp Format.std_formatter var;
+      pp_check_err Format.std_formatter err)
+    check_errs

lib/analysis/dune

@@ -2,7 +2,12 @@
  (public_name bincaml.analysis)
  (name analysis)
  (flags -w -27)
- (modules dataflow_graph intra_analysis defuse_bool lattice_types)
+ (modules
+  dataflow_graph
+  intra_analysis
+  defuse_bool
+  lattice_types
+  analysis_check)
  (libraries
   patricia-tree
   loader

lib/lang/interp.ml

@@ -370,7 +370,9 @@ end
 
 module IState = struct
   type stack_frame = { locals : IValue.t VarMap.t; proc : Program.proc }
-  type loc = { proc : Program.proc; vert : Procedure.Vert.t }
+
+  type loc = { proc : Program.proc; [@opaque] vert : Procedure.Vert.t }
+  [@@deriving show { with_path = false }]
 
   let show_loc l =
     Printf.sprintf "%s::%s"
@@ -386,6 +388,25 @@ module IState = struct
         value : Ops.AllOps.const;
       }
     | Load of { mem : string; addr : Ops.AllOps.const }
+    | TraceVariables of {
+        vars : Ops.AllOps.const VarMap.t;
+            [@printer fun fmt -> VarMap.pp Var.pp Ops.AllOps.pp_const fmt]
+        loc : loc;
+        stmt : (Var.t, Var.t, Ops.AllOps.const) Stmt.t;
+            [@printer
+              fun fmt ->
+                Stmt.pretty Var.pretty Var.pretty (fun const ->
+                    let buf = Buffer.create 50 in
+                    let fmt = Format.formatter_of_buffer buf in
+                    Ops.AllOps.pp_const fmt const;
+                    Containers_pp.text (Buffer.contents buf))]
+      }
+        (** A moment-in-time trace of the state of variables in during
+            evaluation.
+
+            The map of variables is represented as a function returning a value,
+            and this includes locals and globals. This function may throw
+            {!ReadUninit} if the requested variable is uninitialised. *)
   [@@deriving show { with_path = false }]
 
   type t = {
@@ -396,23 +417,13 @@ module IState = struct
     pc : loc;
     last_block : ID.t option;
     events : event list;
+    events_filter : event -> bool;
+        (** Filter applied to events before they are recorded in the trace.
+            Events are kept if and only if this filter function returns [true].
+        *)
     random_gen : Random.State.t option;
   }
 
-  let add_event st e = { st with events = e :: st.events }
-
-  let add_event_stmt st (stmt : ('a, 'b, Ops.AllOps.const) Stmt.t) =
-    let open Expr.AbstractExpr in
-    let log = add_event st in
-    match stmt with
-    | Stmt.Instr_Load { mem; addr; cells; endian } ->
-        log @@ Load { mem = Var.name mem; addr }
-    | Stmt.Instr_Store { mem; addr; value } ->
-        log @@ Store { mem = Var.name mem; addr; value }
-    | Stmt.Instr_Call { procid; args } ->
-        log @@ Call { procid; args = StringMap.values args |> Iter.to_list }
-    | _ -> st
-
   let show ?(show_stack = true) st =
     let open Containers_pp in
     let stack =
@@ -453,9 +464,15 @@ module IState = struct
             ^ text (PageTable.show m)))
     |> Pretty.to_string ~width:200
 
-  (** create a new state for prog that is either zero-intiialised or randomly
-      initialised based on whether the random geenrator is passed *)
-  let create ?random (prog : Program.t) =
+  (** Creates a new interpreter state for the given program
+
+      @param random Random generator to use for initialising memory. If
+      unspecified, memory is zero-initialised.
+
+      @param events_filter Filter function to use as {!t.events_filter}. If
+      unspecified, defaults to a function returning [false] for
+      {!TraceVariables}, and [true] otherwise. *)
+  let create ?random ?(events_filter = function | TraceVariables _ -> false | _ -> true) (prog : Program.t) =
     let stack = [] in
     let pc =
       {
@@ -493,6 +510,7 @@ module IState = struct
       memories;
       globals;
       events = [];
+      events_filter;
       last_block = None;
       random_gen = random;
     }
@@ -536,6 +554,33 @@ module IState = struct
         { st with stack }
     | Global -> { st with globals = VarMap.add var value st.globals }
 
+  (* FIXME: this still *computes* every event, even those that are dropped by the filter. *)
+  let add_event st e =
+    { st with events = List.filter st.events_filter [ e ] @ st.events }
+
+  let add_event_stmt st (stmt : ('a, 'b, Ops.AllOps.const) Stmt.t) =
+    let open Expr.AbstractExpr in
+    let map_add st (k, v) = VarMap.add k v st in
+    let vars =
+      Iter.append (VarMap.keys st.globals) (VarMap.keys (stack_top st).locals)
+      |> Iter.map (fun v -> (v, read_var v st))
+      |> Iter.fold map_add VarMap.empty
+    in
+
+    let new_events =
+      TraceVariables { vars; loc = st.pc; stmt }
+      ::
+      (match stmt with
+      | Stmt.Instr_Load { mem; addr; cells; endian } ->
+          [ Load { mem = Var.name mem; addr } ]
+      | Stmt.Instr_Store { mem; addr; value } ->
+          [ Store { mem = Var.name mem; addr; value } ]
+      | Stmt.Instr_Call { procid; args } ->
+          [ Call { procid; args = StringMap.values args |> Iter.to_list } ]
+      | _ -> [])
+    in
+    List.fold_left add_event st new_events
+
   let map f v = (fst v, f (snd v))
 
   let return_outputs st =

test/lang/dune

@@ -66,3 +66,11 @@
  (modules pagetable_qcheck)
  (flags -w -27)
  (libraries pagetable_spec qcheck-core.runner qcheck-stm.sequential))
+
+
+(executable
+ (name test_analysis_check)
+ (modules test_analysis_check)
+ (flags -w -27)
+ (libraries bincaml))
+

test/lang/test_analysis_check.ml

@@ -0,0 +1 @@
+let () = Analysis.Analysis_check.go ()