[sledge] Add explicit type for Alarms

Summary:
Currently all alarms are reported as "Invalid memory access", which is
not accurate for `abort` and hence assertion violations. This diff
adds an explicit type for alarms which distinguishes these two
cases. Further refinement is left for later.

Reviewed By: jvillard

Differential Revision: D27828754

fbshipit-source-id: 9c33f3c86

sledge/cli/domain_itv.ml

@@ -47,7 +47,6 @@ let pp fs =
   in
   bindings >> Array.pp "@," (pp_pair Var.print Interval.print) fs
 
-let report_fmt_thunk = Fun.flip pp
 let init _gs = Abstract1.top (Lazy.force man) (Environment.make [||] [||])
 let apron_var_of_name = (fun nm -> "%" ^ nm) >> Apron.Var.of_string
 let apron_var_of_reg = Llair.Reg.name >> apron_var_of_name
@@ -187,17 +186,22 @@ let exec_move move_vec q =
 
 let exec_inst i q =
   match (i : Llair.inst) with
-  | Move {reg_exps; loc= _} -> Some (exec_move reg_exps q)
+  | Move {reg_exps; loc= _} -> Ok (exec_move reg_exps q)
   | Store {ptr; exp; len= _; loc= _} -> (
     match Llair.Reg.of_exp ptr with
-    | Some reg -> Some (assign reg exp q)
-    | None -> Some q )
-  | Load {reg; ptr; len= _; loc= _} -> Some (assign reg ptr q)
-  | Nondet {reg= Some reg; msg= _; loc= _} -> Some (exec_kill reg q)
-  | Nondet {reg= None; msg= _; loc= _} | Alloc _ | Free _ -> Some q
-  | Abort _ -> None
-  | Intrinsic {reg= Some reg; _} -> Some (exec_kill reg q)
-  | Intrinsic {reg= None; _} -> Some q
+    | Some reg -> Ok (assign reg exp q)
+    | None -> Ok q )
+  | Load {reg; ptr; len= _; loc= _} -> Ok (assign reg ptr q)
+  | Nondet {reg= Some reg; msg= _; loc= _} -> Ok (exec_kill reg q)
+  | Nondet {reg= None; msg= _; loc= _} | Alloc _ | Free _ -> Ok q
+  | Intrinsic {reg= Some reg; _} -> Ok (exec_kill reg q)
+  | Intrinsic {reg= None; _} -> Ok q
+  | Abort {loc} ->
+      Error
+        { Alarm.kind= Abort
+        ; loc
+        ; pp_action= Fun.flip Llair.Inst.pp i
+        ; pp_state= Fun.flip pp q }
 
 type from_call = {areturn: Llair.Reg.t option; caller_q: t}
 [@@deriving sexp_of]

sledge/src/alarm.ml

@@ -0,0 +1,25 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+type kind = Abort | Invalid_memory_access
+
+let pp_kind fs = function
+  | Abort -> Format.fprintf fs "Abort"
+  | Invalid_memory_access -> Format.fprintf fs "Invalid memory access"
+
+type t =
+  { kind: kind
+  ; loc: Llair.Loc.t
+  ; pp_action: Format.formatter -> unit
+  ; pp_state: Format.formatter -> unit }
+
+let pp fs {kind; loc; pp_action} =
+  Format.fprintf fs "%a %a@;<1 2>@[%t@]" Llair.Loc.pp loc pp_kind kind
+    pp_action
+
+let pp_trace fs alarm =
+  Format.fprintf fs "%a@;<1 2>@[{ %t@ }@]" pp alarm alarm.pp_state

sledge/src/alarm.mli

@@ -0,0 +1,20 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+type kind = Abort | Invalid_memory_access
+
+type t =
+  { kind: kind
+  ; loc: Llair.Loc.t
+  ; pp_action: Format.formatter -> unit
+  ; pp_state: Format.formatter -> unit }
+
+val pp : t pp
+(** print an alarm for the user report *)
+
+val pp_trace : t pp
+(** print an error for the debug trace *)

sledge/src/control.ml

@@ -499,17 +499,11 @@ module Make (Opts : Domain_intf.Opts) (Dom : Domain_intf.Dom) = struct
     | Throw {exc} -> exec_throw stk state block exc
     | Unreachable -> Work.skip
 
-  let exec_inst :
-         Llair.block
-      -> Llair.inst
-      -> Dom.t
-      -> (Dom.t, Dom.t * Llair.inst) result =
+  let exec_inst : Llair.block -> Llair.inst -> Dom.t -> Dom.t Or_alarm.t =
    fun block inst state ->
     [%Trace.info "@\n@[%a@]@\n%a" Dom.pp state Llair.Inst.pp inst] ;
     Report.step_inst block inst ;
     Dom.exec_inst inst state
-    |> function
-    | Some state -> Result.Ok state | None -> Result.Error (state, inst)
 
   let exec_block :
       Llair.program -> Stack.t -> Dom.t -> Llair.block -> Work.x =
@@ -528,8 +522,8 @@ module Make (Opts : Domain_intf.Opts) (Dom : Domain_intf.Dom) = struct
         state
     with
     | Ok state -> exec_term pgm stk state block
-    | Error (state, inst) ->
-        Report.invalid_access_inst (Dom.report_fmt_thunk state) inst ;
+    | Error alarm ->
+        Report.alarm alarm ;
         Work.skip
 
   let harness : Llair.program -> Work.t option =

sledge/src/domain_intf.ml

@@ -10,14 +10,13 @@ module type Dom = sig
   type t [@@deriving compare, equal, sexp_of]
 
   val pp : t pp
-  val report_fmt_thunk : t -> Format.formatter -> unit
   val init : Llair.GlobalDefn.t iarray -> t
   val join : t -> t -> t option
   val dnf : t -> t list
   val exec_assume : t -> Llair.Exp.t -> t option
   val exec_kill : Llair.Reg.t -> t -> t
   val exec_move : (Llair.Reg.t * Llair.Exp.t) iarray -> t -> t
-  val exec_inst : Llair.inst -> t -> t option
+  val exec_inst : Llair.inst -> t -> t Or_alarm.t
 
   type from_call [@@deriving sexp_of]
 

sledge/src/domain_relation.ml

@@ -31,7 +31,6 @@ module Make (State_domain : State_domain_sig) = struct
   let pp fs (entry, curr) =
     Format.fprintf fs "@[%a%a@]" pp_entry entry State_domain.pp curr
 
-  let report_fmt_thunk (_, curr) fs = State_domain.pp fs curr
   let init globals = embed (State_domain.init globals)
 
   let join (entry_a, current_a) (entry_b, current_b) =
@@ -51,6 +50,7 @@ module Make (State_domain : State_domain_sig) = struct
     (entry, State_domain.exec_move reg_exps current)
 
   let exec_inst inst (entry, current) =
+    let open Or_alarm.Import in
     let+ next = State_domain.exec_inst inst current in
     (entry, next)
 

sledge/src/domain_sh.ml

@@ -13,7 +13,6 @@ open Fol
 type t = Sh.t [@@deriving compare, equal, sexp]
 
 let pp fs q = Format.fprintf fs "@[{ %a@ }@]" Sh.pp q
-let report_fmt_thunk = Fun.flip pp
 
 (* set by cli *)
 let simplify_states = ref true
@@ -55,25 +54,37 @@ let exec_move res q =
   |> simplify
 
 let exec_inst inst pre =
+  let alarm kind =
+    { Alarm.kind
+    ; loc= Llair.Inst.loc inst
+    ; pp_action= Fun.flip Llair.Inst.pp inst
+    ; pp_state= Fun.flip pp pre }
+  in
+  let or_alarm = function
+    | Some post -> Ok post
+    | None -> Error (alarm Invalid_memory_access)
+  in
   ( match (inst : Llair.inst) with
   | Move {reg_exps; _} ->
-      Some
+      Ok
         (Exec.move pre
            (IArray.map reg_exps ~f:(fun (r, e) -> (X.reg r, X.term e))))
   | Load {reg; ptr; len; _} ->
       Exec.load pre ~reg:(X.reg reg) ~ptr:(X.term ptr) ~len:(X.term len)
+      |> or_alarm
   | Store {ptr; exp; len; _} ->
       Exec.store pre ~ptr:(X.term ptr) ~exp:(X.term exp) ~len:(X.term len)
+      |> or_alarm
   | Alloc {reg; num; len; _} ->
-      Exec.alloc pre ~reg:(X.reg reg) ~num:(X.term num) ~len
-  | Free {ptr; _} -> Exec.free pre ~ptr:(X.term ptr)
-  | Nondet {reg; _} -> Some (Exec.nondet pre (Option.map ~f:X.reg reg))
-  | Abort _ -> Exec.abort pre
+      Exec.alloc pre ~reg:(X.reg reg) ~num:(X.term num) ~len |> or_alarm
+  | Free {ptr; _} -> Exec.free pre ~ptr:(X.term ptr) |> or_alarm
+  | Nondet {reg; _} -> Ok (Exec.nondet pre (Option.map ~f:X.reg reg))
+  | Abort _ -> Error (alarm Abort)
   | Intrinsic {reg; name; args; _} ->
       let areturn = Option.map ~f:X.reg reg in
       let actuals = IArray.map ~f:X.term args in
-      Exec.intrinsic pre areturn name actuals )
-  |> Option.map ~f:simplify
+      Exec.intrinsic pre areturn name actuals |> or_alarm )
+  |> Or_alarm.map ~f:simplify
 
 let value_determined_by ctx us a =
   List.exists (Context.class_of ctx a) ~f:(fun b ->

sledge/src/domain_unit.ml

@@ -10,13 +10,12 @@
 type t = unit [@@deriving compare, equal, sexp]
 
 let pp fs () = Format.pp_print_string fs "()"
-let report_fmt_thunk () fs = pp fs ()
 let init _ = ()
 let join () () = Some ()
 let exec_assume () _ = Some ()
 let exec_kill _ () = ()
 let exec_move _ () = ()
-let exec_inst _ () = Some ()
+let exec_inst _ () = Ok ()
 
 type from_call = unit [@@deriving compare, equal, sexp]
 

sledge/src/domain_used_globals.ml

@@ -10,7 +10,6 @@
 type t = Llair.Global.Set.t [@@deriving compare, equal, sexp]
 
 let pp = Llair.Global.Set.pp
-let report_fmt_thunk = Fun.flip pp
 let empty = Llair.Global.Set.empty
 
 let init globals =
@@ -39,10 +38,10 @@ let exec_move reg_exps st =
 let exec_inst inst st =
   [%Trace.call fun {pf} -> pf "@ pre:{%a} %a" pp st Llair.Inst.pp inst]
   ;
-  Some (Llair.Inst.fold_exps ~f:used_globals inst st)
+  Ok (Llair.Inst.fold_exps ~f:used_globals inst st)
   |>
   [%Trace.retn fun {pf} ->
-    Option.iter ~f:(fun uses -> pf "post:{%a}" pp uses)]
+    Or_alarm.iter ~f:(fun uses -> pf "post:{%a}" pp uses)]
 
 type from_call = t [@@deriving sexp]
 

sledge/src/exec.ml

@@ -737,7 +737,6 @@ let store pre ~ptr ~exp ~len = exec_spec pre (store_spec ptr exp len)
 let alloc pre ~reg ~num ~len = exec_spec pre (alloc_spec reg num len)
 let free pre ~ptr = exec_spec pre (free_spec ptr)
 let nondet pre = function Some reg -> kill pre reg | None -> pre
-let abort _ = None
 
 let intrinsic :
        Sh.t

sledge/src/exec.mli

@@ -17,7 +17,6 @@ val store : Sh.t -> ptr:Term.t -> exp:Term.t -> len:Term.t -> Sh.t option
 val alloc : Sh.t -> reg:Var.t -> num:Term.t -> len:int -> Sh.t option
 val free : Sh.t -> ptr:Term.t -> Sh.t option
 val nondet : Sh.t -> Var.t option -> Sh.t
-val abort : Sh.t -> Sh.t option
 
 val intrinsic :
   Sh.t -> Var.t option -> Llair.Intrinsic.t -> Term.t iarray -> Sh.t option

sledge/src/or_alarm.ml

@@ -0,0 +1,21 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+module T = struct
+  type 'a t = ('a, Alarm.t) result
+end
+
+include Stdlib.Result
+
+include Monad.Make (struct
+  include T
+
+  let return = Result.ok
+  let bind = Result.bind
+end)
+
+let iter x ~f = iter f x

sledge/src/or_alarm.mli

@@ -0,0 +1,12 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+type 'a t = ('a, Alarm.t) result
+
+include Monad.S with type 'a t := 'a t
+
+val iter : 'a t -> f:('a -> unit) -> unit

sledge/src/report.ml

@@ -7,6 +7,14 @@
 
 (** Issue reporting *)
 
+let alarm_count = ref 0
+
+let alarm alrm =
+  Int.incr alarm_count ;
+  Format.printf "@\n@[<v 2>%a@]@." Alarm.pp alrm ;
+  [%Trace.printf "@\n@[<v 2>%a@]@." Alarm.pp_trace alrm] ;
+  Stop.on_alarm ()
+
 let unknown_call call =
   [%Trace.kprintf
     Stop.on_unknown_call
@@ -20,24 +28,6 @@ let unknown_call call =
         | _ -> () )
       call Llair.Term.pp call]
 
-let invalid_access_count = ref 0
-
-let invalid_access fmt_thunk pp access loc =
-  Int.incr invalid_access_count ;
-  let rep fs =
-    Format.fprintf fs "%a Invalid memory access@;<1 2>@[%a@]" Llair.Loc.pp
-      (loc access) pp access
-  in
-  Format.printf "@\n@[<v 2>%t@]@." rep ;
-  [%Trace.printf "@\n@[<v 2>%t@;<1 2>@[{ %t@ }@]@]@." rep fmt_thunk] ;
-  Stop.on_invalid_access ()
-
-let invalid_access_inst fmt_thunk inst =
-  invalid_access fmt_thunk Llair.Inst.pp inst Llair.Inst.loc
-
-let invalid_access_term fmt_thunk term =
-  invalid_access fmt_thunk Llair.Term.pp term Llair.Term.loc
-
 (** Functional statistics *)
 
 let solver_steps = ref 0
@@ -95,8 +85,8 @@ let pp_status ppf stat =
   | UnknownError msg -> pf "Unknown error: %s" msg
 
 let safe_or_unsafe () =
-  if !invalid_access_count = 0 then Safe {bound= !bound}
-  else Unsafe {alarms= !invalid_access_count; bound= !bound}
+  if !alarm_count = 0 then Safe {bound= !bound}
+  else Unsafe {alarms= !alarm_count; bound= !bound}
 
 type gc_stats = {allocated: float; promoted: float; peak_size: float}
 [@@deriving sexp]

sledge/src/report.mli

@@ -13,8 +13,7 @@ val step_inst : Llair.block -> Llair.inst -> unit
 val step_term : Llair.block -> unit
 val hit_bound : int -> unit
 val unknown_call : Llair.term -> unit
-val invalid_access_inst : (Format.formatter -> unit) -> Llair.inst -> unit
-val invalid_access_term : (Format.formatter -> unit) -> Llair.term -> unit
+val alarm : Alarm.t -> unit
 
 type status =
   | Safe of {bound: int}

sledge/src/stop.ml

@@ -8,4 +8,4 @@
 (** Stop analysis when encountering issues *)
 
 let on_unknown_call _ = [%Trace.kprintf (fun _ -> assert false) ""]
-let on_invalid_access _ = [%Trace.kprintf (fun _ -> assert false) ""]
+let on_alarm _ = [%Trace.kprintf (fun _ -> assert false) ""]

sledge/src/stop.mli

@@ -8,4 +8,4 @@
 (** Stop analysis when encountering issues *)
 
 val on_unknown_call : 'a -> unit
-val on_invalid_access : 'a -> unit
+val on_alarm : 'a -> unit