pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[sledge] Revise program expressions

Browse Source 
Summary:
Revise program expressions based on the changed constraints now that
Term is separate from Exp. In particular:

- Add types to all application, indicating how the operation
  interprets its arguments

- Change to a simpler uncurried form

- Remove now-unneeded normalizations

Reviewed By: bennostein

Differential Revision: D17665236

fbshipit-source-id: 1bcf2efd6
master
Josh Berdine 5 years ago committed by Facebook Github Bot
parent 00639e15bb
commit e3f0ba8c54
7 changed files with 528 additions and 1192 deletions
Show Stats Download Patch File Download Diff File

8
sledge/src/control.ml
Unescape View File

@ -406,14 +406,16 @@ module Make (Dom : Domain_sig.Dom) = struct
| Switch {key; tbl; els} ->
Vector.fold tbl
~f:(fun x (case, jump) ->
match Dom.exec_assume state (Exp.eq key case) with
match Dom.exec_assume state (Exp.eq (Exp.typ key) key case) with
| Some state -> exec_jump stk state block jump |> Work.seq x
| None -> x )
~init:
( match
Dom.exec_assume state
(Vector.fold tbl ~init:(Exp.bool true)
~f:(fun b (case, _) -> Exp.and_ (Exp.dq key case) b))
~f:(fun b (case, _) ->
Exp.and_ Typ.bool (Exp.dq (Exp.typ key) key case) b
))
with
| Some state -> exec_jump stk state block els
| None -> Work.skip )
@ -421,7 +423,7 @@ module Make (Dom : Domain_sig.Dom) = struct
Vector.fold tbl ~init:Work.skip ~f:(fun x (jump : Llair.jump) ->
match
Dom.exec_assume state
(Exp.eq ptr
(Exp.eq Typ.ptr ptr
(Exp.label
~parent:(Reg.name jump.dst.parent.name.reg)
~name:jump.dst.lbl))

1183
sledge/src/llair/exp.ml
View File

File diff suppressed because it is too large Load Diff

143
sledge/src/llair/exp.mli
Unescape View File

@ -8,30 +8,15 @@
(** Expressions
Pure (heap-independent) expressions are complex arithmetic,
bitwise-logical, etc. operations over literal values and registers.
bitwise-logical, etc. operations over literal values and registers. *)
Expressions for operations that are uninterpreted in the analyzer are
represented in curried form, where [App] is an application of a function
symbol to an argument. This is done to simplify the definition of
'subexpression' and make it explicit. The specific constructor functions
indicate and check the expected arity of the function symbols. *)
type comparator_witness
type qset = (t, comparator_witness) Qset.t
type op1 =
| Convert of {dst: Typ.t; signed: bool}
(** Convert between specified types, possibly with loss of information *)
| Select of int (** Select an index from a record *)
[@@deriving compare, equal, hash, sexp]
and t = private
| Add of {args: qset; typ: Typ.t} (** Addition *)
| Mul of {args: qset; typ: Typ.t} (** Multiplication *)
| Reg of {name: string; global: bool}
(** Local variable / virtual register *)
| Nondet of {msg: string}
(** Anonymous register with arbitrary value, representing
non-deterministic approximation of value described by [msg] *)
| Label of {parent: string; name: string}
(** Address of named code block within parent function *)
| App of {op: t; arg: t}
(** Application of function symbol to argument, curried *)
type op2 =
| Eq (** Equal test *)
| Dq (** Disequal test *)
| Gt (** Greater-than test *)
@ -44,9 +29,12 @@ and t = private
| Ule (** Unsigned less-than-or-equal test *)
| Ord (** Ordered test (neither arg is nan) *)
| Uno (** Unordered test (some arg is nan) *)
| Add (** Addition *)
| Sub (** Subtraction *)
| Mul (** Multiplication *)
| Div (** Division *)
| Udiv (** Unsigned division *)
| Rem (** Remainder of division *)
| Udiv (** Unsigned division *)
| Urem (** Remainder of unsigned division *)
| And (** Conjunction, boolean or bitwise *)
| Or (** Disjunction, boolean or bitwise *)
@ -54,27 +42,42 @@ and t = private
| Shl (** Shift left, bitwise *)
| Lshr (** Logical shift right, bitwise *)
| Ashr (** Arithmetic shift right, bitwise *)
| Conditional (** If-then-else *)
| Update of int (** Constant record with updated index *)
[@@deriving compare, equal, hash, sexp]
type op3 = Conditional (** If-then-else *)
[@@deriving compare, equal, hash, sexp]
type opN =
| Record (** Record (array / struct) constant *)
| Select (** Select an index from a record *)
| Update (** Constant record with updated index *)
| Struct_rec of {elts: t vector}
| Struct_rec
(** Struct constant that may recursively refer to itself
(transitively) from [elts]. NOTE: represented by cyclic values. *)
| Convert of {signed: bool; dst: Typ.t; src: Typ.t}
(** Convert between specified types, possibly with loss of information *)
| Integer of {data: Z.t; typ: Typ.t}
(** Integer constant, or if [typ] is a [Pointer], null pointer value
that never refers to an object *)
| Float of {data: string} (** Floating-point constant *)
[@@deriving compare, equal, hash, sexp]
val comparator : (t, comparator_witness) Comparator.t
type t =
| Reg of {name: string; typ: Typ.t; global: bool} (** Virtual register *)
| Nondet of {msg: string; typ: Typ.t}
(** Anonymous register with arbitrary value, representing
non-deterministic approximation of value described by [msg] *)
| Label of {parent: string; name: string}
(** Address of named code block within parent function *)
| Integer of {data: Z.t; typ: Typ.t} (** Integer constant *)
| Float of {data: string; typ: Typ.t} (** Floating-point constant *)
| Ap1 of op1 * Typ.t * t
| Ap2 of op2 * Typ.t * t * t
| Ap3 of op3 * Typ.t * t * t * t
| ApN of opN * Typ.t * t vector
[@@deriving compare, equal, hash, sexp]
type exp = t
include Comparator.S with type t := t
val pp : t pp
include Invariant.S with type t := t
type exp = t
(** Exp.Reg is re-exported as Reg *)
module Reg : sig
type t = private exp [@@deriving compare, equal, hash, sexp]
@ -106,7 +109,7 @@ module Reg : sig
include Invariant.S with type t := t
val of_exp : exp -> t option
val program : ?global:unit -> string -> t
val program : ?global:unit -> Typ.t -> string -> t
val name : t -> string
val global : t -> bool
end
@ -114,47 +117,45 @@ end
(** Construct *)
val reg : Reg.t -> t
val nondet : string -> t
val nondet : Typ.t -> string -> t
val label : parent:string -> name:string -> t
val null : t
val bool : bool -> t
val integer : Z.t -> Typ.t -> t
val float : string -> t
val eq : t -> t -> t
val dq : t -> t -> t
val gt : t -> t -> t
val ge : t -> t -> t
val lt : t -> t -> t
val le : t -> t -> t
val ugt : t -> t -> t
val uge : t -> t -> t
val ult : t -> t -> t
val ule : t -> t -> t
val ord : t -> t -> t
val uno : t -> t -> t
val neg : Typ.t -> t -> t
val integer : Typ.t -> Z.t -> t
val float : Typ.t -> string -> t
val eq : Typ.t -> t -> t -> t
val dq : Typ.t -> t -> t -> t
val gt : Typ.t -> t -> t -> t
val ge : Typ.t -> t -> t -> t
val lt : Typ.t -> t -> t -> t
val le : Typ.t -> t -> t -> t
val ugt : Typ.t -> t -> t -> t
val uge : Typ.t -> t -> t -> t
val ult : Typ.t -> t -> t -> t
val ule : Typ.t -> t -> t -> t
val ord : Typ.t -> t -> t -> t
val uno : Typ.t -> t -> t -> t
val add : Typ.t -> t -> t -> t
val sub : Typ.t -> t -> t -> t
val mul : Typ.t -> t -> t -> t
val div : t -> t -> t
val udiv : t -> t -> t
val rem : t -> t -> t
val urem : t -> t -> t
val and_ : t -> t -> t
val or_ : t -> t -> t
val xor : t -> t -> t
val not_ : Typ.t -> t -> t
val shl : t -> t -> t
val lshr : t -> t -> t
val ashr : t -> t -> t
val conditional : cnd:t -> thn:t -> els:t -> t
val record : t list -> t
val select : rcd:t -> idx:t -> t
val update : rcd:t -> elt:t -> idx:t -> t
val div : Typ.t -> t -> t -> t
val rem : Typ.t -> t -> t -> t
val udiv : Typ.t -> t -> t -> t
val urem : Typ.t -> t -> t -> t
val and_ : Typ.t -> t -> t -> t
val or_ : Typ.t -> t -> t -> t
val xor : Typ.t -> t -> t -> t
val shl : Typ.t -> t -> t -> t
val lshr : Typ.t -> t -> t -> t
val ashr : Typ.t -> t -> t -> t
val conditional : Typ.t -> cnd:t -> thn:t -> els:t -> t
val record : Typ.t -> t vector -> t
val select : Typ.t -> t -> int -> t
val update : Typ.t -> rcd:t -> int -> elt:t -> t
val struct_rec :
(module Hashtbl.Key with type t = 'id)
-> (id:'id -> t lazy_t vector -> t) Staged.t
-> (id:'id -> Typ.t -> t lazy_t vector -> t) Staged.t
(** [struct_rec Id id element_thunks] constructs a possibly-cyclic [Struct]
value. Cycles are detected using [Id]. The caller of [struct_rec Id]
must ensure that a single unstaging of [struct_rec Id] is used for each
@ -163,10 +164,14 @@ val struct_rec :
one point on each cycle. Failure to obey these requirements will lead to
stack overflow. *)
val convert : ?signed:bool -> dst:Typ.t -> src:Typ.t -> t -> t
val convert : dst:Typ.t -> ?signed:bool -> src:Typ.t -> t -> t
(** Access *)
val fold_regs : t -> init:'a -> f:('a -> Reg.t -> 'a) -> 'a
(** Query *)
val is_true : t -> bool
val is_false : t -> bool
val typ : t -> Typ.t

213
sledge/src/llair/frontend.ml
Unescape View File

@ -281,21 +281,26 @@ let xlate_int : x -> Llvm.llvalue -> Exp.t =
| None ->
Z.of_string (suffix_after_last_space (Llvm.string_of_llvalue llv))
in
Exp.integer data typ
Exp.integer typ data
let xlate_float : Llvm.llvalue -> Exp.t =
fun llv ->
let xlate_float : x -> Llvm.llvalue -> Exp.t =
fun x llv ->
let llt = Llvm.type_of llv in
let typ = xlate_type x llt in
let data = suffix_after_last_space (Llvm.string_of_llvalue llv) in
Exp.float data
Exp.float typ data
let xlate_name ?global : Llvm.llvalue -> Reg.t =
fun llv -> Reg.program ?global (find_name llv)
let xlate_name x ?global : Llvm.llvalue -> Reg.t =
fun llv ->
let typ = xlate_type x (Llvm.type_of llv) in
Reg.program ?global typ (find_name llv)
let xlate_name_opt : Llvm.llvalue -> Reg.t option =
fun instr ->
match Llvm.classify_type (Llvm.type_of instr) with
let xlate_name_opt : x -> Llvm.llvalue -> Reg.t option =
fun x instr ->
let llt = Llvm.type_of instr in
match Llvm.classify_type llt with
| Void -> None
| _ -> Some (xlate_name instr)
| _ -> Some (xlate_name x instr)
let memo_value : (bool * Llvm.llvalue, Exp.t) Hashtbl.t =
Hashtbl.Poly.create ()
@ -326,12 +331,12 @@ let ptr_fld x ~ptr ~fld ~lltyp =
let offset =
Llvm_target.DataLayout.offset_of_element lltyp fld x.lldatalayout
in
Exp.add Typ.ptr ptr (Exp.integer (Z.of_int64 offset) Typ.siz)
Exp.add Typ.ptr ptr (Exp.integer Typ.siz (Z.of_int64 offset))
let ptr_idx x ~ptr ~idx ~llelt =
let stride = Llvm_target.DataLayout.abi_size llelt x.lldatalayout in
Exp.add Typ.ptr ptr
(Exp.mul Typ.siz (Exp.integer (Z.of_int64 stride) Typ.siz) idx)
(Exp.mul Typ.siz (Exp.integer Typ.siz (Z.of_int64 stride)) idx)
let xlate_llvm_eh_typeid_for : x -> Typ.t -> Exp.t -> Exp.t =
fun x typ arg -> Exp.convert ~dst:(i32 x) ~src:typ arg
@ -358,28 +363,32 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Exp.t =
let fname = Llvm.value_name func in
match xlate_intrinsic_exp fname with
| Some intrinsic when inline || should_inline llv -> intrinsic x llv
| _ -> Exp.reg (xlate_name llv) )
| _ -> Exp.reg (xlate_name x llv) )
| Instruction (Invoke | Alloca | Load | PHI | LandingPad | VAArg)
|Argument ->
Exp.reg (xlate_name llv)
Exp.reg (xlate_name x llv)
| Function | GlobalVariable -> Exp.reg (xlate_global x llv).reg
| GlobalAlias -> xlate_value x (Llvm.operand llv 0)
| ConstantInt -> xlate_int x llv
| ConstantFP -> xlate_float llv
| ConstantFP -> xlate_float x llv
| ConstantPointerNull | ConstantAggregateZero -> Exp.null
| ConstantVector | ConstantArray ->
let typ = xlate_type x (Llvm.type_of llv) in
let len = Llvm.num_operands llv in
let f i = xlate_value x (Llvm.operand llv i) in
Exp.record (List.init len ~f)
Exp.record typ (Vector.init len ~f)
| ConstantDataVector ->
let typ = xlate_type x (Llvm.type_of llv) in
let len = Llvm.vector_size (Llvm.type_of llv) in
let f i = xlate_value x (Llvm.const_element llv i) in
Exp.record (List.init len ~f)
Exp.record typ (Vector.init len ~f)
| ConstantDataArray ->
let typ = xlate_type x (Llvm.type_of llv) in
let len = Llvm.array_length (Llvm.type_of llv) in
let f i = xlate_value x (Llvm.const_element llv i) in
Exp.record (List.init len ~f)
Exp.record typ (Vector.init len ~f)
| ConstantStruct ->
let typ = xlate_type x (Llvm.type_of llv) in
let is_recursive =
Llvm.fold_left_uses
(fun b use -> b || llv == Llvm.used_value use)
@ -390,16 +399,18 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Exp.t =
Vector.init (Llvm.num_operands llv) ~f:(fun i ->
lazy (xlate_value x (Llvm.operand llv i)) )
in
struct_rec ~id:llv elt_thks
struct_rec ~id:llv typ elt_thks
else
Exp.record
(List.init (Llvm.num_operands llv) ~f:(fun i ->
Exp.record typ
(Vector.init (Llvm.num_operands llv) ~f:(fun i ->
xlate_value x (Llvm.operand llv i) ))
| BlockAddress ->
let parent = find_name (Llvm.operand llv 0) in
let name = find_name (Llvm.operand llv 1) in
Exp.label ~parent ~name
| UndefValue -> Exp.nondet (Llvm.string_of_llvalue llv)
| UndefValue ->
let typ = xlate_type x (Llvm.type_of llv) in
Exp.nondet typ (Llvm.string_of_llvalue llv)
| Instruction
( ( Trunc | ZExt | SExt | FPToUI | FPToSI | UIToFP | SIToFP
| FPTrunc | FPExt | PtrToInt | IntToPtr | BitCast | AddrSpaceCast
@ -408,7 +419,7 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Exp.t =
| Select | GetElementPtr | ExtractElement | InsertElement
| ShuffleVector | ExtractValue | InsertValue ) as opcode ) ->
if inline || should_inline llv then xlate_opcode x llv opcode
else Exp.reg (xlate_name llv)
else Exp.reg (xlate_name x llv)
| ConstantExpr -> xlate_opcode x llv (Llvm.constexpr_opcode llv)
| GlobalIFunc -> todo "ifuncs: %a" pp_llvalue llv ()
| Instruction (CatchPad | CleanupPad | CatchSwitch) ->
@ -433,21 +444,26 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
;
let xlate_rand i = xlate_value x (Llvm.operand llv i) in
let typ = lazy (xlate_type x (Llvm.type_of llv)) in
let check_vector =
lazy
( 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 signed =
let rand = Llvm.operand llv 0 in
let dst = Lazy.force typ in
let rand = Llvm.operand llv 0 in
let src = xlate_type x (Llvm.type_of rand) in
let arg = xlate_value x rand in
Exp.convert ~signed ~dst ~src arg
Exp.convert ~dst ~signed ~src arg
in
let binary mk =
if Poly.equal (Llvm.classify_type (Llvm.type_of llv)) Vector then
todo "vector operations: %a" pp_llvalue llv () ;
mk (xlate_rand 0) (xlate_rand 1)
Lazy.force check_vector ;
let typ = xlate_type x (Llvm.type_of (Llvm.operand llv 0)) in
mk typ (xlate_rand 0) (xlate_rand 1)
in
let unordered_or mk =
binary (fun x y -> Exp.or_ (Exp.uno x y) (mk x y))
binary (fun typ e f -> Exp.or_ Typ.bool (Exp.uno typ e f) (mk typ e f))
in
( match opcode with
| AddrSpaceCast | BitCast -> cast ()
@ -469,7 +485,7 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
| Ule -> binary Exp.ule )
| FCmp -> (
match Llvm.fcmp_predicate llv with
| None | Some False -> binary (fun _ _ -> Exp.bool false)
| None | Some False -> binary (fun _ _ _ -> Exp.bool false)
| Some Oeq -> binary Exp.eq
| Some Ogt -> binary Exp.gt
| Some Oge -> binary Exp.ge
@ -484,10 +500,10 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
| Some Ult -> unordered_or Exp.lt
| Some Ule -> unordered_or Exp.le
| Some Une -> unordered_or Exp.dq
| Some True -> binary (fun _ _ -> Exp.bool true) )
| Add | FAdd -> binary (Exp.add (Lazy.force typ))
| Sub | FSub -> binary (Exp.sub (Lazy.force typ))
| Mul | FMul -> binary (Exp.mul (Lazy.force typ))
| Some True -> binary (fun _ _ _ -> Exp.bool true) )
| Add | FAdd -> binary Exp.add
| Sub | FSub -> binary Exp.sub
| Mul | FMul -> binary Exp.mul
| SDiv | FDiv -> binary Exp.div
| UDiv -> binary Exp.udiv
| SRem | FRem -> binary Exp.rem
@ -499,25 +515,27 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
| Or -> binary Exp.or_
| Xor -> binary Exp.xor
| Select ->
Exp.conditional ~cnd:(xlate_rand 0) ~thn:(xlate_rand 1)
let typ = xlate_type x (Llvm.type_of (Llvm.operand llv 1)) in
Exp.conditional typ ~cnd:(xlate_rand 0) ~thn:(xlate_rand 1)
~els:(xlate_rand 2)
| ExtractElement -> Exp.select ~rcd:(xlate_rand 0) ~idx:(xlate_rand 1)
| InsertElement ->
Exp.update ~rcd:(xlate_rand 0) ~elt:(xlate_rand 1) ~idx:(xlate_rand 2)
| ExtractElement | InsertElement ->
todo "vector operations: %a" pp_llvalue llv ()
| ExtractValue | InsertValue ->
let agg = xlate_rand 0 in
let typ = xlate_type x (Llvm.type_of (Llvm.operand llv 0)) in
let indices = Llvm.indices llv in
let num = Array.length indices in
let rec xlate_indices i rcd =
let rcd_i, upd =
match typ with
| Tuple _ | Struct _ ->
let idx = Exp.integer (Z.of_int indices.(i)) Typ.siz in
(Exp.select ~rcd ~idx, Exp.update ~rcd ~idx)
| Array _ ->
let idx = Exp.integer (Z.of_int indices.(i)) Typ.siz in
(Exp.select ~rcd ~idx, Exp.update ~rcd ~idx)
let rec xlate_indices i rcd typ =
let rcd_i, typ_i, upd =
match (typ : Typ.t) with
| Tuple {elts} | Struct {elts} ->
( Exp.select typ rcd indices.(i)
, Vector.get elts indices.(i)
, Exp.update typ ~rcd indices.(i) )
| Array {elt} ->
( Exp.select typ rcd indices.(i)
, elt
, Exp.update typ ~rcd indices.(i) )
| _ -> fail "xlate_value: %a" pp_llvalue llv ()
in
let update_or_return elt ret =
@ -526,13 +544,13 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t =
| ExtractValue -> ret
in
if i < num - 1 then
let elt = xlate_indices (i + 1) rcd_i in
let elt = xlate_indices (i + 1) rcd_i typ_i in
update_or_return (lazy elt) elt
else
let elt = lazy (xlate_rand 1) in
update_or_return elt rcd_i
in
xlate_indices 0 agg
xlate_indices 0 agg typ
| GetElementPtr ->
if Poly.equal (Llvm.classify_type (Llvm.type_of llv)) Vector then
todo "vector operations: %a" pp_llvalue llv () ;
@ -604,7 +622,7 @@ and xlate_global : x -> Llvm.llvalue -> Global.t =
Hashtbl.find_or_add memo_global llg ~default:(fun () ->
[%Trace.call fun {pf} -> pf "%a" pp_llvalue llg]
;
let g = xlate_name ~global:() llg in
let g = xlate_name x ~global:() llg in
let llt = Llvm.type_of llg in
let typ = xlate_type x llt in
let loc = find_loc llg in
@ -629,13 +647,13 @@ and xlate_global : x -> Llvm.llvalue -> Global.t =
type pop_thunk = Loc.t -> Llair.inst list
let pop_stack_frame_of_function :
Llvm.llvalue -> Llvm.llbasicblock -> pop_thunk =
fun func entry_blk ->
x -> Llvm.llvalue -> Llvm.llbasicblock -> pop_thunk =
fun x func entry_blk ->
let append_stack_regs blk regs =
Llvm.fold_right_instrs
(fun instr regs ->
match Llvm.instr_opcode instr with
| Alloca -> xlate_name instr :: regs
| Alloca -> xlate_name x instr :: regs
| _ -> regs )
blk regs
in
@ -686,6 +704,12 @@ let landingpad_typs : x -> Llvm.llvalue -> Typ.t * Typ.t * Llvm.lltype =
let cxa_exception = Llvm.struct_type llcontext [|tip; dtor|] in
(i32, xlate_type x tip, cxa_exception)
let exception_typs =
let pi8 = Typ.pointer ~elt:(Typ.integer ~bits:8) in
let i32 = Typ.integer ~bits:32 in
let exc = Typ.tuple ~packed:false (Vector.of_array [|pi8; i32|]) in
(pi8, i32, exc)
(** Translate a control transfer from instruction [instr] to block [dst] to
a jump, if necessary by extending [blocks] with a trampoline containing
the PHIs of [dst] translated to a move. *)
@ -708,7 +732,7 @@ let xlate_jump :
List.find_map_exn (Llvm.incoming dst_instr)
~f:(fun (arg, pred) ->
if Poly.equal pred src then
Some (xlate_name dst_instr, xlate_value x arg)
Some (xlate_name x dst_instr, xlate_value x arg)
else None )
in
xlate_jump_ (reg_exp :: reg_exps) (Llvm.instr_succ dst_instr)
@ -754,7 +778,7 @@ let pp_code fs (insts, term, blocks) =
let rec xlate_func_name x llv =
match Llvm.classify_value llv with
| Function -> Exp.reg (xlate_name ~global:() llv)
| Function -> Exp.reg (xlate_name x ~global:() llv)
| ConstantExpr -> xlate_opcode x llv (Llvm.constexpr_opcode llv)
| Argument | Instruction _ -> xlate_value x llv
| GlobalAlias -> xlate_func_name x (Llvm.operand llv 0)
@ -794,7 +818,7 @@ let xlate_instr :
let inline_or_move xlate =
if should_inline instr then nop ()
else
let reg = xlate_name instr in
let reg = xlate_name x instr in
let exp = xlate instr in
let reg_exps = Vector.of_array [|(reg, exp)|] in
emit_inst (Llair.Inst.move ~reg_exps ~loc)
@ -802,20 +826,19 @@ let xlate_instr :
let opcode = Llvm.instr_opcode instr in
match opcode with
| Load ->
let reg = xlate_name instr in
let len =
Exp.integer (Z.of_int (size_of x (Llvm.type_of instr))) Typ.siz
in
let reg = xlate_name x instr in
let llt = Llvm.type_of instr in
let len = Exp.integer Typ.siz (Z.of_int (size_of x llt)) in
let ptr = xlate_value x (Llvm.operand instr 0) in
emit_inst (Llair.Inst.load ~reg ~ptr ~len ~loc)
| Store ->
let exp = xlate_value x (Llvm.operand instr 0) in
let llt = Llvm.type_of (Llvm.operand instr 0) in
let len = Exp.integer (Z.of_int (size_of x llt)) Typ.siz in
let len = Exp.integer Typ.siz (Z.of_int (size_of x llt)) in
let ptr = xlate_value x (Llvm.operand instr 1) in
emit_inst (Llair.Inst.store ~ptr ~exp ~len ~loc)
| Alloca ->
let reg = xlate_name instr in
let reg = xlate_name x instr in
let rand = Llvm.operand instr 0 in
let num =
Exp.convert ~dst:Typ.siz
@ -824,7 +847,7 @@ let xlate_instr :
in
assert (Poly.(Llvm.classify_type (Llvm.type_of instr) = Pointer)) ;
let llt = Llvm.element_type (Llvm.type_of instr) in
let len = Exp.integer (Z.of_int (size_of x llt)) Typ.siz in
let len = Exp.integer Typ.siz (Z.of_int (size_of x llt)) in
emit_inst (Llair.Inst.alloc ~reg ~num ~len ~loc)
| Call -> (
let llfunc =
@ -852,7 +875,7 @@ let xlate_instr :
( match Hash_set.strict_add ignored_callees fname with
| Ok () -> warn "ignoring uninterpreted %s %s" msg fname ()
| Error _ -> () ) ;
let reg = xlate_name_opt instr in
let reg = xlate_name_opt x instr in
emit_inst (Llair.Inst.nondet ~reg ~msg:fname ~loc)
in
(* intrinsics *)
@ -864,22 +887,22 @@ let xlate_instr :
let exc = xlate_value x (Llvm.operand instr 0) in
emit_term ~prefix:(pop loc) (Llair.Term.throw ~exc ~loc)
| ["__llair_alloc" (* void* __llair_alloc(unsigned size) *)] ->
let reg = xlate_name instr in
let reg = xlate_name x instr in
let num_operand = Llvm.operand instr 0 in
let num =
Exp.convert ~dst:Typ.siz
(xlate_value x num_operand)
~src:(xlate_type x (Llvm.type_of num_operand))
in
let len = Exp.integer (Z.of_int 1) Typ.siz in
let len = Exp.integer Typ.siz (Z.of_int 1) in
emit_inst (Llair.Inst.alloc ~reg ~num ~len ~loc)
| ["_Znwm" (* operator new(size_t num) *)]
|[ "_ZnwmSt11align_val_t"
(* operator new(unsigned long, std::align_val_t) *) ] ->
let reg = xlate_name instr in
let reg = xlate_name x instr in
let num = xlate_value x (Llvm.operand instr 0) in
let llt = Llvm.type_of instr in
let len = Exp.integer (Z.of_int (size_of x llt)) Typ.siz in
let len = Exp.integer Typ.siz (Z.of_int (size_of x llt)) in
emit_inst (Llair.Inst.alloc ~reg ~num ~len ~loc)
| ["_ZdlPv" (* operator delete(void* ptr) *)]
|[ "_ZdlPvSt11align_val_t"
@ -947,7 +970,7 @@ let xlate_instr :
List.rev_init num_args ~f:(fun i ->
xlate_value x (Llvm.operand instr i) )
in
let areturn = xlate_name_opt instr in
let areturn = xlate_name_opt x instr in
let return = Llair.Jump.mk lbl in
Llair.Term.call ~func ~typ ~args ~areturn ~return ~throw:None
~loc
@ -977,7 +1000,7 @@ let xlate_instr :
List.rev_init num_args ~f:(fun i ->
xlate_value x (Llvm.operand instr i) )
in
let areturn = xlate_name_opt instr in
let areturn = xlate_name_opt x instr in
(* intrinsics *)
match String.split fname ~on:'.' with
| _ when Option.is_some (xlate_intrinsic_exp fname) ->
@ -992,10 +1015,10 @@ let xlate_instr :
|[ "_ZnwmSt11align_val_t"
(* operator new(unsigned long num, std::align_val_t) *) ]
when num_args > 0 ->
let reg = xlate_name instr in
let reg = xlate_name x instr in
let num = xlate_value x (Llvm.operand instr 0) in
let llt = Llvm.type_of instr in
let len = Exp.integer (Z.of_int (size_of x llt)) Typ.siz in
let len = Exp.integer Typ.siz (Z.of_int (size_of x llt)) in
let dst, blocks = xlate_jump x instr return_blk loc [] in
emit_term
~prefix:[Llair.Inst.alloc ~reg ~num ~len ~loc]
@ -1077,29 +1100,30 @@ let xlate_instr :
passing a value for the selector which the handler code tests to
e.g. either cleanup or rethrow. *)
let i32, tip, cxa_exception = landingpad_typs x instr in
let exc = Exp.reg (Reg.program (find_name instr ^ ".exc")) in
let ti = Reg.program (name ^ ".ti") in
let pi8, _, exc_typ = exception_typs in
let exc = Exp.reg (Reg.program pi8 (find_name instr ^ ".exc")) in
let ti = Reg.program tip (name ^ ".ti") in
(* std::type_info* ti = ((__cxa_exception* )exc - 1)->exceptionType *)
let load_ti =
let typ = cxa_exception in
(* field number of the exceptionType member of __cxa_exception *)
let fld = 0 in
(* index from exc that points to header *)
let idx = Exp.integer Z.minus_one Typ.siz in
let idx = Exp.integer Typ.siz Z.minus_one in
let ptr =
ptr_fld x
~ptr:(ptr_idx x ~ptr:exc ~idx ~llelt:typ)
~fld ~lltyp:typ
in
let len = Exp.integer (Z.of_int (size_of x typ)) Typ.siz in
let len = Exp.integer Typ.siz (Z.of_int (size_of x typ)) in
Llair.Inst.load ~reg:ti ~ptr ~len ~loc
in
let ti = Exp.reg ti in
let typeid = xlate_llvm_eh_typeid_for x tip ti in
let lbl = name ^ ".unwind" in
let param = xlate_name instr in
let param = xlate_name x instr in
let jump_unwind i sel rev_blocks =
let arg = Exp.record [exc; sel] in
let arg = Exp.record exc_typ (Vector.of_array [|exc; sel|]) in
let mov =
Llair.Inst.move ~reg_exps:(Vector.of_array [|(param, arg)|]) ~loc
in
@ -1117,7 +1141,7 @@ let xlate_instr :
in
let term_unwind, rev_blocks =
if Llvm.is_cleanup instr then
goto_unwind 0 (Exp.integer Z.zero i32) []
goto_unwind 0 (Exp.integer i32 Z.zero) []
else
let num_clauses = Llvm.num_operands instr in
let lbl i = name ^ "." ^ Int.to_string i in
@ -1127,7 +1151,7 @@ let xlate_instr :
in
let match_filter i rev_blocks =
jump_unwind i
(Exp.sub i32 (Exp.integer Z.zero i32) typeid)
(Exp.sub i32 (Exp.integer i32 Z.zero) typeid)
rev_blocks
in
let xlate_clause i rev_blocks =
@ -1144,8 +1168,9 @@ let xlate_instr :
let rec xlate_filter i =
let tiI = xlate_value x (Llvm.operand clause i) in
if i < num_tis - 1 then
Exp.and_ (Exp.dq tiI ti) (xlate_filter (i + 1))
else Exp.dq tiI ti
Exp.and_ Typ.bool (Exp.dq tip tiI ti)
(xlate_filter (i + 1))
else Exp.dq tip tiI ti
in
let key = xlate_filter 0 in
let nzero, rev_blocks = match_filter i rev_blocks in
@ -1153,9 +1178,12 @@ let xlate_instr :
, rev_blocks )
| _ -> fail "xlate_instr: %a" pp_llvalue instr () )
| _ (* catch *) ->
let typ = xlate_type x (Llvm.type_of clause) in
let clause = xlate_value x clause in
let key =
Exp.or_ (Exp.eq clause Exp.null) (Exp.eq clause ti)
Exp.or_ Typ.bool
(Exp.eq typ clause Exp.null)
(Exp.eq typ clause ti)
in
let nzero, rev_blocks = jump_unwind i typeid rev_blocks in
( Llair.Term.branch ~loc ~key ~nzero ~zero:(jump (i + 1))
@ -1175,8 +1203,10 @@ let xlate_instr :
, List.rev_append rev_blocks
[Llair.Block.mk ~lbl ~cmnd:(Vector.of_list insts) ~term] ) )
| Resume ->
let rcd = xlate_value x (Llvm.operand instr 0) in
let exc = Exp.select ~rcd ~idx:(Exp.integer Z.zero Typ.siz) in
let llrcd = Llvm.operand instr 0 in
let typ = xlate_type x (Llvm.type_of llrcd) in
let rcd = xlate_value x llrcd in
let exc = Exp.select typ rcd 0 in
emit_term ~prefix:(pop loc) (Llair.Term.throw ~exc ~loc)
| Unreachable -> emit_term Llair.Term.unreachable
| Trunc | ZExt | SExt | FPToUI | FPToSI | UIToFP | SIToFP | FPTrunc
@ -1187,7 +1217,7 @@ let xlate_instr :
|ExtractValue | InsertValue ->
inline_or_move (xlate_value ~inline:true x)
| VAArg ->
let reg = xlate_name_opt instr in
let reg = xlate_name_opt x instr in
warn "variadic function argument: %a" Loc.pp loc () ;
emit_inst (Llair.Inst.nondet ~reg ~msg:"vaarg" ~loc)
| CleanupRet | CatchRet | CatchPad | CleanupPad | CatchSwitch ->
@ -1240,19 +1270,20 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func =
let name = xlate_global x llf in
let params =
Llvm.fold_left_params
(fun rev_args param -> xlate_name param :: rev_args)
(fun rev_args param -> xlate_name x param :: rev_args)
[] llf
in
let freturn =
match name.typ with
| Pointer {elt= Function {return= Some _; _}} ->
Some (Reg.program "freturn")
| Pointer {elt= Function {return= Some typ; _}} ->
Some (Reg.program typ "freturn")
| _ -> None
in
let fthrow = Reg.program "fthrow" in
let _, _, exc_typ = exception_typs in
let fthrow = Reg.program exc_typ "fthrow" in
( match Llvm.block_begin llf with
| Before entry_blk ->
let pop = pop_stack_frame_of_function llf entry_blk in
let pop = pop_stack_frame_of_function x llf entry_blk in
let[@warning "p"] (entry_block :: entry_blocks) =
xlate_block pop x entry_blk
in

2
sledge/src/llair/llair.ml
Unescape View File

@ -219,8 +219,8 @@ let rec dummy_block =
; sort_index= 0 }
and dummy_func =
let dummy_reg = Reg.program ~global:() "dummy" in
let dummy_ptr_typ = Typ.pointer ~elt:(Typ.opaque ~name:"dummy") in
let dummy_reg = Reg.program ~global:() dummy_ptr_typ "dummy" in
{ name= Global.mk dummy_reg dummy_ptr_typ Loc.none
; params= []
; freturn= None

164
sledge/src/symbheap/term.ml
Unescape View File

@ -21,29 +21,12 @@ module Z = struct
let clamp_bop ~signed bits op x y =
clamp ~signed bits (op (clamp ~signed bits x) (clamp ~signed bits y))
let beq ~bits x y = clamp_cmp ~signed:true bits Z.equal x y
let bleq ~bits x y = clamp_cmp ~signed:true bits Z.leq x y
let bgeq ~bits x y = clamp_cmp ~signed:true bits Z.geq x y
let blt ~bits x y = clamp_cmp ~signed:true bits Z.lt x y
let bgt ~bits x y = clamp_cmp ~signed:true bits Z.gt x y
let buleq ~bits x y = clamp_cmp ~signed:false bits Z.leq x y
let bugeq ~bits x y = clamp_cmp ~signed:false bits Z.geq x y
let bult ~bits x y = clamp_cmp ~signed:false bits Z.lt x y
let bugt ~bits x y = clamp_cmp ~signed:false bits Z.gt x y
let bsub ~bits x y = clamp_bop ~signed:true bits Z.sub x y
let bmul ~bits x y = clamp_bop ~signed:true bits Z.mul x y
let bdiv ~bits x y = clamp_bop ~signed:true bits Z.div x y
let brem ~bits x y = clamp_bop ~signed:true bits Z.rem x y
let budiv ~bits x y = clamp_bop ~signed:false bits Z.div x y
let burem ~bits x y = clamp_bop ~signed:false bits Z.rem x y
let blogand ~bits x y = clamp_bop ~signed:true bits Z.logand x y
let blogor ~bits x y = clamp_bop ~signed:true bits Z.logor x y
let blogxor ~bits x y = clamp_bop ~signed:true bits Z.logxor x y
let bshift_left ~bits z i = Z.shift_left (clamp bits ~signed:true z) i
let bshift_right ~bits z i = Z.shift_right (clamp bits ~signed:true z) i
let bshift_right_trunc ~bits z i =
Z.shift_right_trunc (clamp bits ~signed:true z) i
end
module rec T : sig
@ -488,14 +471,6 @@ let invariant ?(partial = false) e =
assert (not (Vector.is_empty elts)) ;
assert_arity 0
let bits_of_int term =
match term with
| Integer {typ} -> (
match Typ.prim_bit_size_of typ with
| Some bits -> bits
| None -> violates invariant term )
| _ -> fail "bits_of_int" ()
(** Variables are the terms constructed by [Var] *)
module Var = struct
include T
@ -665,8 +640,7 @@ let simp_convert signed (dst : Typ.t) src arg =
let simp_gt x y =
match (x, y) with
| Integer {data= i}, Integer {data= j; typ= Integer {bits}} ->
bool (Z.bgt ~bits i j)
| Integer {data= i}, Integer {data= j} -> bool (Z.gt i j)
| _ -> App {op= App {op= Gt; arg= x}; arg= y}
let simp_ugt x y =
@ -677,8 +651,7 @@ let simp_ugt x y =
let simp_ge x y =
match (x, y) with
| Integer {data= i}, Integer {data= j; typ= Integer {bits}} ->
bool (Z.bgeq ~bits i j)
| Integer {data= i}, Integer {data= j} -> bool (Z.geq i j)
| _ -> App {op= App {op= Ge; arg= x}; arg= y}
let simp_uge x y =
@ -689,8 +662,7 @@ let simp_uge x y =
let simp_lt x y =
match (x, y) with
| Integer {data= i}, Integer {data= j; typ= Integer {bits}} ->
bool (Z.blt ~bits i j)
| Integer {data= i}, Integer {data= j} -> bool (Z.lt i j)
| _ -> App {op= App {op= Lt; arg= x}; arg= y}
let simp_ult x y =
@ -701,8 +673,7 @@ let simp_ult x y =
let simp_le x y =
match (x, y) with
| Integer {data= i}, Integer {data= j; typ= Integer {bits}} ->
bool (Z.bleq ~bits i j)
| Integer {data= i}, Integer {data= j} -> bool (Z.leq i j)
| _ -> App {op= App {op= Le; arg= x}; arg= y}
let simp_ule x y =
@ -729,18 +700,13 @@ let rec sum_to_term typ sum =
| _ -> Add {typ; args= sum} )
| _ -> Add {typ; args= sum}
and rational Q.{num; den} typ =
let bits = Option.value_exn (Typ.prim_bit_size_of typ) in
simp_div
(integer (Z.clamp ~signed:true bits num) typ)
(integer (Z.clamp ~signed:true bits den) typ)
and rational Q.{num; den} typ = simp_div (integer num typ) (integer den typ)
and simp_div x y =
match (x, y) with
(* i / j *)
| Integer {data= i; typ}, Integer {data= j} when not (Z.equal Z.zero j) ->
let bits = Option.value_exn (Typ.prim_bit_size_of typ) in
integer (Z.bdiv ~bits i j) typ
integer (Z.div i j) typ
(* e / 1 ==> e *)
| e, Integer {data} when Z.equal Z.one data -> e
(* (∑ᵢ cᵢ × Xᵢ) / z ==> ∑ᵢ cᵢ/z × Xᵢ *)
@ -762,8 +728,7 @@ let simp_rem x y =
match (x, y) with
(* i % j *)
| Integer {data= i; typ}, Integer {data= j} when not (Z.equal Z.zero j) ->
let bits = Option.value_exn (Typ.prim_bit_size_of typ) in
integer (Z.brem ~bits i j) typ
integer (Z.rem i j) typ
(* e % 1 ==> 0 *)
| _, Integer {data; typ} when Z.equal Z.one data -> integer Z.zero typ
| _ -> App {op= App {op= Rem; arg= x}; arg= y}
@ -842,8 +807,7 @@ end
let rec simp_mul2 typ e f =
match (e, f) with
(* c₁ × c₂ ==> c₁×c₂ *)
| Integer {data= i}, Integer {data= j} ->
integer (Z.bmul ~bits:(bits_of_int e) i j) typ
| Integer {data= i}, Integer {data= j} -> integer (Z.mul i j) typ
(* 0 × f ==> 0 *)
| Integer {data}, _ when Z.equal Z.zero data -> e
(* e × 0 ==> 0 *)
@ -889,9 +853,7 @@ let simp_negate typ x = simp_mul2 typ (minus_one typ) x
let simp_sub typ x y =
match (x, y) with
(* i - j *)
| Integer {data= i}, Integer {data= j} ->
let bits = Option.value_exn (Typ.prim_bit_size_of typ) in
integer (Z.bsub ~bits i j) typ
| Integer {data= i}, Integer {data= j} -> integer (Z.sub i j) typ
(* x - y ==> x + (-1 * y) *)
| _ -> simp_add2 typ x (simp_negate typ y)
@ -907,9 +869,7 @@ let simp_cond cnd thn els =
let rec simp_and x y =
match (x, y) with
(* i && j *)
| Integer {data= i; typ}, Integer {data= j} ->
let bits = Option.value_exn (Typ.prim_bit_size_of typ) in
integer (Z.blogand ~bits i j) typ
| Integer {data= i; typ}, Integer {data= j} -> integer (Z.logand i j) typ
(* e && true ==> e *)
| Integer {data; typ= Integer {bits= 1}}, e
|e, Integer {data; typ= Integer {bits= 1}}
@ -931,9 +891,7 @@ let rec simp_and x y =
let rec simp_or x y =
match (x, y) with
(* i || j *)
| Integer {data= i; typ}, Integer {data= j} ->
let bits = Option.value_exn (Typ.prim_bit_size_of typ) in
integer (Z.blogor ~bits i j) typ
| Integer {data= i; typ}, Integer {data= j} -> integer (Z.logor i j) typ
(* e || true ==> true *)
| (Integer {data; typ= Integer {bits= 1}} as t), _
|_, (Integer {data; typ= Integer {bits= 1}} as t)
@ -996,10 +954,8 @@ let rec simp_not (typ : Typ.t) term =
and simp_eq x y =
match (x, y) with
| Integer {data= i; typ}, Integer {data= j} ->
let bits = Option.value_exn (Typ.prim_bit_size_of typ) in
(* i = j *)
bool (Z.beq ~bits i j)
(* i = j *)
| Integer {data= i}, Integer {data= j} -> bool (Z.equal i j)
(* b = false ==> ¬b *)
| b, Integer {data} when Z.is_false data && is_boolean b ->
simp_not Typ.bool b
@ -1031,9 +987,7 @@ and simp_dq x y =
let simp_xor x y =
match (x, y) with
(* i xor j *)
| Integer {data= i; typ}, Integer {data= j} ->
let bits = Option.value_exn (Typ.prim_bit_size_of typ) in
integer (Z.blogxor ~bits i j) typ
| Integer {data= i; typ}, Integer {data= j} -> integer (Z.logxor i j) typ
(* true xor b ==> ¬b *)
| Integer {data}, b when Z.is_true data && is_boolean b ->
simp_not Typ.bool b
@ -1046,7 +1000,7 @@ let simp_shl x y =
(* i shl j *)
| Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j}
when Z.sign j >= 0 && Z.lt j (Z.of_int bits) ->
integer (Z.bshift_left ~bits i (Z.to_int j)) typ
integer (Z.shift_left i (Z.to_int j)) typ
(* e shl 0 ==> e *)
| e, Integer {data} when Z.equal Z.zero data -> e
| _ -> App {op= App {op= Shl; arg= x}; arg= y}
@ -1056,7 +1010,7 @@ let simp_lshr x y =
(* i lshr j *)
| Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j}
when Z.sign j >= 0 && Z.lt j (Z.of_int bits) ->
integer (Z.bshift_right_trunc ~bits i (Z.to_int j)) typ
integer (Z.shift_right_trunc i (Z.to_int j)) typ
(* e lshr 0 ==> e *)
| e, Integer {data} when Z.equal Z.zero data -> e
| _ -> App {op= App {op= Lshr; arg= x}; arg= y}
@ -1066,7 +1020,7 @@ let simp_ashr x y =
(* i ashr j *)
| Integer {data= i; typ= Integer {bits} as typ}, Integer {data= j}
when Z.sign j >= 0 && Z.lt j (Z.of_int bits) ->
integer (Z.bshift_right ~bits i (Z.to_int j)) typ
integer (Z.shift_right i (Z.to_int j)) typ
(* e ashr 0 ==> e *)
| e, Integer {data} when Z.equal Z.zero data -> e
| _ -> App {op= App {op= Ashr; arg= x}; arg= y}
@ -1251,51 +1205,55 @@ let convert ?(signed = false) ~dst ~src term =
app1 (Convert {signed; dst; src}) term
let rec of_exp (e : Exp.t) =
let of_exps exps =
Qset.fold exps ~init:empty_qset ~f:(fun e q ts ->
Qset.add ts (of_exp e) q )
in
match e with
| Add {args; typ} -> Add {args= of_exps args; typ}
| Mul {args; typ} -> Mul {args= of_exps args; typ}
| Reg {name} -> Var {id= 0; name}
| Nondet {msg} -> Nondet {msg}
| Label {parent; name} -> Label {parent; name}
| App {op; arg} -> App {op= of_exp op; arg= of_exp arg}
| Eq -> Eq
| Dq -> Dq
| Gt -> Gt
| Ge -> Ge
| Lt -> Lt
| Le -> Le
| Ugt -> Ugt
| Uge -> Uge
| Ult -> Ult
| Ule -> Ule
| Ord -> Ord
| Uno -> Uno
| Div -> Div
| Udiv -> Udiv
| Rem -> Rem
| Urem -> Urem
| And -> And
| Or -> Or
| Xor -> Xor
| Shl -> Shl
| Lshr -> Lshr
| Ashr -> Ashr
| Conditional -> Conditional
| Record -> Record
| Select -> Select
| Update -> Update
| Struct_rec {elts} ->
| Reg {name} -> var (Var {id= 0; name})
| Nondet {msg} -> nondet msg
| Label {parent; name} -> label ~parent ~name
| Integer {data; typ= Integer {bits} as typ} ->
integer (Z.signed_extract data 0 bits) typ
| Integer {data; typ} -> integer data typ
| Float {data} -> float data
| Ap1 (Convert {dst; signed}, src, arg) ->
convert ~signed ~dst ~src (of_exp arg)
| Ap1 (Select idx, _, arg) ->
select ~rcd:(of_exp arg) ~idx:(integer (Z.of_int idx) Typ.siz)
| Ap2 (Eq, _, x, y) -> eq (of_exp x) (of_exp y)
| Ap2 (Dq, _, x, y) -> dq (of_exp x) (of_exp y)
| Ap2 (Gt, _, x, y) -> gt (of_exp x) (of_exp y)
| Ap2 (Ge, _, x, y) -> ge (of_exp x) (of_exp y)
| Ap2 (Lt, _, x, y) -> lt (of_exp x) (of_exp y)
| Ap2 (Le, _, x, y) -> le (of_exp x) (of_exp y)
| Ap2 (Ugt, _, x, y) -> ugt (of_exp x) (of_exp y)
| Ap2 (Uge, _, x, y) -> uge (of_exp x) (of_exp y)
| Ap2 (Ult, _, x, y) -> ult (of_exp x) (of_exp y)
| Ap2 (Ule, _, x, y) -> ule (of_exp x) (of_exp y)
| Ap2 (Ord, _, x, y) -> ord (of_exp x) (of_exp y)
| Ap2 (Uno, _, x, y) -> uno (of_exp x) (of_exp y)
| Ap2 (Add, typ, x, y) -> add typ (of_exp x) (of_exp y)
| Ap2 (Sub, typ, x, y) -> sub typ (of_exp x) (of_exp y)
| Ap2 (Mul, typ, x, y) -> mul typ (of_exp x) (of_exp y)
| Ap2 (Div, _, x, y) -> div (of_exp x) (of_exp y)
| Ap2 (Rem, _, x, y) -> rem (of_exp x) (of_exp y)
| Ap2 (Udiv, _, x, y) -> udiv (of_exp x) (of_exp y)
| Ap2 (Urem, _, x, y) -> urem (of_exp x) (of_exp y)
| Ap2 (And, _, x, y) -> and_ (of_exp x) (of_exp y)
| Ap2 (Or, _, x, y) -> or_ (of_exp x) (of_exp y)
| Ap2 (Xor, _, x, y) -> xor (of_exp x) (of_exp y)
| Ap2 (Shl, _, x, y) -> shl (of_exp x) (of_exp y)
| Ap2 (Lshr, _, x, y) -> lshr (of_exp x) (of_exp y)
| Ap2 (Ashr, _, x, y) -> ashr (of_exp x) (of_exp y)
| Ap2 (Update idx, _, rcd, elt) ->
update ~rcd:(of_exp rcd) ~elt:(of_exp elt)
~idx:(integer (Z.of_int idx) Typ.siz)
| Ap3 (Conditional, _, cnd, thn, els) ->
conditional ~cnd:(of_exp cnd) ~thn:(of_exp thn) ~els:(of_exp els)
| ApN (Record, _, elts) ->
record (Vector.to_list (Vector.map ~f:of_exp elts))
| ApN (Struct_rec, _, elts) ->
Staged.unstage
(struct_rec (module Exp))
~id:e
(Vector.map elts ~f:(fun e -> lazy (of_exp e)))
| Convert {signed; dst; src} -> Convert {signed; dst; src}
| Integer {data; typ} -> Integer {data; typ}
| Float {data} -> Float {data}
let size_of t =
Option.bind (Typ.prim_bit_size_of t) ~f:(fun n ->

7
sledge/src/symbheap/term_test.ml
Unescape View File

@ -44,9 +44,10 @@ let%test_module _ =
let%test "boolean overflow" =
Term.is_true
(Term.eq
(Term.integer Z.minus_one Typ.bool)
(Term.integer Z.one Typ.bool))
(Term.of_exp
(Exp.eq Typ.bool
(Exp.integer Typ.bool Z.minus_one)
(Exp.integer Typ.bool Z.one)))
let%test "unsigned boolean overflow" =
Term.is_true

Write Preview
Loading…
Cancel
Save