diff --git a/lib/analysis/analysis_check.ml b/lib/analysis/analysis_check.ml new file mode 100644 index 0000000..fc558fa --- /dev/null +++ b/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 diff --git a/lib/analysis/dune b/lib/analysis/dune index 8ed1119..8ffd03b 100644 --- a/lib/analysis/dune +++ b/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 diff --git a/lib/lang/interp.ml b/lib/lang/interp.ml index 86fe0e6..c419975 100644 --- a/lib/lang/interp.ml +++ b/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 = diff --git a/test/lang/dune b/test/lang/dune index 7c256e2..0946cf5 100644 --- a/test/lang/dune +++ b/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)) + diff --git a/test/lang/test_analysis_check.ml b/test/lang/test_analysis_check.ml new file mode 100644 index 0000000..d3a9358 --- /dev/null +++ b/test/lang/test_analysis_check.ml @@ -0,0 +1 @@ +let () = Analysis.Analysis_check.go ()