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

[sledge] Keep size in both bits and bytes for each type

Browse Source 
Summary:
- The `Llvm_target.DataLayout.size_in_bits` needs to be used for checking casts
  e.g. it is ok to `bitcast <16 x i1> to i16`: they both have 16 bits, but they have sizes 16 vs 2 bytes
- The `Llvm_target.DataLayout.abi_size` needs to be used for the size of memory blocks containing values
  e.g. for the size of memory segments containing the initial values of globals
- The example above shows that we can't compute the byte size from the bit size without knowing the target specific datalayout
- So we need both in each sized type
- Also add checks that Convert exps and terms are not no-ops
- Simplifications of size manipulating code

Reviewed By: ngorogiannis

Differential Revision: D17801928

fbshipit-source-id: 8c8ce6128
master
Josh Berdine 5 years ago committed by Facebook Github Bot
parent 9dbe55c419
commit ca95fc098f
8 changed files with 178 additions and 146 deletions
Show Stats Download Patch File Download Diff File

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

@ -212,6 +212,7 @@ let rec invariant exp =
match typ with Float _ -> assert true | _ -> assert false ) match typ with Float _ -> assert true | _ -> assert false )
| Label _ -> assert true | Label _ -> assert true
| Ap1 (Convert {dst}, src, arg) -> | Ap1 (Convert {dst}, src, arg) ->
assert (not (Typ.equal dst src)) ;
assert (Typ.convertible dst src) ; assert (Typ.convertible dst src) ;
assert (Typ.castable src (typ_of arg)) assert (Typ.castable src (typ_of arg))
| Ap1 (Select idx, typ, rcd) -> ( | Ap1 (Select idx, typ, rcd) -> (
@ -223,9 +224,9 @@ let rec invariant exp =
| Ap2 (Splat, typ, byt, siz) -> ( | Ap2 (Splat, typ, byt, siz) -> (
assert (Typ.convertible Typ.byt (typ_of byt)) ; assert (Typ.convertible Typ.byt (typ_of byt)) ;
assert (Typ.convertible Typ.siz (typ_of siz)) ; assert (Typ.convertible Typ.siz (typ_of siz)) ;
match (Typ.size_of typ, siz.desc) with assert (Typ.is_sized typ) ;
| Some n, Integer {data} -> assert (Z.equal (Z.of_int n) data) match siz.desc with
| None, Integer {data} -> assert (not (Z.equal Z.zero data)) | Integer {data} -> assert (Z.equal (Z.of_int (Typ.size_of typ)) data)
| _ -> () ) | _ -> () )
| Ap2 (Update idx, typ, rcd, elt) -> ( | Ap2 (Update idx, typ, rcd, elt) -> (
assert (Typ.castable typ (typ_of rcd)) ; assert (Typ.castable typ (typ_of rcd)) ;
@ -295,6 +296,8 @@ and typ_of exp =
typ typ
[@@warning "-9"] [@@warning "-9"]
let typ = typ_of
type exp = t type exp = t
let pp_exp = pp let pp_exp = pp
@ -422,10 +425,8 @@ let binary op mk ?typ x y =
let ubinary op mk ?typ x y = let ubinary op mk ?typ x y =
let typ = match typ with Some typ -> typ | None -> typ_of x in let typ = match typ with Some typ -> typ | None -> typ_of x in
let umk x y = let umk x y =
let bits = Option.value_exn (Typ.prim_bit_size_of typ) in let extract = Term.extract ~unsigned:true ~bits:(Typ.bit_size_of typ) in
mk mk (extract x) (extract y)
(Term.extract ~unsigned:true ~bits x)
(Term.extract ~unsigned:true ~bits y)
in in
binary op umk ~typ x y binary op umk ~typ x y
@ -520,6 +521,8 @@ let struct_rec key =
forcing the recursive thunks also updates this value. *) forcing the recursive thunks also updates this value. *)
{desc= ApN (Struct_rec, typ, elts); term= rec_app ~id Vector.empty} {desc= ApN (Struct_rec, typ, elts); term= rec_app ~id Vector.empty}
let size_of exp = integer Typ.siz (Z.of_int (Typ.size_of (typ exp)))
(** Traverse *) (** Traverse *)
let fold_exps e ~init ~f = let fold_exps e ~init ~f =

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

@ -196,6 +196,8 @@ val struct_rec :
one point on each cycle. Failure to obey these requirements will lead to one point on each cycle. Failure to obey these requirements will lead to
stack overflow. *) stack overflow. *)
val size_of : t -> t
(** Traverse *) (** Traverse *)
val fold_regs : t -> init:'a -> f:('a -> Reg.t -> 'a) -> 'a val fold_regs : t -> init:'a -> f:('a -> Reg.t -> 'a) -> 'a

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

@ -190,69 +190,79 @@ type x =
let ptr_siz : x -> int = let ptr_siz : x -> int =
fun x -> Llvm_target.DataLayout.pointer_size x.lldatalayout fun x -> Llvm_target.DataLayout.pointer_size x.lldatalayout
let size_of : x -> Llvm.lltype -> int = let size_of, bit_size_of =
fun x llt -> let size_to_int size_of x llt =
if Llvm.type_is_sized llt then if Llvm.type_is_sized llt then
match match Int64.to_int (size_of llt x.lldatalayout) with
Int64.to_int (Llvm_target.DataLayout.abi_size llt x.lldatalayout) | Some n -> n
with | None -> fail "type size too large: %a" pp_lltype llt ()
| Some n -> n else fail "types with undetermined size: %a" pp_lltype llt ()
| None -> fail "size_of: %a" pp_lltype llt () in
else todo "types with undetermined size: %a" pp_lltype llt () ( size_to_int Llvm_target.DataLayout.abi_size
, size_to_int Llvm_target.DataLayout.size_in_bits )
let memo_type : (Llvm.lltype, Typ.t) Hashtbl.t = Hashtbl.Poly.create () let memo_type : (Llvm.lltype, Typ.t) Hashtbl.t = Hashtbl.Poly.create ()
let rec xlate_type : x -> Llvm.lltype -> Typ.t = let rec xlate_type : x -> Llvm.lltype -> Typ.t =
fun x llt -> fun x llt ->
let xlate_type_ llt = let xlate_type_ llt =
match Llvm.classify_type llt with if Llvm.type_is_sized llt then
| Half -> Typ.float ~bits:16 ~siz:(size_of x llt) ~enc:`IEEE let byts = size_of x llt in
| Float -> Typ.float ~bits:32 ~siz:(size_of x llt) ~enc:`IEEE let bits = bit_size_of x llt in
| Double -> Typ.float ~bits:64 ~siz:(size_of x llt) ~enc:`IEEE match Llvm.classify_type llt with
| X86fp80 -> Typ.float ~bits:80 ~siz:(size_of x llt) ~enc:`Extended | Half | Float | Double | Fp128 -> Typ.float ~bits ~byts ~enc:`IEEE
| Fp128 -> Typ.float ~bits:128 ~siz:(size_of x llt) ~enc:`IEEE | X86fp80 -> Typ.float ~bits ~byts ~enc:`Extended
| Ppc_fp128 -> Typ.float ~bits:128 ~siz:(size_of x llt) ~enc:`Pair | Ppc_fp128 -> Typ.float ~bits ~byts ~enc:`Pair
| Integer -> | Integer -> Typ.integer ~bits ~byts
Typ.integer ~bits:(Llvm.integer_bitwidth llt) ~siz:(size_of x llt) | X86_mmx -> Typ.integer ~bits ~byts
| X86_mmx -> Typ.integer ~bits:64 ~siz:(size_of x llt) | Pointer ->
| Function -> if byts <> ptr_siz x then
let return = xlate_type_opt x (Llvm.return_type llt) in todo "non-integral pointer types: %a" pp_lltype llt () ;
let llargs = Llvm.param_types llt in let elt = xlate_type x (Llvm.element_type llt) in
let len = Array.length llargs in Typ.pointer ~elt
let args = Vector.init len ~f:(fun i -> xlate_type x llargs.(i)) in | Vector ->
Typ.function_ ~return ~args let elt = xlate_type x (Llvm.element_type llt) in
| Pointer -> let len = Llvm.vector_size llt in
if size_of x llt <> ptr_siz x then Typ.array ~elt ~len ~bits ~byts
todo "non-integral pointer types: %a" pp_lltype llt () ; | Array ->
let elt = xlate_type x (Llvm.element_type llt) in let elt = xlate_type x (Llvm.element_type llt) in
Typ.pointer ~elt let len = Llvm.array_length llt in
| Vector -> Typ.array ~elt ~len ~bits ~byts
let elt = xlate_type x (Llvm.element_type llt) in | Struct ->
let len = Llvm.vector_size llt in let llelts = Llvm.struct_element_types llt in
Typ.array ~elt ~len ~siz:(size_of x llt) let len = Array.length llelts in
| Array -> let packed = Llvm.is_packed llt in
let elt = xlate_type x (Llvm.element_type llt) in if Llvm.is_literal llt then
let len = Llvm.array_length llt in let elts =
Typ.array ~elt ~len ~siz:(size_of x llt) Vector.map ~f:(xlate_type x) (Vector.of_array llelts)
| Struct -> in
let llelts = Llvm.struct_element_types llt in Typ.tuple elts ~bits ~byts ~packed
let len = Array.length llelts in
let packed = Llvm.is_packed llt in
if Llvm.is_literal llt then
let elts =
Vector.map ~f:(xlate_type x) (Vector.of_array llelts)
in
Typ.tuple elts ~siz:(size_of x llt) ~packed
else
let name = struct_name llt in
if Llvm.is_opaque llt then Typ.opaque ~name ~siz:(size_of x llt)
else else
let name = struct_name llt in
let elts = let elts =
Vector.init len ~f:(fun i -> lazy (xlate_type x llelts.(i))) Vector.init len ~f:(fun i -> lazy (xlate_type x llelts.(i)))
in in
Typ.struct_ ~name elts ~siz:(size_of x llt) ~packed Typ.struct_ ~name elts ~bits ~byts ~packed
| Token -> Typ.opaque ~name:"token" ~siz:(size_of x llt) | Function -> fail "expected to be unsized: %a" pp_lltype llt ()
| Void | Label | Metadata -> assert false | Void | Label | Metadata | Token -> assert false
else
match Llvm.classify_type llt with
| Function ->
let return = xlate_type_opt x (Llvm.return_type llt) in
let llargs = Llvm.param_types llt in
let len = Array.length llargs in
let args =
Vector.init len ~f:(fun i -> xlate_type x llargs.(i))
in
Typ.function_ ~return ~args
| Struct when Llvm.is_opaque llt -> Typ.opaque ~name:(struct_name llt)
| Token -> Typ.opaque ~name:"token"
| Vector | Array | Struct ->
todo "unsized non-opaque aggregate types: %a" pp_lltype llt ()
| Half | Float | Double | X86fp80 | Fp128 | Ppc_fp128 | Integer
|X86_mmx | Pointer ->
fail "expected to be sized: %a" pp_lltype llt ()
| Void | Label | Metadata -> assert false
in in
Hashtbl.find_or_add memo_type llt ~default:(fun () -> Hashtbl.find_or_add memo_type llt ~default:(fun () ->
[%Trace.call fun {pf} -> pf "%a" pp_lltype llt] [%Trace.call fun {pf} -> pf "%a" pp_lltype llt]
@ -374,17 +384,16 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Exp.t =
| ConstantFP -> xlate_float x llv | ConstantFP -> xlate_float x llv
| ConstantPointerNull -> Exp.null | ConstantPointerNull -> Exp.null
| ConstantAggregateZero -> ( | ConstantAggregateZero -> (
let llt = Llvm.type_of llv in let typ = xlate_type x (Llvm.type_of llv) in
let typ = xlate_type x llt in
match typ with match typ with
| Integer _ -> Exp.integer typ Z.zero | Integer _ -> Exp.integer typ Z.zero
| Pointer _ -> Exp.null | Pointer _ -> Exp.null
| Array _ | Tuple _ | Struct _ -> | Array _ | Tuple _ | Struct _ ->
let llsiz = size_of x llt in let siz = Typ.size_of typ in
if llsiz = 0 then todo "ConstantAggregateZero of size 0" () ; if siz = 0 then todo "ConstantAggregateZero of size 0" () ;
Exp.splat typ Exp.splat typ
~byt:(Exp.integer Typ.byt Z.zero) ~byt:(Exp.integer Typ.byt Z.zero)
~siz:(Exp.integer Typ.siz (Z.of_int llsiz)) ~siz:(Exp.integer Typ.siz (Z.of_int siz))
| _ -> fail "ConstantAggregateZero of type %a" Typ.pp typ () ) | _ -> fail "ConstantAggregateZero of type %a" Typ.pp typ () )
| ConstantVector | ConstantArray -> | ConstantVector | ConstantArray ->
let typ = xlate_type x (Llvm.type_of llv) in let typ = xlate_type x (Llvm.type_of llv) in
@ -720,9 +729,9 @@ let landingpad_typs : x -> Llvm.llvalue -> Typ.t * Typ.t * Llvm.lltype =
let exception_typs = let exception_typs =
let pi8 = Typ.pointer ~elt:Typ.byt in let pi8 = Typ.pointer ~elt:Typ.byt in
let i32 = Typ.integer ~bits:32 ~siz:4 in let i32 = Typ.integer ~bits:32 ~byts:4 in
let exc = let exc =
Typ.tuple ~packed:false (Vector.of_array [|pi8; i32|]) ~siz:12 Typ.tuple ~packed:false (Vector.of_array [|pi8; i32|]) ~bits:96 ~byts:12
in in
(pi8, i32, exc) (pi8, i32, exc)
@ -843,14 +852,12 @@ let xlate_instr :
match opcode with match opcode with
| Load -> | Load ->
let reg = xlate_name x instr in let reg = xlate_name x instr in
let llt = Llvm.type_of instr in let len = Exp.size_of (Exp.reg reg) 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 let ptr = xlate_value x (Llvm.operand instr 0) in
emit_inst (Llair.Inst.load ~reg ~ptr ~len ~loc) emit_inst (Llair.Inst.load ~reg ~ptr ~len ~loc)
| Store -> | Store ->
let exp = xlate_value x (Llvm.operand instr 0) in let exp = xlate_value x (Llvm.operand instr 0) in
let llt = Llvm.type_of (Llvm.operand instr 0) in let len = Exp.size_of exp 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 let ptr = xlate_value x (Llvm.operand instr 1) in
emit_inst (Llair.Inst.store ~ptr ~exp ~len ~loc) emit_inst (Llair.Inst.store ~ptr ~exp ~len ~loc)
| Alloca -> | Alloca ->
@ -862,8 +869,7 @@ let xlate_instr :
(xlate_value x rand) (xlate_value x rand)
in in
assert (Poly.(Llvm.classify_type (Llvm.type_of instr) = Pointer)) ; assert (Poly.(Llvm.classify_type (Llvm.type_of instr) = Pointer)) ;
let llt = Llvm.element_type (Llvm.type_of instr) in let len = Exp.size_of (Exp.reg reg) in
let len = Exp.integer Typ.siz (Z.of_int (size_of x llt)) in
emit_inst (Llair.Inst.alloc ~reg ~num ~len ~loc) emit_inst (Llair.Inst.alloc ~reg ~num ~len ~loc)
| Call -> ( | Call -> (
let maybe_llfunc = Llvm.operand instr (Llvm.num_operands instr - 1) in let maybe_llfunc = Llvm.operand instr (Llvm.num_operands instr - 1) in
@ -914,8 +920,7 @@ let xlate_instr :
(* operator new(unsigned long, std::align_val_t) *) ] -> (* operator new(unsigned long, std::align_val_t) *) ] ->
let reg = xlate_name x instr in let reg = xlate_name x instr in
let num = xlate_value x (Llvm.operand instr 0) in let num = xlate_value x (Llvm.operand instr 0) in
let llt = Llvm.type_of instr in let len = Exp.size_of (Exp.reg reg) in
let len = Exp.integer Typ.siz (Z.of_int (size_of x llt)) in
emit_inst (Llair.Inst.alloc ~reg ~num ~len ~loc) emit_inst (Llair.Inst.alloc ~reg ~num ~len ~loc)
| ["_ZdlPv" (* operator delete(void* ptr) *)] | ["_ZdlPv" (* operator delete(void* ptr) *)]
|[ "_ZdlPvSt11align_val_t" |[ "_ZdlPvSt11align_val_t"
@ -1036,8 +1041,7 @@ let xlate_instr :
when num_args > 0 -> when num_args > 0 ->
let reg = xlate_name x instr in let reg = xlate_name x instr in
let num = xlate_value x (Llvm.operand instr 0) in let num = xlate_value x (Llvm.operand instr 0) in
let llt = Llvm.type_of instr in let len = Exp.size_of (Exp.reg reg) 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 let dst, blocks = xlate_jump x instr return_blk loc [] in
emit_term emit_term
~prefix:[Llair.Inst.alloc ~reg ~num ~len ~loc] ~prefix:[Llair.Inst.alloc ~reg ~num ~len ~loc]

21
sledge/src/llair/term.ml
Unescape View File

@ -352,7 +352,9 @@ let invariant e =
| ApN (Concat, mems) -> assert (Vector.length mems <> 1) | ApN (Concat, mems) -> assert (Vector.length mems <> 1)
| ApN (Record, elts) | RecN (Record, elts) -> | ApN (Record, elts) | RecN (Record, elts) ->
assert (not (Vector.is_empty elts)) assert (not (Vector.is_empty elts))
| Ap1 (Convert {dst; src}, _) -> assert (Typ.convertible src dst) | Ap1 (Convert {dst; src}, _) ->
assert (not (Typ.equivalent dst src)) ;
assert (Typ.convertible dst src)
| _ -> () | _ -> ()
[@@warning "-9"] [@@warning "-9"]
@ -497,12 +499,13 @@ let simp_extract ~unsigned bits arg =
| _ -> Ap1 (Extract {unsigned; bits}, arg) | _ -> Ap1 (Extract {unsigned; bits}, arg)
let simp_convert ~unsigned dst src arg = let simp_convert ~unsigned dst src arg =
if (not unsigned) && Typ.equivalent dst src then arg match (dst, src, arg) with
else | Typ.Integer {bits= m; _}, Typ.Integer {bits= n; _}, Integer {data} ->
match (dst, src, arg) with if (not unsigned) && m >= n then arg
| Integer {bits= m; _}, Integer {bits= n; _}, Integer {data} -> else integer (Z.extract ~unsigned (min m n) data)
integer (Z.extract ~unsigned (min m n) data) | _ ->
| _ -> Ap1 (Convert {unsigned; dst; src}, arg) if Typ.equivalent dst src then arg
else Ap1 (Convert {unsigned; dst; src}, arg)
(* arithmetic *) (* arithmetic *)
@ -949,9 +952,7 @@ let concat xs = normN Concat (Vector.of_array xs)
let record elts = normN Record elts let record elts = normN Record elts
let select ~rcd ~idx = norm1 (Select idx) rcd let select ~rcd ~idx = norm1 (Select idx) rcd
let update ~rcd ~idx ~elt = norm2 (Update idx) rcd elt let update ~rcd ~idx ~elt = norm2 (Update idx) rcd elt
let size_of t = integer (Z.of_int (Typ.size_of t))
let size_of t =
Option.map ~f:(fun n -> integer (Z.of_int n)) (Typ.size_of t)
(** Transform *) (** Transform *)

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

@ -197,7 +197,7 @@ val rec_app :
(module Hashtbl.Key with type t = 'id) (module Hashtbl.Key with type t = 'id)
-> (id:'id -> recN -> t lazy_t vector -> t) Staged.t -> (id:'id -> recN -> t lazy_t vector -> t) Staged.t
val size_of : Typ.t -> t option val size_of : Typ.t -> t
(** Transform *) (** Transform *)

91
sledge/src/llair/typ.ml
Unescape View File

@ -9,18 +9,19 @@
type t = type t =
| Function of {return: t option; args: t vector} | Function of {return: t option; args: t vector}
| Integer of {bits: int; siz: int} | Integer of {bits: int; byts: int}
| Float of {bits: int; siz: int; enc: [`IEEE | `Extended | `Pair]} | Float of {bits: int; byts: int; enc: [`IEEE | `Extended | `Pair]}
| Pointer of {elt: t} | Pointer of {elt: t}
| Array of {elt: t; len: int; siz: int} | Array of {elt: t; len: int; bits: int; byts: int}
| Tuple of {elts: t vector; siz: int; packed: bool} | Tuple of {elts: t vector; bits: int; byts: int; packed: bool}
| Struct of | Struct of
{ name: string { name: string
; elts: t vector (* possibly cyclic, name unique *) ; elts: t vector (* possibly cyclic, name unique *)
[@compare.ignore] [@equal.ignore] [@sexp_drop_if fun _ -> true] [@compare.ignore] [@equal.ignore] [@sexp_drop_if fun _ -> true]
; siz: int ; bits: int
; byts: int
; packed: bool } ; packed: bool }
| Opaque of {name: string; siz: int} | Opaque of {name: string}
[@@deriving compare, equal, hash, sexp] [@@deriving compare, equal, hash, sexp]
let rec pp fs typ = let rec pp fs typ =
@ -78,34 +79,41 @@ let invariant t =
(** Constructors *) (** Constructors *)
let function_ ~return ~args = Function {return; args} |> check invariant let function_ ~return ~args = Function {return; args} |> check invariant
let integer ~bits ~siz = Integer {bits; siz} |> check invariant let integer ~bits ~byts = Integer {bits; byts} |> check invariant
let float ~bits ~siz ~enc = Float {bits; siz; enc} |> check invariant let float ~bits ~byts ~enc = Float {bits; byts; enc} |> check invariant
let pointer ~elt = Pointer {elt} |> check invariant let pointer ~elt = Pointer {elt} |> check invariant
let array ~elt ~len ~siz = Array {elt; len; siz} |> check invariant
let tuple elts ~siz ~packed = Tuple {elts; siz; packed} |> check invariant let array ~elt ~len ~bits ~byts =
let opaque ~name ~siz = Opaque {name; siz} |> check invariant Array {elt; len; bits; byts} |> check invariant
let tuple elts ~bits ~byts ~packed =
Tuple {elts; bits; byts; packed} |> check invariant
let opaque ~name = Opaque {name} |> check invariant
let struct_ = let struct_ =
let defns : (string, t) Hashtbl.t = Hashtbl.create (module String) in let defns : (string, t) Hashtbl.t = Hashtbl.create (module String) in
let dummy_typ = Opaque {name= "dummy"; siz= 0} in let dummy_typ = Opaque {name= "dummy"} in
fun ~name ~siz ~packed elt_thks -> fun ~name ~bits ~byts ~packed elt_thks ->
match Hashtbl.find defns name with match Hashtbl.find defns name with
| Some typ -> typ | Some typ -> typ
| None -> | None ->
(* Add placeholder defn to prevent computing [elts] in calls to (* Add placeholder defn to prevent computing [elts] in calls to
[struct] from [elts] for recursive occurrences of [name]. *) [struct] from [elts] for recursive occurrences of [name]. *)
let elts = Array.create ~len:(Vector.length elt_thks) dummy_typ in let elts = Array.create ~len:(Vector.length elt_thks) dummy_typ in
let typ = Struct {name; elts= Vector.of_array elts; siz; packed} in let typ =
Struct {name; elts= Vector.of_array elts; bits; byts; packed}
in
Hashtbl.set defns ~key:name ~data:typ ; Hashtbl.set defns ~key:name ~data:typ ;
Vector.iteri elt_thks ~f:(fun i (lazy elt) -> elts.(i) <- elt) ; Vector.iteri elt_thks ~f:(fun i (lazy elt) -> elts.(i) <- elt) ;
typ |> check invariant typ |> check invariant
(** Constants *) (** Constants *)
let bool = integer ~bits:1 ~siz:1 let bool = integer ~bits:1 ~byts:1
let byt = integer ~bits:8 ~siz:1 let byt = integer ~bits:8 ~byts:1
let int = integer ~bits:32 ~siz:4 let int = integer ~bits:32 ~byts:4
let siz = integer ~bits:64 ~siz:8 let siz = integer ~bits:64 ~byts:8
(** [ptr] is semantically equivalent to [siz], but has a distinct (** [ptr] is semantically equivalent to [siz], but has a distinct
representation because the element type is important for [Global]s *) representation because the element type is important for [Global]s *)
@ -113,38 +121,39 @@ let ptr = pointer ~elt:byt
(** Queries *) (** Queries *)
let bit_size_of = function
| (Function _ | Opaque _) as t ->
fail "bit_size_of requires is_sized: %a" pp t ()
| Integer {bits; _}
|Float {bits; _}
|Array {bits; _}
|Tuple {bits; _}
|Struct {bits; _} ->
bits
| Pointer _ -> 64
let size_of = function let size_of = function
| Function _ -> None | (Function _ | Opaque _) as t ->
| Integer {siz} fail "size_of requires is_sized: %a" pp t ()
|Float {siz} | Integer {byts; _}
|Array {siz} |Float {byts; _}
|Tuple {siz} |Array {byts; _}
|Struct {siz} |Tuple {byts; _}
|Opaque {siz} -> |Struct {byts; _} ->
Some siz byts
| Pointer _ -> Some 8 | Pointer _ -> 8
let rec prim_bit_size_of = function
| Integer {bits} | Float {bits} -> Some bits
| Pointer _ -> prim_bit_size_of siz
| Array {elt; len} ->
Option.map (prim_bit_size_of elt) ~f:(fun n -> n * len)
| Function _ | Tuple _ | Struct _ | Opaque _ -> None
let rec equivalent t0 t1 = let rec equivalent t0 t1 =
match (t0, t1) with match (t0, t1) with
| (Pointer _ | Integer _), (Pointer _ | Integer _) -> ( | (Pointer _ | Integer _), (Pointer _ | Integer _) ->
match (prim_bit_size_of t0, prim_bit_size_of t1) with bit_size_of t0 = bit_size_of t1
| Some n0, Some n1 -> n0 = n1
| _ -> false )
| Array {elt= t; len= m}, Array {elt= u; len= n} -> | Array {elt= t; len= m}, Array {elt= u; len= n} ->
m = n && equivalent t u m = n && equivalent t u
| _ -> equal t0 t1 | _ -> equal t0 t1
let castable t0 t1 = let castable t0 t1 =
match (size_of t0, size_of t1) with (is_sized t0 && is_sized t1 && bit_size_of t0 = bit_size_of t1)
| Some m, Some n -> m = n || equal t0 t1
| _ -> equal t0 t1
let rec convertible t0 t1 = let rec convertible t0 t1 =
castable t0 t1 castable t0 t1

43
sledge/src/llair/typ.mli
Unescape View File

@ -10,19 +10,24 @@
type t = private type t = private
| Function of {return: t option; args: t vector} | Function of {return: t option; args: t vector}
(** (Global) function names have type Pointer to Function. *) (** (Global) function names have type Pointer to Function. *)
| Integer of {bits: int; siz: int} (** Integer of given bitwidth. *) | Integer of {bits: int; byts: int} (** Integer of given bitwidth. *)
| Float of {bits: int; siz: int; enc: [`IEEE | `Extended | `Pair]} | Float of {bits: int; byts: int; enc: [`IEEE | `Extended | `Pair]}
(** Floating-point numbers of given bitwidth and encoding. *) (** Floating-point numbers of given bitwidth and encoding. *)
| Pointer of {elt: t} (** Pointer to element type. *) | Pointer of {elt: t} (** Pointer to element type. *)
| Array of {elt: t; len: int; siz: int} | Array of {elt: t; len: int; bits: int; byts: int}
(** Statically-sized array of [len] elements of type [elt]. *) (** Statically-sized array of [len] elements of type [elt]. *)
| Tuple of {elts: t vector; siz: int; packed: bool} | Tuple of {elts: t vector; bits: int; byts: int; packed: bool}
(** Anonymous aggregate of heterogeneous types. *) (** Anonymous aggregate of heterogeneous types. *)
| Struct of {name: string; elts: t vector; siz: int; packed: bool} | Struct of
{ name: string
; elts: t vector
; bits: int
; byts: int
; packed: bool }
(** Uniquely named aggregate of heterogeneous types. Every cycle of (** Uniquely named aggregate of heterogeneous types. Every cycle of
recursive types contains a [Struct]. NOTE: recursive [Struct] recursive types contains a [Struct]. NOTE: recursive [Struct]
types are represented by cyclic values. *) types are represented by cyclic values. *)
| Opaque of {name: string; siz: int} | Opaque of {name: string}
(** Uniquely named aggregate type whose definition is hidden. *) (** Uniquely named aggregate type whose definition is hidden. *)
[@@deriving compare, equal, hash, sexp] [@@deriving compare, equal, hash, sexp]
@ -39,22 +44,30 @@ val int : t
val siz : t val siz : t
val ptr : t val ptr : t
val function_ : return:t option -> args:t vector -> t val function_ : return:t option -> args:t vector -> t
val integer : bits:int -> siz:int -> t val integer : bits:int -> byts:int -> t
val float : bits:int -> siz:int -> enc:[`Extended | `IEEE | `Pair] -> t val float : bits:int -> byts:int -> enc:[`Extended | `IEEE | `Pair] -> t
val pointer : elt:t -> t val pointer : elt:t -> t
val array : elt:t -> len:int -> siz:int -> t val array : elt:t -> len:int -> bits:int -> byts:int -> t
val tuple : t vector -> siz:int -> packed:bool -> t val tuple : t vector -> bits:int -> byts:int -> packed:bool -> t
val struct_ : name:string -> siz:int -> packed:bool -> t lazy_t vector -> t
val opaque : name:string -> siz:int -> t
(** Queries *) val struct_ :
name:string -> bits:int -> byts:int -> packed:bool -> t lazy_t vector -> t
val opaque : name:string -> t
val size_of : t -> int option (** Queries *)
val prim_bit_size_of : t -> int option
val is_sized : t -> bool val is_sized : t -> bool
(** Holds of types which are first-class and have a statically-known size. *) (** Holds of types which are first-class and have a statically-known size. *)
val bit_size_of : t -> int
(** The number of bits required to hold a value of the given type. Raises
unless [is_sized] holds. *)
val size_of : t -> int
(** The number of bytes between adjacent values of the given type, including
alignment padding. Raises unless is_sized holds. *)
val equivalent : t -> t -> bool val equivalent : t -> t -> bool
(** Equivalent types are those that denote the same sets of values in the (** Equivalent types are those that denote the same sets of values in the
semantic model. An equivalence relation. *) semantic model. An equivalence relation. *)

4
sledge/src/symbheap/exec.ml
Unescape View File

@ -328,7 +328,7 @@ let calloc_spec us reg num len =
let post = Sh.or_ (null_eq (Term.var reg)) (Sh.seg seg) in let post = Sh.or_ (null_eq (Term.var reg)) (Sh.seg seg) in
{xs; foot; sub; ms; post} {xs; foot; sub; ms; post}
let size_of_ptr = Option.value_exn (Term.size_of Typ.ptr) let size_of_ptr = Term.size_of Typ.ptr
(* { p-[_;_)->⟨W,_⟩ } (* { p-[_;_)->⟨W,_⟩ }
* posix_memalign r p s * posix_memalign r p s
@ -529,7 +529,7 @@ let nallocx_spec us reg siz =
let post = Sh.or_ (null_eq loc) (Sh.pure (Term.eq loc siz)) in let post = Sh.or_ (null_eq loc) (Sh.pure (Term.eq loc siz)) in
{xs; foot; sub; ms; post} {xs; foot; sub; ms; post}
let size_of_int_mul n = Term.mul (Option.value_exn (Term.size_of Typ.siz)) n let size_of_int_mul = Term.mul (Term.size_of Typ.siz)
(* { r-[_;_)->⟨m,_⟩ * i-[_;_)->⟨_,m⟩ * w=0 * n=0 } (* { r-[_;_)->⟨m,_⟩ * i-[_;_)->⟨_,m⟩ * w=0 * n=0 }
* mallctl r i w n * mallctl r i w n

Write Preview
Loading…
Cancel
Save