From 410cb621a74cd8846b366a0ec39cb49c607d1b23 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 29 Jan 2024 16:28:59 +0100 Subject: [PATCH 1/2] Clean up some relational code. --- src/analyses/apron/affineEqualityAnalysis.apron.ml | 8 +------- src/cdomains/apron/affineEqualityDomain.apron.ml | 8 +++----- src/cdomains/apron/relationDomain.apron.ml | 1 - 3 files changed, 4 insertions(+), 13 deletions(-) diff --git a/src/analyses/apron/affineEqualityAnalysis.apron.ml b/src/analyses/apron/affineEqualityAnalysis.apron.ml index ce859d87b7..d4a1e5be2e 100644 --- a/src/analyses/apron/affineEqualityAnalysis.apron.ml +++ b/src/analyses/apron/affineEqualityAnalysis.apron.ml @@ -9,16 +9,10 @@ include RelationAnalysis let spec_module: (module MCPSpec) Lazy.t = lazy ( let module AD = AffineEqualityDomain.D2 (VectorMatrix.ArrayVector) (VectorMatrix.ArrayMatrix) in - let module RD: RelationDomain.RD = - struct - module V = AffineEqualityDomain.V - include AD - end - in let module Priv = (val RelationPriv.get_priv ()) in let module Spec = struct - include SpecFunctor (Priv) (RD) (RelationPrecCompareUtil.DummyUtil) + include SpecFunctor (Priv) (AD) (RelationPrecCompareUtil.DummyUtil) let name () = "affeq" end in diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index ea8a350d3c..dacdce659e 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -26,8 +26,6 @@ module Mpqf = struct let hash x = 31 * (Z.hash (get_den x)) + Z.hash (get_num x) end -module V = RelationDomain.V - (** It defines the type t of the affine equality domain (a struct that contains an optional matrix and an apron environment) and provides the functions needed for handling variables (which are defined by RelationDomain.D2) such as add_vars remove_vars. Furthermore, it provides the function get_coeff_vec that parses an apron expression into a vector of coefficients if the apron expression has an affine form. *) module VarManagement (Vec: AbstractVector) (Mx: AbstractMatrix)= @@ -240,7 +238,7 @@ struct include VarManagement (Vc) (Mx) module Bounds = ExpressionBounds (Vc) (Mx) - + module V = RelationDomain.V module Convert = SharedFunctions.Convert (V) (Bounds) (struct let allow_global = true end) (SharedFunctions.Tracked) type var = V.t @@ -703,9 +701,9 @@ struct let unmarshal t = t end -module D2(Vc: AbstractVector) (Mx: AbstractMatrix): RelationDomain.S3 with type var = Var.t = +module D2(Vc: AbstractVector) (Mx: AbstractMatrix): RelationDomain.RD with type var = Var.t = struct module D = D (Vc) (Mx) - include SharedFunctions.AssertionModule (V) (D) + include SharedFunctions.AssertionModule (D.V) (D) include D end diff --git a/src/cdomains/apron/relationDomain.apron.ml b/src/cdomains/apron/relationDomain.apron.ml index 48720b0382..82e7e20d20 100644 --- a/src/cdomains/apron/relationDomain.apron.ml +++ b/src/cdomains/apron/relationDomain.apron.ml @@ -128,7 +128,6 @@ end module type S3 = sig include S2 - val cil_exp_of_lincons1: Lincons1.t -> exp option val invariant: t -> Lincons1.t list end From eb1ad54e85985a45e66bc31194ac47f2306c7ecd Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Thu, 1 Feb 2024 13:51:37 +0100 Subject: [PATCH 2/2] Avoid intermediate definition of module in ApronAnalysis. --- src/analyses/apron/apronAnalysis.apron.ml | 11 ++--------- src/cdomains/apron/apronDomain.apron.ml | 7 ++++++- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml index 0ba17cdb35..f4d72c3d71 100644 --- a/src/analyses/apron/apronAnalysis.apron.ml +++ b/src/analyses/apron/apronAnalysis.apron.ml @@ -9,18 +9,11 @@ let spec_module: (module MCPSpec) Lazy.t = let module Man = (val ApronDomain.get_manager ()) in let module AD = ApronDomain.D2 (Man) in let diff_box = GobConfig.get_bool "ana.apron.invariant.diff-box" in - let module AD = (val if diff_box then (module ApronDomain.BoxProd (AD): ApronDomain.S3) else (module AD)) in - let module RD: RelationDomain.RD = - struct - module V = ApronDomain.V - include AD - type var = Apron.Var.t - end - in + let module AD = (val if diff_box then (module ApronDomain.BoxProd (AD): RelationDomain.RD) else (module AD)) in let module Priv = (val RelationPriv.get_priv ()) in let module Spec = struct - include SpecFunctor (Priv) (RD) (ApronPrecCompareUtil.Util) + include SpecFunctor (Priv) (AD) (ApronPrecCompareUtil.Util) let name () = "apron" end in diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index e78176fc41..2b8f360bc5 100644 --- a/src/cdomains/apron/apronDomain.apron.ml +++ b/src/cdomains/apron/apronDomain.apron.ml @@ -779,6 +779,7 @@ module type S2 = (* TODO: ExS3 or better extend RelationDomain.S3 directly?*) sig module Man: Manager + module V: RV include module type of AOps (Tracked) (Man) include SLattice with type t = Man.mt A.t @@ -803,6 +804,7 @@ sig include SLattice include AOps with type t := t + module V: RV module Tracked: RelationDomain.Tracked val assert_inv : t -> exp -> bool -> bool Lazy.t -> t @@ -813,6 +815,7 @@ end module D2 (Man: Manager) : S2 with module Man = Man = struct include D (Man) + module V = RelationDomain.V type marshal = OctagonD.marshal @@ -926,8 +929,10 @@ struct |> Lincons1Set.elements end -module BoxProd (D: S3): S3 = +module BoxProd (D: S3): RD = struct + module V = D.V + type var = V.t module BP0 = BoxProd0 (D) module Tracked = SharedFunctions.Tracked include BP0