Merge pull request #1310 from goblint/unboxed

Unbox some types

src/cdomain/value/cdomains/floatDomain.ml

@@ -1036,11 +1036,11 @@ module FloatDomTupleImpl = struct
   type 'a m = (module FloatDomain with type t = 'a)
   (* only first-order polymorphism on functions
      -> use records to get around monomorphism restriction on arguments (Same trick as used in intDomain) *)
-  type 'b poly_in = { fi : 'a. 'a m -> 'b -> 'a }
-  type 'b poly_pr = { fp : 'a. 'a m -> 'a -> 'b }
-  type 'b poly2_pr = { f2p : 'a. 'a m -> 'a -> 'a -> 'b }
-  type poly1 = { f1 : 'a. 'a m -> 'a -> 'a }
-  type poly2 = { f2 : 'a. 'a m -> 'a -> 'a -> 'a }
+  type 'b poly_in = { fi : 'a. 'a m -> 'b -> 'a } [@@unboxed]
+  type 'b poly_pr = { fp : 'a. 'a m -> 'a -> 'b } [@@unboxed]
+  type 'b poly2_pr = { f2p : 'a. 'a m -> 'a -> 'a -> 'b } [@@unboxed]
+  type poly1 = { f1 : 'a. 'a m -> 'a -> 'a } [@@unboxed]
+  type poly2 = { f2 : 'a. 'a m -> 'a -> 'a -> 'a } [@@unboxed]
 
   let create r x (f1 : float_precision) =
     let f b g = if b then Some (g x) else None in

src/cdomain/value/cdomains/intDomain.ml

@@ -1802,7 +1802,7 @@ struct
   module I = BI
   (* We use these types for the functions in this module to make the intended meaning more explicit *)
   type t = Exc of BISet.t * Interval32.t
-  type inc = Inc of BISet.t
+  type inc = Inc of BISet.t [@@unboxed]
   let max_of_range r = Size.max_from_bit_range (Option.get (R.maximal r))
   let min_of_range r = Size.min_from_bit_range (Option.get (R.minimal r))
   let cardinality_of_range r = BI.add BI.one (BI.add (BI.neg (min_of_range r)) (max_of_range r))
@@ -3310,18 +3310,18 @@ module IntDomTupleImpl = struct
   type 'a m2 = (module SOverflow with type t = 'a and type int_t = int_t )
 
   (* only first-order polymorphism on functions -> use records to get around monomorphism restriction on arguments *)
-  type 'b poly_in  = { fi  : 'a. 'a m -> 'b -> 'a } (* inject *)
-  type 'b poly2_in  = { fi2  : 'a. 'a m2 -> 'b -> 'a } (* inject for functions that depend on int_t *)
-  type 'b poly2_in_ovc  = { fi2_ovc  : 'a. 'a m2 -> 'b -> 'a * overflow_info} (* inject for functions that depend on int_t *)
-
-  type 'b poly_pr  = { fp  : 'a. 'a m -> 'a -> 'b } (* project *)
-  type 'b poly_pr2  = { fp2  : 'a. 'a m2 -> 'a -> 'b } (* project for functions that depend on int_t *)
-  type 'b poly2_pr = {f2p: 'a. 'a m -> ?no_ov:bool -> 'a -> 'a -> 'b}
-  type poly1 = {f1: 'a. 'a m -> ?no_ov:bool -> 'a -> 'a} (* needed b/c above 'b must be different from 'a *)
-  type poly1_ovc = {f1_ovc: 'a. 'a m -> ?no_ov:bool -> 'a -> 'a * overflow_info } (* needed b/c above 'b must be different from 'a *)
-  type poly2 = {f2: 'a. 'a m -> ?no_ov:bool -> 'a -> 'a -> 'a}
-  type poly2_ovc = {f2_ovc: 'a. 'a m -> ?no_ov:bool -> 'a -> 'a -> 'a * overflow_info }
-  type 'b poly3 = { f3: 'a. 'a m -> 'a option } (* used for projection to given precision *)
+  type 'b poly_in  = { fi  : 'a. 'a m -> 'b -> 'a } [@@unboxed] (* inject *)
+  type 'b poly2_in  = { fi2  : 'a. 'a m2 -> 'b -> 'a } [@@unboxed] (* inject for functions that depend on int_t *)
+  type 'b poly2_in_ovc  = { fi2_ovc  : 'a. 'a m2 -> 'b -> 'a * overflow_info} [@@unboxed] (* inject for functions that depend on int_t *)
+
+  type 'b poly_pr  = { fp  : 'a. 'a m -> 'a -> 'b } [@@unboxed] (* project *)
+  type 'b poly_pr2  = { fp2  : 'a. 'a m2 -> 'a -> 'b } [@@unboxed] (* project for functions that depend on int_t *)
+  type 'b poly2_pr = {f2p: 'a. 'a m -> ?no_ov:bool -> 'a -> 'a -> 'b} [@@unboxed]
+  type poly1 = {f1: 'a. 'a m -> ?no_ov:bool -> 'a -> 'a} [@@unboxed] (* needed b/c above 'b must be different from 'a *)
+  type poly1_ovc = {f1_ovc: 'a. 'a m -> ?no_ov:bool -> 'a -> 'a * overflow_info } [@@unboxed] (* needed b/c above 'b must be different from 'a *)
+  type poly2 = {f2: 'a. 'a m -> ?no_ov:bool -> 'a -> 'a -> 'a} [@@unboxed]
+  type poly2_ovc = {f2_ovc: 'a. 'a m -> ?no_ov:bool -> 'a -> 'a -> 'a * overflow_info } [@@unboxed]
+  type 'b poly3 = { f3: 'a. 'a m -> 'a option } [@@unboxed] (* used for projection to given precision *)
   let create r x ((p1, p2, p3, p4, p5): int_precision) =
     let f b g = if b then Some (g x) else None in
     f p1 @@ r.fi (module I1), f p2 @@ r.fi (module I2), f p3 @@ r.fi (module I3), f p4 @@ r.fi (module I4), f p5 @@ r.fi (module I5)

src/domains/queries.ml

@@ -134,7 +134,7 @@ type 'a result = 'a
     Use [Analyses.ask_of_ctx] to convert [ctx] to [ask]. *)
 (* Must be in a singleton record due to second-order polymorphism.
    See https://ocaml.org/manual/polymorphism.html#s%3Ahigher-rank-poly. *)
-type ask = { f: 'a. 'a t -> 'a result }
+type ask = { f: 'a. 'a t -> 'a result } [@@unboxed]
 
 (* Result cannot implement Lattice.S because the function types are different due to GADT. *)
 module Result =
@@ -267,7 +267,7 @@ end
 
 (* The type any_query can't be directly defined in Any as t,
    because it also refers to the t from the outer scope. *)
-type any_query = Any: 'a t -> any_query
+type any_query = Any: 'a t -> any_query [@@unboxed]
 
 module Any =
 struct

src/framework/analyses.ml

@@ -175,7 +175,7 @@ exception Ctx_failure of string
 let ctx_failwith s = raise (Ctx_failure s) (* TODO: use everywhere in ctx *)
 
 (** Convert [ctx] to [Queries.ask]. *)
-let ask_of_ctx ctx: Queries.ask = { Queries.f = fun (type a) (q: a Queries.t) -> ctx.ask q }
+let ask_of_ctx ctx: Queries.ask = { Queries.f = ctx.ask }
 
 
 module type Spec =