[sledge] Add abort instruction and use it for abort and llvm.trap

Summary:
There are two motivations for this:

1. Distinguish between `Unreachable`, which silently terminates
   execution a la `assume false`; and `Abort`, which vocally
   terminates execution a la `assert false`.

2. Distinguish between undefined functions, which have `Unreachable`
   bodies, and bomb functions such as:
   ```
   define void bomb() {
     tail call void llvm.trap()
     unreachable
   }
   ```

Reviewed By: ngorogiannis

Differential Revision: D15408246

fbshipit-source-id: b64354cdb

sledge/src/llair/frontend.ml

@@ -956,10 +956,10 @@ let xlate_instr :
           let src = xlate_value x (Llvm.operand instr 1) in
           let len = xlate_value x (Llvm.operand instr 2) in
           emit_inst (Llair.Inst.memmov ~dst ~src ~len ~loc)
+      | ["abort"] | ["llvm"; "trap"] -> emit_inst (Llair.Inst.abort ~loc)
       (* dropped / handled elsewhere *)
       | ["llvm"; "dbg"; ("declare" | "value")]
-       |"llvm" :: ("lifetime" | "invariant") :: ("start" | "end") :: _
+       |"llvm" :: ("lifetime" | "invariant") :: ("start" | "end") :: _ ->
-       |["llvm"; "trap"] ->
           nop ()
       (* unimplemented *)
       | ["llvm"; ("stacksave" | "stackrestore")] ->

sledge/src/llair/llair.ml

@@ -16,6 +16,7 @@ type inst =
   | Alloc of {reg: Var.t; num: Exp.t; len: Exp.t; loc: Loc.t}
   | Free of {ptr: Exp.t; loc: Loc.t}
   | Nondet of {reg: Var.t option; msg: string; loc: Loc.t}
+  | Abort of {loc: Loc.t}
 [@@deriving sexp]
 
 type cmnd = inst vector [@@deriving sexp]
@@ -135,6 +136,7 @@ let pp_inst fs inst =
   | Nondet {reg; msg; loc} ->
       pf "@[<2>nondet %a\"%s\";@]\t%a" (Option.pp "%a " Var.pp) reg msg
         Loc.pp loc
+  | Abort {loc} -> pf "@[<2>abort;@]\t%a" Loc.pp loc
 
 let pp_args pp_arg fs args =
   Format.fprintf fs "@ (@[%a@])" (List.pp ",@ " pp_arg) (List.rev args)
@@ -216,6 +218,7 @@ module Inst = struct
   let alloc ~reg ~num ~len ~loc = Alloc {reg; num; len; loc}
   let free ~ptr ~loc = Free {ptr; loc}
   let nondet ~reg ~msg ~loc = Nondet {reg; msg; loc}
+  let abort ~loc = Abort {loc}
 
   let loc = function
     | Load {loc}
@@ -225,14 +228,16 @@ module Inst = struct
      |Memmov {loc}
      |Alloc {loc}
      |Free {loc}
-     |Nondet {loc} ->
+     |Nondet {loc}
+     |Abort {loc} ->
         loc
 
   let union_locals inst vs =
     match inst with
     | Load {reg} | Alloc {reg} | Nondet {reg= Some reg} -> Set.add vs reg
-    | Store _ | Memcpy _ | Memmov _ | Memset _ | Free _ | Nondet {reg= None}
+    | Store _ | Memcpy _ | Memmov _ | Memset _ | Free _
-      ->
+     |Nondet {reg= None}
+     |Abort _ ->
         vs
 
   let locals inst = union_locals inst Var.Set.empty

sledge/src/llair/llair.mli

@@ -50,6 +50,7 @@ type inst = private
   | Nondet of {reg: Var.t option; msg: string; loc: Loc.t}
       (** Bind [reg] to an arbitrary value, representing non-deterministic
           approximation of behavior described by [msg]. *)
+  | Abort of {loc: Loc.t}  (** Trigger abnormal program termination *)
 
 (** A (straight-line) command is a sequence of instructions. *)
 type cmnd = inst vector
@@ -130,6 +131,7 @@ module Inst : sig
   val alloc : reg:Var.t -> num:Exp.t -> len:Exp.t -> loc:Loc.t -> inst
   val free : ptr:Exp.t -> loc:Loc.t -> inst
   val nondet : reg:Var.t option -> msg:string -> loc:Loc.t -> inst
+  val abort : loc:Loc.t -> inst
   val loc : inst -> Loc.t
   val locals : inst -> Var.Set.t
 end

sledge/src/symbheap/exec.ml

@@ -614,6 +614,7 @@ let inst : Sh.t -> Llair.inst -> (Sh.t, unit) result =
   | Alloc {reg; num; len} -> exec_spec pre (alloc_spec us reg num len)
   | Free {ptr} -> exec_spec pre (free_spec us ptr)
   | Nondet _ -> Ok pre
+  | Abort _ -> Error ()
 
 let skip : Sh.t -> (Sh.t, _) result option = fun pre -> Some (Ok pre)