From 38cab376f6758fca90278fbcd6a5c61aece9c6c0 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 14 Oct 2019 00:54:05 -0700 Subject: [PATCH] [sledge] Keep BitCasts and similar in expressions Summary: While BitCasts are the identity function on the bitwise representation, they are not necessarily so in the semantics or the logical representation. So be more conservative about eliding them in the Exp language. Those that are actually semantic identities are still omitted in the Term language. Reviewed By: ngorogiannis Differential Revision: D17801950 fbshipit-source-id: bf9ae57b5 --- sledge/src/llair/frontend.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml index 01116c3cb..173f669a7 100644 --- a/sledge/src/llair/frontend.ml +++ b/sledge/src/llair/frontend.ml @@ -472,7 +472,6 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t = ( if Poly.equal (Llvm.classify_type (Llvm.type_of llv)) Vector then todo "vector operations: %a" pp_llvalue llv () ) in - let cast () = xlate_rand 0 in let convert ?unsigned () = let dst = Lazy.force typ in let rand = Llvm.operand llv 0 in @@ -490,7 +489,7 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t = Exp.or_ ~typ:Typ.bool (Exp.uno ?typ e f) (mk ?typ e f) ) in ( match opcode with - | AddrSpaceCast | BitCast -> cast () + | AddrSpaceCast | BitCast -> convert () | Trunc | ZExt | FPToUI | UIToFP | PtrToInt | IntToPtr -> convert ~unsigned:true () | SExt | FPTrunc | FPExt | FPToSI | SIToFP -> convert () @@ -578,7 +577,7 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t = if Poly.equal (Llvm.classify_type (Llvm.type_of llv)) Vector then todo "vector operations: %a" pp_llvalue llv () ; let len = Llvm.num_operands llv in - if len <= 1 then cast () + if len <= 1 then convert () else let rec xlate_indices i = [%Trace.call fun {pf} ->