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

[sledge] Update typ

Browse Source 
Reviewed By: mbouaziz

Differential Revision: D9846741

fbshipit-source-id: 1c2876954
master
Josh Berdine 6 years ago committed by Facebook Github Bot
parent 6a7c21e7c9
commit 742b181282
2 changed files with 107 additions and 139 deletions
Show Stats Download Patch File Download Diff File

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

@ -16,127 +16,112 @@ type t =
| Tuple of {elts: t vector; packed: bool}
| Struct of
{ name: string
; elts: t vector [@compare.ignore] (* possibly cyclic, name unique *)
; elts: t vector (* possibly cyclic, name unique *)
[@compare.ignore] [@sexp_drop_if fun _ -> true]
; packed: bool }
| Opaque of {name: string}
| Bytes
[@@deriving compare, sexp]
[@@deriving compare, hash, sexp]
let equal x y = compare x y = 0
let rec fmt ff typ =
let rec pp fs typ =
let pf pp =
Format.pp_open_box fs 2 ;
Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs pp
in
match typ with
| Function {return; args} ->
Format.fprintf ff "@[%a@ (@[%a@])@]" (option_fmt "%a" fmt) return fmts
args
| Integer {bits} -> Format.fprintf ff "@[i%i@]" bits
pf "%a@ (@[%a@])" (Option.pp "%a" pp) return pps args
| Integer {bits} -> pf "i%i" bits
| Float {bits; enc} ->
let fmt_enc ff = function
| `IEEE -> ()
| `Extended -> Format.pp_print_string ff "extend"
| `Pair -> Format.pp_print_string ff "pair"
let enc_str =
match enc with
| `IEEE -> ""
| `Extended -> "extend"
| `Pair -> "pair"
in
Format.fprintf ff "@[f%i%a@]" bits fmt_enc enc
| Pointer {elt} -> Format.fprintf ff "@[%a*@]" fmt elt
| Array {elt; len} -> Format.fprintf ff "@[[%i x %a]@]" len fmt elt
pf "f%i%s" bits enc_str
| Pointer {elt} -> pf "%a*" pp elt
| Array {elt; len} -> pf "[%i x %a]" len pp elt
| Tuple {elts; packed} ->
let opn, cls = if packed then ("<{", "}>") else ("{", "}") in
Format.fprintf ff "@[%s @[%a@] %s@]" opn fmts elts cls
| Struct {name} | Opaque {name} -> Format.fprintf ff "@[%%%s@]" name
| Bytes -> Format.fprintf ff "bytes"
pf "%s @[%a@] %s" opn pps elts cls
| Struct {name} | Opaque {name} -> pf "%%%s" name
and pps fs typs = Vector.pp ",@ " pp fs typs
and fmts ff typs = vector_fmt ",@ " fmt ff typs
let fmt_defn ff = function
let pp_defn fs = function
| Struct {name; elts; packed} ->
let opn, cls = if packed then ("<{", "}>") else ("{", "}") in
Format.fprintf ff "@[<2>%%%s =@ @[%s %a@] %s@]" name opn fmts elts cls
| Opaque {name} -> Format.fprintf ff "@[<2>%%%s =@ opaque@]" name
| typ -> fmt ff typ
Format.fprintf fs "@[<2>%%%s =@ @[%s %a@] %s@]" name opn pps elts cls
| Opaque {name} -> Format.fprintf fs "@[<2>%%%s =@ opaque@]" name
| typ -> pp fs typ
(** Invariants *)
let is_sized = function
| Function _ | Bytes -> false
| Function _ | Opaque _ -> false
| Integer _ | Float _ | Pointer _ | Array _ | Tuple _ | Struct _ -> true
| Opaque _ ->
(* This is optimisic since sizedness of Opaque types is indeterminate,
as they are not sized but may become sized through linking. *)
true
let invariant t =
Invariant.invariant [%here] t [%sexp_of: t]
@@ fun () ->
match t with
| Function {return; args} ->
assert (Option.for_all ~f:is_sized return) ;
assert (Vector.for_all ~f:is_sized args)
| Array {elt} -> assert (is_sized elt)
| Tuple {elts} | Struct {elts} -> assert (Vector.for_all ~f:is_sized elts)
| Integer {bits} | Float {bits} -> assert (bits > 0)
| Pointer _ | Opaque _ -> assert true
(** Constructors *)
let function_ ~return ~args = Function {return; args} |> check invariant
let integer ~bits = Integer {bits} |> check invariant
let float ~bits ~enc = Float {bits; enc} |> check invariant
let pointer ~elt = Pointer {elt} |> check invariant
let array ~elt ~len = Array {elt; len} |> check invariant
let tuple elts ~packed = Tuple {elts; packed} |> check invariant
let opaque ~name = Opaque {name} |> check invariant
let struct_ =
let defns : (string, t) Hashtbl.t = Hashtbl.create (module String) in
let dummy_typ = Opaque {name= "dummy"} in
fun ~name ~packed elt_thks ->
match Hashtbl.find defns name with
| Some typ -> typ
| None ->
(* Add placeholder defn to prevent computing [elts] in calls to
[struct] from [elts] for recursive occurrences of [name]. *)
let elts = Array.create ~len:(Vector.length elt_thks) dummy_typ in
let typ = Struct {name; elts= Vector.of_array elts; packed} in
Hashtbl.set defns ~key:name ~data:typ ;
Vector.iteri elt_thks ~f:(fun i (lazy elt) -> elts.(i) <- elt) ;
typ |> check invariant
(** Queries *)
let rec prim_bit_size_of = function
| Integer {bits} | Float {bits} -> Some bits
| Array {elt; len} ->
Option.map (prim_bit_size_of elt) ~f:(fun n -> n * len)
| Opaque _ | Function _ | Pointer _ | Tuple _ | Struct _ | Bytes -> None
let rec compatible t0 t1 =
match (t0, t1, prim_bit_size_of t0, prim_bit_size_of t1) with
| ( (Integer _ | Float _ | Pointer _)
, (Integer _ | Float _ | Pointer _)
, _
, _ ) ->
true
| Array {elt= t; len= m}, Array {elt= u; len= n}, _, _
when m = n && compatible t u ->
true
| ( (Integer _ | Float _ | Pointer _ | Array _)
, (Integer _ | Float _ | Pointer _ | Array _)
, Some s0
, Some s1 )
when s0 = s1 ->
| Function _ | Pointer _ | Tuple _ | Struct _ | Opaque _ -> None
let castable t0 t1 =
match (t0, t1) with
| Pointer _, Pointer _ -> true
| _ -> (
match (prim_bit_size_of t0, prim_bit_size_of t1) with
| Some n0, Some n1 -> Int.equal n0 n1
| _ -> false )
let rec convertible t0 t1 =
castable t0 t1
||
match (t0, t1) with
| (Integer _ | Float _ | Pointer _), (Integer _ | Float _ | Pointer _) ->
true
| Array {elt= t; len= m}, Array {elt= u; len= n} ->
m = n && convertible t u
| _ -> false
let mkFunction ~return ~args =
assert (
Option.for_all ~f:is_sized return && Vector.for_all ~f:is_sized args ) ;
Function {return; args}
let mkInteger ~bits = Integer {bits}
let mkFloat ~bits ~enc = Float {bits; enc}
let mkPointer ~elt = Pointer {elt}
let mkArray ~elt ~len =
assert (is_sized elt) ;
Array {elt; len}
let defns : (string, t) Hashtbl.t = Hashtbl.create (module String) ()
let mkTuple ~packed elts =
assert (Vector.for_all ~f:is_sized elts) ;
Tuple {elts; packed}
let mkStruct ~name ~packed elt_thks =
match Hashtbl.find defns name with
| Some typ -> typ
| None ->
(* Add placeholder defn to prevent computing [elts] in calls to
[mkStruct] from [elts] for recursive occurrences of [name]. *)
let elts =
Array.create ~len:(Vector.length elt_thks) (mkInteger ~bits:0)
in
let typ = Struct {name; elts= Vector.of_array elts; packed} in
Hashtbl.set defns ~key:name ~data:typ ;
Vector.iteri elt_thks ~f:(fun i elt_thk ->
let elt = Lazy.force elt_thk in
assert (is_sized elt) ;
elts.(i) <- elt ) ;
typ
let mkOpaque ~name = Opaque {name}
let mkBytes = Bytes
let i1 = mkInteger ~bits:1
let i8p = mkPointer ~elt:(mkInteger ~bits:8)

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

@ -10,10 +10,10 @@
type t = private
| Function of {return: t option; args: t vector}
(** (Global) function names have type Pointer to Function. *)
| Integer of {bits: int} (** Integer of given bitwidth *)
| Integer of {bits: int} (** Integer of given bitwidth. *)
| Float of {bits: int; enc: [`IEEE | `Extended | `Pair]}
(** Floating-point numbers of given bitwidth and encoding *)
| Pointer of {elt: t} (** Pointer to element type *)
(** Floating-point numbers of given bitwidth and encoding. *)
| Pointer of {elt: t} (** Pointer to element type. *)
| Array of {elt: t; len: int}
(** Statically-sized array of [len] elements of type [elt]. *)
| Tuple of {elts: t vector; packed: bool}
@ -24,53 +24,36 @@ type t = private
types are represented by cyclic values. *)
| Opaque of {name: string}
(** Uniquely named aggregate type whose definition is hidden. *)
| Bytes (** Dynamically-sized byte-array. *)
val compare : t -> t -> int
[@@deriving compare, hash, sexp]
val equal : t -> t -> bool
val pp : t pp
val pp_defn : t pp
val t_of_sexp : Sexp.t -> t
val sexp_of_t : t -> Sexp.t
val fmt : t fmt
val fmt_defn : t fmt
include Invariant.S with type t := t
(** Constructors *)
val mkFunction : return:t option -> args:t vector -> t
val mkInteger : bits:int -> t
val mkFloat : bits:int -> enc:[`Extended | `IEEE | `Pair] -> t
val mkPointer : elt:t -> t
val mkArray : elt:t -> len:int -> t
val mkTuple : packed:bool -> t vector -> t
val mkStruct : name:string -> packed:bool -> t lazy_t vector -> t
val mkOpaque : name:string -> t
val mkBytes : t
(** Special types *)
val i1 : t
(** Booleans are represented by 1-bit integers. *)
val i8p : t
(** Byte-pointers are effectively a universal type. *)
val function_ : return:t option -> args:t vector -> t
val integer : bits:int -> t
val float : bits:int -> enc:[`Extended | `IEEE | `Pair] -> t
val pointer : elt:t -> t
val array : elt:t -> len:int -> t
val tuple : t vector -> packed:bool -> t
val struct_ : name:string -> packed:bool -> t lazy_t vector -> t
val opaque : name:string -> t
(** Queries *)
val compatible : t -> t -> bool
(** Compatible types are those that can be cast or converted between,
perhaps with some loss of information. *)
val is_sized : t -> bool
(** Holds of types which are first-class and have a statically-known size. *)
val castable : t -> t -> bool
(** Castable types are those that can be cast between without loss of
information. An equivalence relation. *)
val convertible : t -> t -> bool
(** Convertible types are those that can be converted between, perhaps with
some loss of information. Not transitive: some admissible conversions
must be performed in multiple steps, such as from [Pointer] to [Integer]
to [Array]. *)

Write Preview
Loading…
Cancel
Save