From dde116b04090e3a95418f78844047a8564a0a352 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 10 Jun 2020 07:05:30 -0700 Subject: [PATCH] [sledge] Change: Translate LLVM undef to register assigned by nondet MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/sledge/bin/frontend.ml b/sledge/bin/frontend.ml index b9cc1262a..0bbc68c52 100644 --- a/sledge/bin/frontend.ml +++ b/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