From e40215085352b054f7e753e03cc7cfc7c25d9932 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 23 Nov 2023 12:11:29 +0200 Subject: [PATCH 1/2] Unbox some types --- src/cdomains/floatDomain.ml | 10 +++++----- src/cdomains/intDomain.ml | 26 +++++++++++++------------- src/domains/queries.ml | 4 ++-- 3 files changed, 20 insertions(+), 20 deletions(-) diff --git a/src/cdomains/floatDomain.ml b/src/cdomains/floatDomain.ml index 39d3744401..e3787541bd 100644 --- a/src/cdomains/floatDomain.ml +++ b/src/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 diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml index 376dab71c2..103f54413e 100644 --- a/src/cdomains/intDomain.ml +++ b/src/cdomains/intDomain.ml @@ -1895,7 +1895,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)) @@ -3403,18 +3403,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) diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 24e5d45593..f5fc832a9e 100644 --- a/src/domains/queries.ml +++ b/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 From be69a349aabf14a87980aa5415b36a81f36bd193 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 9 Jan 2024 12:00:25 +0200 Subject: [PATCH 2/2] Eta-reduce ask_of_ctx to avoid function allocation --- src/framework/analyses.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index 405df5b6a6..adb9b30d40 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -370,7 +370,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 =