[sledge] Change: Translate LLVM undef to register assigned by nondet

Summary:
Instead of relying on Exp.nondet to encode the semantics of LLVM's
undef, translate each to a per-function unique register, with a nondet
assignment to it prior to each use. This avoids the need for
Exp.nondet, which is ill-formed in the sense that expressions denote
values, not sets of values (with particular constraints on what ways
in which the choice must be angelic vs demonic). This change
essentially allows the backend to be sane, and makes it the frontend's
problem to deal with LLVM's undef.

This treatment, like the treatment based on Exp.nondet, is expected to
result in LLAIR code with different semantics of undef compared to the
semantics of LLVM described in the
[LangRef](https://llvm.org/docs/LangRef.html#undefined-values). In
particular, the LLVM LangRef states

> An ‘undef’ “variable” can arbitrarily change its value over its
> “live range”. This is true because the variable doesn’t actually
> have a live range. Instead, the value is logically read from
> arbitrary registers that happen to be around when needed, so the
> value is not necessarily consistent over time.

To model this ability of undef to arbitrarily change its value over
its live range, it is likely that additional nondet assignments would
need to be added. Exactly where it not currently known.

Reviewed By: jvillard

Differential Revision: D21720976

fbshipit-source-id: 90c2a0d26

sledge/bin/frontend.ml

@@ -331,6 +331,10 @@ let pp_prefix_exp fs (insts, exp) =
     (fun fs -> if List.is_empty insts then () else Format.fprintf fs "@ ")
     Exp.pp exp
 
+(* per-function count of 'undef' values, used to translate each occurrence
+   of 'undef' to a distinct register *)
+let undef_count = ref 0
+
 let memo_value : (bool * Llvm.llvalue, Inst.t list * Exp.t) Hashtbl.t =
   Hashtbl.Poly.create ()
 
@@ -456,7 +460,11 @@ and xlate_value ?(inline = false) stk :
         ([], Exp.label ~parent ~name)
     | UndefValue ->
         let typ = xlate_type x (Llvm.type_of llv) in
-        ([], Exp.nondet typ (Llvm.string_of_llvalue llv))
+        let name = sprintf "undef_%i" !undef_count in
+        let loc = Loc.none in
+        let reg = Reg.program typ name in
+        let msg = Llvm.string_of_llvalue llv in
+        ([Inst.nondet ~reg:(Some reg) ~msg ~loc], Exp.reg reg)
     | Instruction
         ( ( Trunc | ZExt | SExt | FPToUI | FPToSI | UIToFP | SIToFP
           | FPTrunc | FPExt | PtrToInt | IntToPtr | BitCast | AddrSpaceCast
@@ -714,7 +722,11 @@ and xlate_global stk : x -> Llvm.llvalue -> Global.t =
         | GlobalVariable ->
             Option.map (Llvm.global_initializer llg) ~f:(fun llv ->
                 let pre, init = xlate_value stk x llv in
-                if not (List.is_empty pre) then
+                (* Nondet insts to set up globals can be dropped to simply
+                   leave the undef regs unconstrained. Other insts to set up
+                   globals are currently not supported *)
+                let is_nondet = function Nondet _ -> true | _ -> false in
+                if not (List.for_all ~f:is_nondet pre) then
                   todo "global initializer instructions" () ;
                 (init, size_of x (Llvm.type_of llv)) )
         | _ -> None
@@ -1387,6 +1399,7 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func =
  fun x llf ->
   [%Trace.call fun {pf} -> pf "%a" pp_llvalue llf]
   ;
+  undef_count := 0 ;
   let name = xlate_global x llf in
   let formals =
     Llvm.fold_left_params