[sledge] Skeleton for symbolic execution of unsafe intrinsics

Summary:
This diff adds support in symbolic execution for calls to intrinsic
functions, to be used in lieu of adding a separate Llair instruction
for each intrinsic. This involves:

- adding skeleton support in Exec for symbolically execution an
  intrinsic function call;

- exposing this in Domain;

- allowing symbolic execution of block terminators (e.g. function
  call) to possibly fail; and

- generalizing Report for failing terminators.

Reviewed By: ngorogiannis

Differential Revision: D14403652

fbshipit-source-id: d86d9d1b8

sledge/src/control.ml

@@ -119,11 +119,14 @@ end
 let push_jump lcls stk =
   if Set.is_empty lcls then stk else Locals (lcls, stk)
 
-let exec_jump stk state block ({dst; args; retreating} : Llair.jump) =
+let exec_goto stk state block ({dst; retreating} : Llair.jump) =
-  let state, _ = Domain.call state args dst.params dst.locals in
   let stk = push_jump dst.locals stk in
   Work.add ~prev:block ~retreating stk state dst
 
+let exec_jump stk state block ({dst; args} as jmp : Llair.jump) =
+  let state, _ = Domain.call state args dst.params dst.locals in
+  exec_goto stk state block jmp
+
 let push_call locals ~return from_call ?throw stk =
   let push_return jmp from_call stk = Return (jmp, from_call, stk) in
   let push_throw jmp stk =
@@ -217,23 +220,40 @@ let exec_term : Llair.t -> stack -> Domain.t -> Llair.block -> Work.x =
     | [] -> exec_skip_func stk state block return
     | callees ->
         List.fold callees ~init:Work.skip ~f:(fun x callee ->
-            ( if Llair.Func.is_undefined callee then
+            ( match
-              exec_skip_func stk state block return
+                Domain.exec_intrinsic state
-            else
+                  (List.hd return.dst.params)
-              exec_call stk state block
+                  callee.name.var args
-                {dst= callee.entry; args; retreating}
+              with
-                return throw )
+            | Some (Error ()) ->
+                Report.invalid_access_term state block.term ;
+                Work.skip
+            | Some (Ok state) -> exec_goto stk state block return
+            | None when Llair.Func.is_undefined callee ->
+                exec_skip_func stk state block return
+            | None ->
+                exec_call stk state block
+                  {dst= callee.entry; args; retreating}
+                  return throw )
             |> Work.seq x ) )
   | Return {exp} -> exec_return stk state block exp
   | Throw {exc} -> exec_throw stk state block exc
   | Unreachable -> Work.skip
 
+let exec_inst :
+    Domain.t -> Llair.inst -> (Domain.t, Domain.t * Llair.inst) result =
+ fun state inst ->
+  Domain.exec_inst state inst
+  |> Result.map_error ~f:(fun () -> (state, inst))
+
 let exec_block : Llair.t -> stack -> Domain.t -> Llair.block -> Work.x =
  fun pgm stk state block ->
   [%Trace.info "exec %a" Llair.Block.pp block] ;
-  match Vector.fold_result ~f:Domain.exec_inst ~init:state block.cmnd with
+  match Vector.fold_result ~f:exec_inst ~init:state block.cmnd with
   | Ok state -> exec_term pgm stk state block
-  | Error (q, i) -> Report.invalid_access i q ; Work.skip
+  | Error (state, inst) ->
+      Report.invalid_access_inst state inst ;
+      Work.skip
 
 let harness : Llair.t -> Work.t option =
  fun pgm ->

sledge/src/report.ml

@@ -24,14 +24,19 @@ let unknown_call call =
         | _ -> () )
       call Llair.Term.pp call]
 
-let invalid_access inst state =
+let invalid_access state pp access loc =
   Format.printf
-    "@\n\
+    "@\n@[<v 2>%a Invalid memory access executing@;<1 2>@[%a@]@]@." Loc.pp
-     @[<v 2>%a Invalid memory access executing instruction@;<1 2>@[%a@]@]@."
+    (loc access) pp access ;
-    Loc.pp (Llair.Inst.loc inst) Llair.Inst.pp inst ;
   [%Trace.kprintf
     (fun _ -> assert false)
       "@\n\
-       @[<v 2>%a Invalid memory access executing instruction@;<1 2>@[%a@]@ \
+       @[<v 2>%a Invalid memory access executing@;<1 2>@[%a@]@ from \
-       from symbolic state@;<1 2>@[{ %a@ }@]@]@."
+       symbolic state@;<1 2>@[{ %a@ }@]@]@."
-      Loc.pp (Llair.Inst.loc inst) Llair.Inst.pp inst Domain.pp state]
+      Loc.pp (loc access) pp access Domain.pp state]
+
+let invalid_access_inst state inst =
+  invalid_access state Llair.Inst.pp inst Llair.Inst.loc
+
+let invalid_access_term state term =
+  invalid_access state Llair.Term.pp term Llair.Term.loc

sledge/src/report.mli

@@ -8,4 +8,5 @@
 (** Issue reporting *)
 
 val unknown_call : Llair.term -> unit
-val invalid_access : Llair.inst -> Domain.t -> unit
+val invalid_access_inst : Domain.t -> Llair.inst -> unit
+val invalid_access_term : Domain.t -> Llair.term -> unit

sledge/src/symbheap/domain.ml

@@ -22,6 +22,7 @@ let init globals =
 let join = Sh.or_
 let assume q b = Exec.assume b q
 let exec_inst = Exec.inst
+let exec_intrinsic = Exec.intrinsic
 
 type from_call = Var.Subst.t [@@deriving compare, equal, sexp]
 

sledge/src/symbheap/domain.mli

@@ -13,7 +13,10 @@ val pp : t pp
 val init : Global.t vector -> t
 val join : t -> t -> t
 val assume : t -> Exp.t -> t option
-val exec_inst : t -> Llair.inst -> (t, t * Llair.inst) result
+val exec_inst : t -> Llair.inst -> (t, unit) result
+
+val exec_intrinsic :
+  t -> Var.t option -> Var.t -> Exp.t list -> (t, unit) result option
 
 type from_call [@@deriving compare, equal, sexp]
 

sledge/src/symbheap/exec.ml

@@ -285,13 +285,13 @@ let rec exec_specs pre = function
       exec_specs pre specs >>| fun posts -> Sh.or_ post posts
   | [] -> Ok (Sh.false_ pre.us)
 
-let inst : Sh.t -> Llair.inst -> (Sh.t, _) result =
+let inst : Sh.t -> Llair.inst -> (Sh.t, unit) result =
  fun pre inst ->
   [%Trace.info
     "@[<2>exec inst %a from@ @[{ %a@ }@]@]" Llair.Inst.pp inst Sh.pp pre] ;
   assert (Set.disjoint (Sh.fv pre) (Llair.Inst.locals inst)) ;
   let us = pre.us in
-  ( match inst with
+  match inst with
   | Load {reg; ptr; len} -> exec_spec pre (load_spec us reg ptr len)
   | Store {ptr; exp; len} -> exec_spec pre (store_spec us ptr exp len)
   | Memset {dst; byt; len} -> exec_spec pre (memset_spec us dst byt len)
@@ -301,5 +301,19 @@ let inst : Sh.t -> Llair.inst -> (Sh.t, _) result =
   | Free {ptr} -> exec_spec pre (free_spec us ptr)
   | Malloc {reg; siz} -> exec_spec pre (malloc_spec us reg siz)
   | Strlen {reg; ptr} -> exec_spec pre (strlen_spec us reg ptr)
-  | Nondet _ -> Ok pre )
+  | Nondet _ -> Ok pre
-  |> Result.map_error ~f:(fun () -> (pre, inst))
+
+let intrinsic :
+       Sh.t
+    -> Var.t option
+    -> Var.t
+    -> Exp.t list
+    -> (Sh.t, unit) result option =
+ fun pre result intrinsic actuals ->
+  [%Trace.info
+    "@[<2>exec intrinsic@ @[%a%a(@[%a@])@] from@ @[{ %a@ }@]@]"
+      (Option.pp "%a := " Var.pp)
+      result Var.pp intrinsic (List.pp ",@ " Exp.pp) (List.rev actuals)
+      Sh.pp pre] ;
+  let us = pre.us in
+  match (result, Var.name intrinsic, actuals) with _ -> None

sledge/src/symbheap/exec.mli

@@ -8,4 +8,7 @@
 (** Symbolic Execution *)
 
 val assume : Exp.t -> Sh.t -> Sh.t option
-val inst : Sh.t -> Llair.inst -> (Sh.t, Sh.t * Llair.inst) result
+val inst : Sh.t -> Llair.inst -> (Sh.t, unit) result
+
+val intrinsic :
+  Sh.t -> Var.t option -> Var.t -> Exp.t list -> (Sh.t, unit) result option