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

[sledge] Eliminate recursive records

Browse Source 
Summary:
The support for recursive references to globals from within their
initializers is enough to handle all the cases of recursive structs
that have been encountered so far. Therefore this diff removes the
complication of recursive records entirely.

Reviewed By: jvillard

Differential Revision: D24772955

fbshipit-source-id: f59f06257
master
Josh Berdine 4 years ago committed by Facebook GitHub Bot
parent 0c17ac4281
commit aa307294a5
10 changed files with 30 additions and 64 deletions
Show Stats Download Patch File Download Diff File

3
sledge/cli/domain_itv.ml
Unescape View File

@ -127,8 +127,7 @@ let rec apron_texpr_of_llair_exp exp q =
| Label _
|Ap1 ((Splat | Select _), _, _)
|Ap3 (Conditional, _, _, _, _)
|ApN (Record, _, _)
|RecRecord _ ->
|ApN (Record, _, _) ->
None
let assign reg exp q =

60
sledge/cli/frontend.ml
Unescape View File

@ -416,7 +416,7 @@ let convert_to_siz =
let xlate_llvm_eh_typeid_for : x -> Typ.t -> Exp.t -> Exp.t =
fun x typ arg -> Exp.convert typ ~to_:(i32 x) arg
let rec xlate_intrinsic_exp stk :
let rec xlate_intrinsic_exp :
string -> (x -> Llvm.llvalue -> Inst.t list * Exp.t) option =
fun name ->
match name with
@ -424,36 +424,36 @@ let rec xlate_intrinsic_exp stk :
Some
(fun x llv ->
let rand = Llvm.operand llv 0 in
let pre, arg = xlate_value stk x rand in
let pre, arg = xlate_value x rand in
let src = xlate_type x (Llvm.type_of rand) in
(pre, xlate_llvm_eh_typeid_for x src arg) )
| _ -> None
and xlate_values stk x len val_i =
and xlate_values x len val_i =
let rec loop i (pre, args) =
if i < 0 then (pre, args)
else
let pre_i, arg_i = xlate_value stk x (val_i i) in
let pre_i, arg_i = xlate_value x (val_i i) in
loop (i - 1) (pre_i @ pre, arg_i :: args)
in
loop (len - 1) ([], [])
and xlate_value ?(inline = false) stk :
x -> Llvm.llvalue -> Inst.t list * Exp.t =
and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Inst.t list * Exp.t
=
fun x llv ->
let xlate_value_ llv =
match Llvm.classify_value llv with
| Instruction Call -> (
let func = Llvm.operand llv (Llvm.num_arg_operands llv) in
let fname = Llvm.value_name func in
match xlate_intrinsic_exp stk fname with
match xlate_intrinsic_exp fname with
| Some intrinsic when inline || should_inline llv -> intrinsic x llv
| _ -> ([], Exp.reg (xlate_name x llv)) )
| Instruction (Invoke | Alloca | Load | PHI | LandingPad | VAArg)
|Argument ->
([], Exp.reg (xlate_name x llv))
| Function | GlobalVariable -> ([], Exp.reg (xlate_global stk x llv).reg)
| GlobalAlias -> xlate_value stk x (Llvm.operand llv 0)
| 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 x llv)
| ConstantPointerNull -> ([], Exp.null)
@ -468,27 +468,23 @@ and xlate_value ?(inline = false) stk :
| ConstantVector | ConstantArray ->
let typ = xlate_type x (Llvm.type_of llv) in
let len = Llvm.num_operands llv in
let pre, args = xlate_values stk x len (Llvm.operand llv) in
let pre, args = xlate_values x len (Llvm.operand llv) in
(pre, Exp.record typ (IArray.of_list args))
| ConstantDataVector ->
let typ = xlate_type x (Llvm.type_of llv) in
let len = Llvm.vector_size (Llvm.type_of llv) in
let pre, args = xlate_values stk x len (Llvm.const_element llv) in
let pre, args = xlate_values x len (Llvm.const_element llv) in
(pre, Exp.record typ (IArray.of_list args))
| ConstantDataArray ->
let typ = xlate_type x (Llvm.type_of llv) in
let len = Llvm.array_length (Llvm.type_of llv) in
let pre, args = xlate_values stk x len (Llvm.const_element llv) in
let pre, args = xlate_values x len (Llvm.const_element llv) in
(pre, Exp.record typ (IArray.of_list args))
| ConstantStruct -> (
| ConstantStruct ->
let typ = xlate_type x (Llvm.type_of llv) in
match List.find_idx ~f:(( == ) llv) stk with
| Some (i, _) -> ([], Exp.rec_record i typ)
| None ->
let stk = llv :: stk in
let len = Llvm.num_operands llv in
let pre, args = xlate_values stk x len (Llvm.operand llv) in
(pre, Exp.record typ (IArray.of_list args)) )
let len = Llvm.num_operands llv in
let pre, args = xlate_values x len (Llvm.operand llv) in
(pre, Exp.record typ (IArray.of_list args))
| BlockAddress ->
let parent = find_name (Llvm.operand llv 0) in
let name = find_name (Llvm.operand llv 1) in
@ -510,9 +506,9 @@ and xlate_value ?(inline = false) stk :
| SRem | FRem | Shl | LShr | AShr | And | Or | Xor | ICmp | FCmp
| Select | GetElementPtr | ExtractElement | InsertElement
| ShuffleVector | ExtractValue | InsertValue ) as opcode ) ->
if inline || should_inline llv then xlate_opcode stk x llv opcode
if inline || should_inline llv then xlate_opcode x llv opcode
else ([], Exp.reg (xlate_name x llv))
| ConstantExpr -> xlate_opcode stk x llv (Llvm.constexpr_opcode llv)
| ConstantExpr -> xlate_opcode x llv (Llvm.constexpr_opcode llv)
| GlobalIFunc -> todo "ifuncs: %a" pp_llvalue llv ()
| Instruction (CatchPad | CleanupPad | CatchSwitch) ->
todo "windows exception handling: %a" pp_llvalue llv ()
@ -530,18 +526,18 @@ and xlate_value ?(inline = false) stk :
|>
[%Trace.retn fun {pf} -> pf "%a" pp_prefix_exp] )
and xlate_opcode stk :
x -> Llvm.llvalue -> Llvm.Opcode.t -> Inst.t list * Exp.t =
and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Inst.t list * Exp.t
=
fun x llv opcode ->
[%Trace.call fun {pf} -> pf "%a" pp_llvalue llv]
;
let xlate_rand i = xlate_value stk x (Llvm.operand llv i) in
let xlate_rand i = xlate_value x (Llvm.operand llv i) in
let typ = lazy (xlate_type x (Llvm.type_of llv)) in
let convert opcode =
let dst = Lazy.force typ in
let rand = Llvm.operand llv 0 in
let src = xlate_type x (Llvm.type_of rand) in
let pre, arg = xlate_value stk x rand in
let pre, arg = xlate_value x rand in
( pre
, match (opcode : Llvm.Opcode.t) with
| Trunc -> Exp.signed (Typ.bit_size_of dst) arg ~to_:dst
@ -729,7 +725,7 @@ and xlate_opcode stk :
| ShuffleVector -> (
(* translate shufflevector <N x t> %x, _, <N x i32> zeroinitializer to
%x *)
let exp = xlate_value stk x (Llvm.operand llv 0) in
let exp = xlate_value x (Llvm.operand llv 0) in
let exp_typ = xlate_type x (Llvm.type_of (Llvm.operand llv 0)) in
let llmask = Llvm.operand llv 2 in
let mask_typ = xlate_type x (Llvm.type_of llmask) in
@ -745,7 +741,7 @@ and xlate_opcode stk :
|>
[%Trace.retn fun {pf} -> pf "%a" pp_prefix_exp]
and xlate_global stk : x -> Llvm.llvalue -> Global.t =
and xlate_global : x -> Llvm.llvalue -> Global.t =
fun x llg ->
GlobTbl.find_or_add memo_global llg ~default:(fun () ->
[%Trace.call fun {pf} -> pf "%a" pp_llvalue llg]
@ -759,7 +755,7 @@ and xlate_global stk : x -> Llvm.llvalue -> Global.t =
match Llvm.classify_value llg with
| GlobalVariable ->
Option.map (Llvm.global_initializer llg) ~f:(fun llv ->
let pre, init = xlate_value stk x llv in
let pre, init = xlate_value x llv in
(* 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 *)
@ -773,12 +769,6 @@ and xlate_global stk : x -> Llvm.llvalue -> Global.t =
|>
[%Trace.retn fun {pf} -> pf "%a" Global.pp_defn] )
let xlate_intrinsic_exp = xlate_intrinsic_exp []
let xlate_value ?inline = xlate_value ?inline []
let xlate_values = xlate_values []
let xlate_opcode = xlate_opcode []
let xlate_global = xlate_global []
type pop_thunk = Loc.t -> Llair.inst list
let pop_stack_frame_of_function :

2
sledge/src/fol/context.ml
Unescape View File

@ -23,7 +23,7 @@ let rec classify e =
| Interpreted -> Interpreted
| Uninterpreted -> Uninterpreted )
| Sized _ | Extract _ | Concat _ -> Interpreted
| Var _ | Z _ | Q _ | Ancestor _ -> Atomic
| Var _ | Z _ | Q _ -> Atomic
| Splat _ | Select _ | Update _ | Record _ | Apply _ -> Uninterpreted
let interpreted e = equal_kind (classify e) Interpreted

1
sledge/src/fol/exp.ml
Unescape View File

@ -237,7 +237,6 @@ module Term = struct
ap2t (fun rcd elt -> Trm.update ~rcd ~idx ~elt) rcd elt
let record elts = apNt Trm.record elts
let ancestor i = `Trm (Trm.ancestor i)
(* uninterpreted *)

3
sledge/src/fol/exp.mli
Unescape View File

@ -56,9 +56,6 @@ module rec Term : sig
val record : t array -> t
(** Record constant *)
val ancestor : int -> t
(** Reference to ancestor recursive record *)
(* uninterpreted *)
val apply : Funsym.t -> t array -> t

12
sledge/src/fol/trm.ml
Unescape View File

@ -86,7 +86,6 @@ and Trm : sig
| Select of {idx: int; rcd: t}
| Update of {idx: int; rcd: t; elt: t}
| Record of t array
| Ancestor of int
(* uninterpreted *)
| Apply of Funsym.t * t array
[@@deriving compare, equal, sexp]
@ -104,7 +103,6 @@ and Trm : sig
val _Select : int -> t -> t
val _Update : int -> t -> t -> t
val _Record : t array -> t
val _Ancestor : int -> t
val _Apply : Funsym.t -> t array -> t
val add : t -> t -> t
val sub : t -> t -> t
@ -126,7 +124,6 @@ end = struct
| Select of {idx: int; rcd: t}
| Update of {idx: int; rcd: t; elt: t}
| Record of t array
| Ancestor of int
| Apply of Funsym.t * t array
[@@deriving compare, equal, sexp]
@ -163,7 +160,6 @@ end = struct
| Update {idx; rcd; elt} ->
pf "[%a@ @[| %i → %a@]]" pp rcd idx pp elt
| Record xs -> pf "{%a}" (ppx_record strength) xs
| Ancestor i -> pf "(ancestor %i)" i
| Apply (f, [||]) -> pf "%a" Funsym.pp f
| Apply
( ( (Rem | BitAnd | BitOr | BitXor | BitShl | BitLshr | BitAshr)
@ -361,7 +357,6 @@ end = struct
let _Select idx rcd = Select {idx; rcd} |> check invariant
let _Update idx rcd elt = Update {idx; rcd; elt} |> check invariant
let _Record es = Record es |> check invariant
let _Ancestor i = Ancestor i |> check invariant
let _Apply f es =
( match Funsym.eval ~equal ~get_z ~ret_z:_Z ~get_q ~ret_q:_Q f es with
@ -374,7 +369,7 @@ end = struct
let rec iter_vars e ~f =
match e with
| Var _ as v -> f (Var.of_ v)
| Z _ | Q _ | Ancestor _ -> ()
| Z _ | Q _ -> ()
| Splat x | Select {rcd= x} -> iter_vars ~f x
| Sized {seq= x; siz= y} | Update {rcd= x; elt= y} ->
iter_vars ~f x ;
@ -438,7 +433,6 @@ let concat elts = _Concat elts
let select ~rcd ~idx = _Select idx rcd
let update ~rcd ~idx ~elt = _Update idx rcd elt
let record elts = _Record elts
let ancestor i = _Ancestor i
(* uninterpreted *)
@ -458,7 +452,6 @@ let rec map_vars e ~f =
| Select {idx; rcd} -> map1 (map_vars ~f) e (_Select idx) rcd
| Update {idx; rcd; elt} -> map2 (map_vars ~f) e (_Update idx) rcd elt
| Record xs -> mapN (map_vars ~f) e _Record xs
| Ancestor _ -> e
| Apply (g, xs) -> mapN (map_vars ~f) e (_Apply g) xs
let map e ~f =
@ -472,14 +465,13 @@ let map e ~f =
| Select {idx; rcd} -> map1 f e (_Select idx) rcd
| Update {idx; rcd; elt} -> map2 f e (_Update idx) rcd elt
| Record xs -> mapN f e _Record xs
| Ancestor _ -> e
| Apply (g, xs) -> mapN f e (_Apply g) xs
(** Traverse *)
let iter_subtrms e ~f =
match e with
| Var _ | Z _ | Q _ | Ancestor _ -> ()
| Var _ | Z _ | Q _ -> ()
| Arith a -> Iter.iter ~f (Arith.trms a)
| Splat x | Select {rcd= x} -> f x
| Sized {seq= x; siz= y} | Update {rcd= x; elt= y} ->

2
sledge/src/fol/trm.mli
Unescape View File

@ -25,7 +25,6 @@ type t = private
| Select of {idx: int; rcd: t}
| Update of {idx: int; rcd: t; elt: t}
| Record of t array
| Ancestor of int
(* uninterpreted *)
| Apply of Funsym.t * t array
[@@deriving compare, equal, sexp]
@ -81,7 +80,6 @@ val concat : t array -> t
val select : rcd:t -> idx:int -> t
val update : rcd:t -> idx:int -> elt:t -> t
val record : t array -> t
val ancestor : int -> t
(* uninterpreted *)
val apply : Funsym.t -> t array -> t

8
sledge/src/llair/exp.ml
Unescape View File

@ -70,7 +70,6 @@ module T = struct
| Ap2 of op2 * Typ.t * t * t
| Ap3 of op3 * Typ.t * t * t * t
| ApN of opN * Typ.t * t iarray
| RecRecord of int * Typ.t
[@@deriving compare, equal, hash, sexp]
end
@ -143,7 +142,6 @@ let rec pp fs exp =
| Ap3 (Conditional, _, cnd, thn, els) ->
pf "(%a@ ? %a@ : %a)" pp cnd pp thn pp els
| ApN (Record, _, elts) -> pf "{%a}" pp_record elts
| RecRecord (i, _) -> pf "rec_record %i" i
[@@warning "-9"]
and pp_record fs elts =
@ -240,7 +238,6 @@ let rec invariant exp =
IArray.for_all2_exn elts args ~f:(fun (_, typ) arg ->
Typ.castable typ (typ_of arg) ) )
| _ -> assert false )
| RecRecord _ -> ()
[@@warning "-9"]
(** Type query *)
@ -268,8 +265,7 @@ and typ_of exp =
, _
, _ )
|Ap3 (Conditional, typ, _, _, _)
|ApN (Record, typ, _)
|RecRecord (_, typ) ->
|ApN (Record, typ, _) ->
typ
[@@warning "-9"]
@ -406,8 +402,6 @@ let select typ rcd idx = Ap1 (Select idx, typ, rcd) |> check invariant
let update typ ~rcd idx ~elt =
Ap2 (Update idx, typ, rcd, elt) |> check invariant
let rec_record i typ = RecRecord (i, typ)
(** Traverse *)
let rec fold_exps e z ~f =

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

@ -81,7 +81,6 @@ type t = private
| Ap2 of op2 * Typ.t * t * t
| Ap3 of op3 * Typ.t * t * t * t
| ApN of opN * Typ.t * t iarray
| RecRecord of int * Typ.t (** Reference to ancestor recursive record *)
[@@deriving compare, equal, hash, sexp]
val pp : t pp
@ -179,7 +178,6 @@ val splat : Typ.t -> t -> t
val record : Typ.t -> t iarray -> t
val select : Typ.t -> t -> int -> t
val update : Typ.t -> rcd:t -> int -> elt:t -> t
val rec_record : int -> Typ.t -> t
(** Traverse *)

1
sledge/src/llair_to_Fol.ml
Unescape View File

@ -125,7 +125,6 @@ and term : Llair.Exp.t -> T.t =
T.update ~rcd:(term rcd) ~idx ~elt:(term elt)
| ApN (Record, _, elts) ->
T.record (Array.map ~f:term (IArray.to_array elts))
| RecRecord (i, _) -> T.ancestor i
| Ap1 (Splat, _, byt) -> T.splat (term byt)
and formula e = F.dq0 (term e)

Write Preview
Loading…
Cancel
Save