From d1b62287dc64b825b3640d5b95ce90394a85d725 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 4 Dec 2023 19:37:06 +0100 Subject: [PATCH] Move `Environment` things into `GobApron` --- .../apron/affineEqualityDomain.apron.ml | 14 ++--- src/cdomains/apron/apronDomain.apron.ml | 25 +++----- src/cdomains/apron/gobApron.apron.ml | 61 +++++++++++++++++++ src/cdomains/apron/sharedFunctions.apron.ml | 60 ------------------ 4 files changed, 76 insertions(+), 84 deletions(-) diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index 0054f685b1..ff2339cd6f 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -32,7 +32,6 @@ module V = RelationDomain.V 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)= struct - include SharedFunctions.EnvOps module Vector = Vec (Mpqf) module Matrix = Mx(Mpqf) (Vec) @@ -77,16 +76,18 @@ struct let change_d t new_env add del = timing_wrap "dimension change" (change_d t new_env add) del + let vars x = Environment.ivars_only x.env + let add_vars t vars = let t = copy t in - let env' = add_vars t.env vars in + let env' = Environment.add_vars t.env vars in change_d t env' true false let add_vars t vars = timing_wrap "add_vars" (add_vars t) vars let drop_vars t vars del = let t = copy t in - let env' = remove_vars t.env vars in + let env' = Environment.remove_vars t.env vars in change_d t env' false del let drop_vars t vars = timing_wrap "drop_vars" (drop_vars t) vars @@ -101,7 +102,7 @@ struct t.env <- t'.env let remove_filter t f = - let env' = remove_filter t.env f in + let env' = Environment.remove_filter t.env f in change_d t env' false false let remove_filter t f = timing_wrap "remove_filter" (remove_filter t) f @@ -113,19 +114,18 @@ struct let keep_filter t f = let t = copy t in - let env' = keep_filter t.env f in + let env' = Environment.keep_filter t.env f in change_d t env' false false let keep_filter t f = timing_wrap "keep_filter" (keep_filter t) f let keep_vars t vs = let t = copy t in - let env' = keep_vars t.env vs in + let env' = Environment.keep_vars t.env vs in change_d t env' false false let keep_vars t vs = timing_wrap "keep_vars" (keep_vars t) vs - let vars t = vars t.env let mem_var t var = Environment.mem_var t.env var diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index ef9eac9bef..077aa971f2 100644 --- a/src/cdomains/apron/apronDomain.apron.ml +++ b/src/cdomains/apron/apronDomain.apron.ml @@ -208,7 +208,6 @@ module type AOpsExtra = sig type t val copy : t -> t - val vars_as_array : t -> Var.t array val vars : t -> Var.t list type marshal val unmarshal : marshal -> t @@ -247,15 +246,6 @@ struct let copy = A.copy Man.mgr - let vars_as_array d = - let ivs, fvs = Environment.vars (A.env d) in - assert (Array.length fvs = 0); (* shouldn't ever contain floats *) - ivs - - let vars d = - let ivs = vars_as_array d in - List.of_enum (Array.enum ivs) - (* marshal type: Abstract0.t and an array of var names *) type marshal = Man.mt Abstract0.t * string array @@ -265,30 +255,32 @@ struct let env = Environment.make vars [||] in {abstract0; env} + let vars x = Environment.ivars_only @@ A.env x + let marshal (x: t): marshal = - let vars = Array.map Var.to_string (vars_as_array x) in + let vars = Array.map Var.to_string (Array.of_list (Environment.ivars_only (A.env x))) in x.abstract0, vars let mem_var d v = Environment.mem_var (A.env d) v let add_vars_with nd vs = - let env' = EnvOps.add_vars (A.env nd) vs in + let env' = Environment.add_vars (A.env nd) vs in A.change_environment_with Man.mgr nd env' false let remove_vars_with nd vs = - let env' = EnvOps.remove_vars (A.env nd) vs in + let env' = Environment.remove_vars (A.env nd) vs in A.change_environment_with Man.mgr nd env' false let remove_filter_with nd f = - let env' = EnvOps.remove_filter (A.env nd) f in + let env' = Environment.remove_filter (A.env nd) f in A.change_environment_with Man.mgr nd env' false let keep_vars_with nd vs = - let env' = EnvOps.keep_vars (A.env nd) vs in + let env' = Environment.keep_vars (A.env nd) vs in A.change_environment_with Man.mgr nd env' false let keep_filter_with nd f = - let env' = EnvOps.keep_filter (A.env nd) f in + let env' = Environment.keep_filter (A.env nd) f in A.change_environment_with Man.mgr nd env' false let forget_vars_with nd vs = @@ -885,7 +877,6 @@ struct let unmarshal (b, d) = (BoxD.unmarshal b, D.unmarshal d) let mem_var (_, d) v = D.mem_var d v - let vars_as_array (_, d) = D.vars_as_array d let vars (_, d) = D.vars d let pretty_diff () ((_, d1), (_, d2)) = D.pretty_diff () (d1, d2) diff --git a/src/cdomains/apron/gobApron.apron.ml b/src/cdomains/apron/gobApron.apron.ml index df20f3c59d..c39a3e42db 100644 --- a/src/cdomains/apron/gobApron.apron.ml +++ b/src/cdomains/apron/gobApron.apron.ml @@ -35,3 +35,64 @@ struct ) |> of_enum end + +(** A few code elements for environment changes from functions as remove_vars etc. have been moved to sharedFunctions as they are needed in a similar way inside affineEqualityDomain. + A module that includes various methods used by variable handling operations such as add_vars, remove_vars etc. in apronDomain and affineEqualityDomain. *) +module Environment = +struct + include Environment + + let ivars_only env = + let ivs, fvs = Environment.vars env in + assert (Array.length fvs = 0); (* shouldn't ever contain floats *) + List.of_enum (Array.enum ivs) + + let add_vars env vs = + let vs' = + vs + |> List.enum + |> Enum.filter (fun v -> not (Environment.mem_var env v)) + |> Array.of_enum + in + Environment.add env vs' [||] + + let remove_vars env vs = + let vs' = + vs + |> List.enum + |> Enum.filter (fun v -> Environment.mem_var env v) + |> Array.of_enum + in + Environment.remove env vs' + + let remove_filter env f = + let vs' = + ivars_only env + |> List.enum + |> Enum.filter f + |> Array.of_enum + in + Environment.remove env vs' + + let keep_vars env vs = + (* Instead of iterating over all vars in env and doing a linear lookup in vs just to remove them, + make a new env with just the desired vs. *) + let vs' = + vs + |> List.enum + |> Enum.filter (fun v -> Environment.mem_var env v) + |> Array.of_enum + in + Environment.make vs' [||] + + let keep_filter env f = + (* Instead of removing undesired vars, + make a new env with just the desired vars. *) + let vs' = + ivars_only env + |> List.enum + |> Enum.filter f + |> Array.of_enum + in + Environment.make vs' [||] +end diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 9c229e2d64..e66be00ae4 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -255,66 +255,6 @@ struct include CilOfApron (V) end -(** A few code elements for environment changes from functions as remove_vars etc. have been moved to sharedFunctions as they are needed in a similar way inside affineEqualityDomain. - A module that includes various methods used by variable handling operations such as add_vars, remove_vars etc. in apronDomain and affineEqualityDomain. *) -module EnvOps = -struct - let vars env = - let ivs, fvs = Environment.vars env in - assert (Array.length fvs = 0); (* shouldn't ever contain floats *) - List.of_enum (Array.enum ivs) - - let add_vars env vs = - let vs' = - vs - |> List.enum - |> Enum.filter (fun v -> not (Environment.mem_var env v)) - |> Array.of_enum - in - Environment.add env vs' [||] - - let remove_vars env vs = - let vs' = - vs - |> List.enum - |> Enum.filter (fun v -> Environment.mem_var env v) - |> Array.of_enum - in - Environment.remove env vs' - - let remove_filter env f = - let vs' = - vars env - |> List.enum - |> Enum.filter f - |> Array.of_enum - in - Environment.remove env vs' - - let keep_vars env vs = - (* Instead of iterating over all vars in env and doing a linear lookup in vs just to remove them, - make a new env with just the desired vs. *) - let vs' = - vs - |> List.enum - |> Enum.filter (fun v -> Environment.mem_var env v) - |> Array.of_enum - in - Environment.make vs' [||] - - let keep_filter env f = - (* Instead of removing undesired vars, - make a new env with just the desired vars. *) - let vs' = - vars env - |> List.enum - |> Enum.filter f - |> Array.of_enum - in - Environment.make vs' [||] - -end - (** A more specific module type for RelationDomain.RelD2 with ConvBounds integrated and various apron elements. It is designed to be the interface for the D2 modules in affineEqualityDomain and apronDomain and serves as a functor argument for AssertionModule. *) module type AssertionRelS =