diff --git a/conf/bench-yaml-validate.json b/conf/bench-yaml-validate.json index 2fcdb418da..d86bb07345 100644 --- a/conf/bench-yaml-validate.json +++ b/conf/bench-yaml-validate.json @@ -19,7 +19,6 @@ "access", "race", "escape", - "expRelation", "mhp", "assert", "var_eq", diff --git a/conf/bench-yaml.json b/conf/bench-yaml.json index 52f0b33347..f53414199b 100644 --- a/conf/bench-yaml.json +++ b/conf/bench-yaml.json @@ -19,7 +19,6 @@ "access", "race", "escape", - "expRelation", "mhp", "assert", "var_eq", diff --git a/conf/examples/medium-program.json b/conf/examples/medium-program.json index 5afc1aa2f8..190075f4ee 100644 --- a/conf/examples/medium-program.json +++ b/conf/examples/medium-program.json @@ -16,7 +16,6 @@ "access", "race", "escape", - "expRelation", "mhp", "assert", "pthreadMutexType", diff --git a/conf/examples/very-precise.json b/conf/examples/very-precise.json index 074d448a85..d76e35efdb 100644 --- a/conf/examples/very-precise.json +++ b/conf/examples/very-precise.json @@ -29,7 +29,6 @@ "access", "race", "escape", - "expRelation", "mhp", "assert", "pthreadMutexType", diff --git a/conf/ldv-races.json b/conf/ldv-races.json index 501e236d17..3d3fb3ba81 100644 --- a/conf/ldv-races.json +++ b/conf/ldv-races.json @@ -26,7 +26,6 @@ "access", "race", "escape", - "expRelation", "mhp", "assert", "var_eq", diff --git a/conf/svcomp-ghost.json b/conf/svcomp-ghost.json index b9c20a7463..6f9d48640e 100644 --- a/conf/svcomp-ghost.json +++ b/conf/svcomp-ghost.json @@ -24,7 +24,6 @@ "access", "race", "escape", - "expRelation", "mhp", "assert", "var_eq", diff --git a/conf/svcomp-yaml-validate.json b/conf/svcomp-yaml-validate.json index ece3327d41..8c6cf1e095 100644 --- a/conf/svcomp-yaml-validate.json +++ b/conf/svcomp-yaml-validate.json @@ -27,7 +27,6 @@ "access", "race", "escape", - "expRelation", "mhp", "assert", "var_eq", diff --git a/conf/svcomp-yaml.json b/conf/svcomp-yaml.json index a922b15db5..0b5f5a5edf 100644 --- a/conf/svcomp-yaml.json +++ b/conf/svcomp-yaml.json @@ -27,7 +27,6 @@ "access", "race", "escape", - "expRelation", "mhp", "assert", "var_eq", diff --git a/conf/svcomp21.json b/conf/svcomp21.json index 5c7ae0371a..5e78605eec 100644 --- a/conf/svcomp21.json +++ b/conf/svcomp21.json @@ -19,7 +19,6 @@ "access", "race", "escape", - "expRelation", "assert", "var_eq", "symb_locks", diff --git a/conf/svcomp22-intervals-novareq-affeq-apron.json b/conf/svcomp22-intervals-novareq-affeq-apron.json index f15fc97341..a777e9ee47 100644 --- a/conf/svcomp22-intervals-novareq-affeq-apron.json +++ b/conf/svcomp22-intervals-novareq-affeq-apron.json @@ -19,7 +19,6 @@ "access", "race", "escape", - "expRelation", "apron", "symb_locks", "region", diff --git a/conf/svcomp22-intervals-novareq-affeq-native.json b/conf/svcomp22-intervals-novareq-affeq-native.json index 3f91a56b18..e16d112cc2 100644 --- a/conf/svcomp22-intervals-novareq-affeq-native.json +++ b/conf/svcomp22-intervals-novareq-affeq-native.json @@ -20,7 +20,6 @@ "access", "race", "escape", - "expRelation", "symb_locks", "region", "thread", diff --git a/conf/svcomp22-intervals-novareq-octagon-apron.json b/conf/svcomp22-intervals-novareq-octagon-apron.json index d5d27b4e30..eb9cb33afa 100644 --- a/conf/svcomp22-intervals-novareq-octagon-apron.json +++ b/conf/svcomp22-intervals-novareq-octagon-apron.json @@ -19,7 +19,6 @@ "access", "race", "escape", - "expRelation", "apron", "symb_locks", "region", diff --git a/conf/svcomp22-intervals-novareq-polyhedra-apron.json b/conf/svcomp22-intervals-novareq-polyhedra-apron.json index 88a1aebdfe..f9f6b25537 100644 --- a/conf/svcomp22-intervals-novareq-polyhedra-apron.json +++ b/conf/svcomp22-intervals-novareq-polyhedra-apron.json @@ -19,7 +19,6 @@ "access", "race", "escape", - "expRelation", "apron", "symb_locks", "region", diff --git a/conf/svcomp22.json b/conf/svcomp22.json index c04fef59fb..38b2f807b3 100644 --- a/conf/svcomp22.json +++ b/conf/svcomp22.json @@ -19,7 +19,6 @@ "access", "race", "escape", - "expRelation", "assert", "var_eq", "symb_locks", diff --git a/conf/svcomp23.json b/conf/svcomp23.json index ef900e763a..dcdffd0966 100644 --- a/conf/svcomp23.json +++ b/conf/svcomp23.json @@ -23,7 +23,6 @@ "access", "race", "escape", - "expRelation", "mhp", "assert", "var_eq", diff --git a/conf/svcomp24-validate.json b/conf/svcomp24-validate.json index ff1a7adc8f..1d1c0db152 100644 --- a/conf/svcomp24-validate.json +++ b/conf/svcomp24-validate.json @@ -24,7 +24,6 @@ "access", "race", "escape", - "expRelation", "mhp", "assert", "var_eq", diff --git a/conf/svcomp24.json b/conf/svcomp24.json index dde5407056..e9cb9b22e4 100644 --- a/conf/svcomp24.json +++ b/conf/svcomp24.json @@ -24,7 +24,6 @@ "access", "race", "escape", - "expRelation", "mhp", "assert", "var_eq", diff --git a/conf/svcomp25-validate.json b/conf/svcomp25-validate.json index 0d414ef439..22c3f3b4d1 100644 --- a/conf/svcomp25-validate.json +++ b/conf/svcomp25-validate.json @@ -24,7 +24,6 @@ "access", "race", "escape", - "expRelation", "mhp", "assert", "var_eq", diff --git a/conf/svcomp25.json b/conf/svcomp25.json index bf1e545e2d..6827bcdec3 100644 --- a/conf/svcomp25.json +++ b/conf/svcomp25.json @@ -24,7 +24,6 @@ "access", "race", "escape", - "expRelation", "mhp", "assert", "var_eq", diff --git a/conf/svcomp26/level00.json b/conf/svcomp26/level00.json index 37efd79f26..7512c13a7a 100644 --- a/conf/svcomp26/level00.json +++ b/conf/svcomp26/level00.json @@ -18,7 +18,6 @@ "access", "race", "escape", - "expRelation", "mhp", "assert", "symb_locks", diff --git a/conf/svcomp26/level01.json b/conf/svcomp26/level01.json index ead6765999..7591312f44 100644 --- a/conf/svcomp26/level01.json +++ b/conf/svcomp26/level01.json @@ -19,7 +19,6 @@ "access", "race", "escape", - "expRelation", "mhp", "assert", "var_eq", diff --git a/conf/svcomp26/level02.json b/conf/svcomp26/level02.json index 022bb711d4..c4fb429b80 100644 --- a/conf/svcomp26/level02.json +++ b/conf/svcomp26/level02.json @@ -21,7 +21,6 @@ "access", "race", "escape", - "expRelation", "mhp", "assert", "var_eq", diff --git a/conf/svcomp26/level03.json b/conf/svcomp26/level03.json index 95ba4e533a..0a8d989143 100644 --- a/conf/svcomp26/level03.json +++ b/conf/svcomp26/level03.json @@ -21,7 +21,6 @@ "access", "race", "escape", - "expRelation", "mhp", "assert", "var_eq", diff --git a/conf/svcomp26/level04-validate.json b/conf/svcomp26/level04-validate.json index 394f33c4f4..24bf9adf0a 100644 --- a/conf/svcomp26/level04-validate.json +++ b/conf/svcomp26/level04-validate.json @@ -22,7 +22,6 @@ "access", "race", "escape", - "expRelation", "mhp", "assert", "var_eq", diff --git a/conf/svcomp26/level04.json b/conf/svcomp26/level04.json index 960b2bdb6b..c251235cce 100644 --- a/conf/svcomp26/level04.json +++ b/conf/svcomp26/level04.json @@ -22,7 +22,6 @@ "access", "race", "escape", - "expRelation", "mhp", "assert", "var_eq", diff --git a/conf/svcomp26/level05.json b/conf/svcomp26/level05.json index c8acd85030..720446a082 100644 --- a/conf/svcomp26/level05.json +++ b/conf/svcomp26/level05.json @@ -21,7 +21,6 @@ "access", "race", "escape", - "expRelation", "mhp", "assert", "var_eq", diff --git a/conf/svcomp2var.json b/conf/svcomp2var.json index 751b38358e..4bfa08ffbf 100644 --- a/conf/svcomp2var.json +++ b/conf/svcomp2var.json @@ -23,7 +23,6 @@ "access", "race", "escape", - "expRelation", "mhp", "assert", "var_eq", diff --git a/conf/traces-rel-toy.json b/conf/traces-rel-toy.json index 449d346b81..e8417b1e1d 100644 --- a/conf/traces-rel-toy.json +++ b/conf/traces-rel-toy.json @@ -1,7 +1,6 @@ { "ana": { "activated": [ - "expRelation", "base", "threadid", "threadflag", diff --git a/conf/zstd-race.json b/conf/zstd-race.json index d1a8848c06..ac0f2f0d36 100644 --- a/conf/zstd-race.json +++ b/conf/zstd-race.json @@ -1,7 +1,7 @@ { "ana": { "activated": [ - "expRelation", "base", "threadid", "threadflag", "threadreturn", + "base", "threadid", "threadflag", "threadreturn", "escape", "mutexEvents", "mutex", "access", "race", "mallocWrapper", "mhp", "assert", "symb_locks", "var_eq", "mallocFresh" ], diff --git a/scripts/test-param-activated.py b/scripts/test-param-activated.py index 27b98abc4e..1659c3b7eb 100755 --- a/scripts/test-param-activated.py +++ b/scripts/test-param-activated.py @@ -10,7 +10,7 @@ # copied from options activated_default = set([ - "expRelation", "base", "threadid", "threadflag", "threadreturn", + "base", "threadid", "threadflag", "threadreturn", "escape", "mutexEvents", "mutex", "access", "mallocWrapper", "mhp", "assert" ]) diff --git a/src/analyses/expRelation.ml b/src/analyses/expRelation.ml deleted file mode 100644 index 09a644f0f2..0000000000 --- a/src/analyses/expRelation.ml +++ /dev/null @@ -1,85 +0,0 @@ -(** Stateless symbolic comparison expression analysis ([expRelation]). *) - -(** An analysis specification to answer questions about how two expressions relate to each other. *) -(** Currently this works purely syntactically on the expressions, and only for {m =_{must}}. *) -(** Does not keep state, this is only formulated as an analysis to integrate well into the framework. *) - -open GoblintCil -open Analyses - -module Spec : Analyses.MCPSpec = -struct - include UnitAnalysis.Spec - - let name () = "expRelation" - - let rec canonize (e:exp) = - match e with - | BinOp (MinusA, BinOp(PlusA, e1, e2, typ1), e3, typ2) when typ1 = typ2 -> (* (e1+e2)-e3 --> (e1-e3)+e2 *) - begin (* where + is arithmetic + *) - let ce1 = canonize e1 in - let ce2 = canonize e2 in - let ce3 = canonize e3 in - BinOp(PlusA, BinOp(MinusA, ce1, ce3, typ1), ce2, typ2) - end - | BinOp (MinusA, e1, BinOp(PlusA, e2, e3, typ1), typ2) when typ1 = typ2 -> (* e1-(e2+e3) --> (e1-e2)-e3 *) - begin (* where + is arithmetic + *) - let ce1 = canonize e1 in - let ce2 = canonize e2 in - let ce3 = canonize e3 in - BinOp(MinusA, BinOp(MinusA, ce1, ce2, typ1), ce3, typ2) - end - | BinOp (MinusPP, BinOp(PlusPI, e1, e2, typ1), e3, typ2) -> (* *) - begin (* MinusPP PlusA *) - let ce1 = canonize e1 in (* / \ => / \ *) - let ce2 = canonize e2 in (* PlusPI \ MinusPP \ *) - let ce3 = canonize e3 in (* / \ \ / \ \ *) - BinOp(PlusA, BinOp(MinusPP, ce1, ce3, typ2), ce2, typ2) (* ptr i array1 ptr array1 i *) - end - | BinOp (MinusPP, BinOp(MinusPI, e1, e2, typ1), e3, typ2) -> (* *) - begin (* MinusPP MinusA *) - let ce1 = canonize e1 in (* / \ => / \ *) - let ce2 = canonize e2 in (* MinusPI \ MinusPP \ *) - let ce3 = canonize e3 in (* / \ \ / \ \ *) - BinOp(MinusA, BinOp(MinusPP, ce1, ce3, typ2), ce2, typ2) (* ptr i array1 ptr array1 i *) - end - | x -> x - - let isFloat e = Cilfacade.isFloatType (Cilfacade.typeOf e) - - let query man (type a) (q: a Queries.t): a Queries.result = - let lvalsEq l1 l2 = CilType.Lval.equal l1 l2 in (* == would be wrong here *) - match q with - | Queries.EvalInt (BinOp (Eq, e1, e2, t)) when not (isFloat e1) && Basetype.CilExp.equal (canonize e1) (canonize e2) -> - Queries.ID.of_bool (Cilfacade.get_ikind t) true - | Queries.EvalInt (BinOp (Lt, e1, e2, t)) when not (isFloat e1) -> - begin - (* Compare the cilint first in the hope that it is cheaper than the LVal comparison *) - match e1, e2 with - | BinOp(PlusA, Lval l1, Const(CInt(i,_,_)), _), Lval l2 when (Z.compare i Z.zero > 0 && lvalsEq l1 l2) -> - Queries.ID.of_bool (Cilfacade.get_ikind t) false (* c > 0 => (! x+c < x) *) - | Lval l1, BinOp(PlusA, Lval l2, Const(CInt(i,_,_)), _) when (Z.compare i Z.zero < 0 && lvalsEq l1 l2) -> - Queries.ID.of_bool (Cilfacade.get_ikind t) false (* c < 0 => (! x < x+c )*) - | BinOp(MinusA, Lval l1, Const(CInt(i,_,_)), _), Lval l2 when (Z.compare i Z.zero < 0 && lvalsEq l1 l2) -> - Queries.ID.of_bool (Cilfacade.get_ikind t) false (* c < 0 => (! x-c < x) *) - | Lval l1, BinOp(MinusA, Lval l2, Const(CInt(i,_,_)), _) when (Z.compare i Z.zero > 0 && lvalsEq l1 l2) -> - Queries.ID.of_bool (Cilfacade.get_ikind t) false (* c > 0 => (! x < x-c) *) - | _ -> - Queries.ID.top () - end - | Queries.EvalInt (BinOp (Eq, e1, e2, t)) when not (isFloat e1) -> - begin - match e1,e2 with - | BinOp(PlusA, Lval l1, Const(CInt(i,_,_)), _), Lval l2 - | Lval l2, BinOp(PlusA, Lval l1, Const(CInt(i,_,_)), _) - | BinOp(MinusA, Lval l1, Const(CInt(i,_,_)), _), Lval l2 - | Lval l2, BinOp(MinusA, Lval l1, Const(CInt(i,_,_)), _) when Z.compare i Z.zero <> 0 && (lvalsEq l1 l2) -> - Queries.ID.of_bool (Cilfacade.get_ikind t) false - | _ -> - Queries.ID.top () - end - | _ -> Queries.Result.top q -end - -let _ = - MCP.register_analysis (module Spec : MCPSpec) diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml index c5522d8141..aa5594f6cb 100644 --- a/src/analyses/mCP.ml +++ b/src/analyses/mCP.ml @@ -328,7 +328,19 @@ struct (* Abort to avoid infinite recursion *) false | _ -> - let r = fold_left (f ~q) (Result.top ()) @@ spec_list man.local in + let providers = + if get_bool "ana.queryproviders.exprelation" then + [(module ExpRelation.Provider : QueryProvider.S)] + else + [] + in + let r = fold_left (fun r (module P: QueryProvider.S) -> + let res = P.query q in + if M.tracing then M.trace "queryanswers" "query provider %s query %a -> answer %a" (P.name ()) Queries.Any.pretty anyq Result.pretty res; + Result.meet r res + ) (Result.top ()) providers + in + let r = fold_left (f ~q) r @@ spec_list man.local in do_sideg man !sides; Queries.Hashtbl.replace querycache anyq (Obj.repr r); r diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 18ea9f4716..d963bc1a13 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -339,15 +339,29 @@ "properties": { "activated": { "title": "ana.activated", - "description": "Lists of activated analyses.", + "description": "List of activated analyses.", "type": "array", "items": { "type": "string" }, "default": [ - "expRelation", "base", "threadid", "threadflag", "threadreturn", + "base", "threadid", "threadflag", "threadreturn", "escape", "mutexEvents", "mutex", "access", "race", "mallocWrapper", "mhp", "assert", "pthreadMutexType" ] }, + "queryproviders": { + "title": "ana.queryproviders", + "description": "Options for stateless query providers.", + "type": "object", + "properties": { + "exprelation": { + "title": "ana.queryproviders.exprelation", + "description": "Enable syntactic expression-relation queries.", + "type": "boolean", + "default": true + } + }, + "additionalProperties": false + }, "path_sens": { "title": "ana.path_sens", "description": "List of path-sensitive analyses", @@ -716,7 +730,7 @@ "domain": { "title": "ana.base.arrays.domain", "description": - "The domain that should be used for arrays. When employing the partition array domain, make sure to enable the expRelation analysis as well. When employing the unrolling array domain, make sure to set the ana.base.arrays.unrolling-factor >0.", + "The domain that should be used for arrays. When employing the partition array domain, make sure to enable ana.queryproviders.exprelation as well. When employing the unrolling array domain, make sure to set the ana.base.arrays.unrolling-factor >0.", "type": "string", "enum": ["trivial", "partitioned", "unroll"], "default": "trivial" diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml index 2cbe47dad9..6f5f06b350 100644 --- a/src/goblint_lib.ml +++ b/src/goblint_lib.ml @@ -37,6 +37,8 @@ module MCPAccess = MCPAccess Query results from different analyses for the same query are {{!Lattice.S.meet} met} for precision. *) module Queries = Queries +module QueryProvider = QueryProvider +module ExpRelation = ExpRelation (** MCP allows activated analyses to emit events to each other during the analysis. *) @@ -189,7 +191,6 @@ module AccessAnalysis = AccessAnalysis module WrapperFunctionAnalysis = WrapperFunctionAnalysis module TaintPartialContexts = TaintPartialContexts module UnassumeAnalysis = UnassumeAnalysis -module ExpRelation = ExpRelation module AbortUnless = AbortUnless module PtranalAnalysis = PtranalAnalysis module StartStateAnalysis = StartStateAnalysis diff --git a/src/queryProviders/expRelation.ml b/src/queryProviders/expRelation.ml new file mode 100644 index 0000000000..d4b02ea7c9 --- /dev/null +++ b/src/queryProviders/expRelation.ml @@ -0,0 +1,78 @@ +(** Stateless symbolic comparison expression query provider ([expRelation]). *) + +(** A query provider to answer questions about how two expressions relate to each other. *) +(** Currently this works purely syntactically on the expressions, and only for {m =_{must}}. *) + +open GoblintCil + +module Provider : QueryProvider.S = +struct + let name () = "expRelation" + + let rec canonize (e:exp) = + match e with + | BinOp (MinusA, BinOp(PlusA, e1, e2, typ1), e3, typ2) when typ1 = typ2 -> (* (e1+e2)-e3 --> (e1-e3)+e2 *) + begin (* where + is arithmetic + *) + let ce1 = canonize e1 in + let ce2 = canonize e2 in + let ce3 = canonize e3 in + BinOp(PlusA, BinOp(MinusA, ce1, ce3, typ1), ce2, typ2) + end + | BinOp (MinusA, e1, BinOp(PlusA, e2, e3, typ1), typ2) when typ1 = typ2 -> (* e1-(e2+e3) --> (e1-e2)-e3 *) + begin (* where + is arithmetic + *) + let ce1 = canonize e1 in + let ce2 = canonize e2 in + let ce3 = canonize e3 in + BinOp(MinusA, BinOp(MinusA, ce1, ce2, typ1), ce3, typ2) + end + | BinOp (MinusPP, BinOp(PlusPI, e1, e2, typ1), e3, typ2) -> (* *) + begin (* MinusPP PlusA *) + let ce1 = canonize e1 in (* / \ => / \ *) + let ce2 = canonize e2 in (* PlusPI \ MinusPP \ *) + let ce3 = canonize e3 in (* / \ \ / \ \ *) + BinOp(PlusA, BinOp(MinusPP, ce1, ce3, typ2), ce2, typ2) (* ptr i array1 ptr array1 i *) + end + | BinOp (MinusPP, BinOp(MinusPI, e1, e2, typ1), e3, typ2) -> (* *) + begin (* MinusPP MinusA *) + let ce1 = canonize e1 in (* / \ => / \ *) + let ce2 = canonize e2 in (* MinusPI \ MinusPP \ *) + let ce3 = canonize e3 in (* / \ \ / \ \ *) + BinOp(MinusA, BinOp(MinusPP, ce1, ce3, typ2), ce2, typ2) (* ptr i array1 ptr array1 i *) + end + | x -> x + + let isFloat e = Cilfacade.isFloatType (Cilfacade.typeOf e) + + let query (type a) (q: a Queries.t): a Queries.result = + let lvalsEq l1 l2 = CilType.Lval.equal l1 l2 in (* == would be wrong here *) + match q with + | Queries.EvalInt (BinOp (Eq, e1, e2, t)) when not (isFloat e1) && Basetype.CilExp.equal (canonize e1) (canonize e2) -> + Queries.ID.of_bool (Cilfacade.get_ikind t) true + | Queries.EvalInt (BinOp (Lt, e1, e2, t)) when not (isFloat e1) -> + begin + (* Compare the cilint first in the hope that it is cheaper than the LVal comparison *) + match e1, e2 with + | BinOp(PlusA, Lval l1, Const(CInt(i,_,_)), _), Lval l2 when (Z.compare i Z.zero > 0 && lvalsEq l1 l2) -> + Queries.ID.of_bool (Cilfacade.get_ikind t) false (* c > 0 => (! x+c < x) *) + | Lval l1, BinOp(PlusA, Lval l2, Const(CInt(i,_,_)), _) when (Z.compare i Z.zero < 0 && lvalsEq l1 l2) -> + Queries.ID.of_bool (Cilfacade.get_ikind t) false (* c < 0 => (! x < x+c )*) + | BinOp(MinusA, Lval l1, Const(CInt(i,_,_)), _), Lval l2 when (Z.compare i Z.zero < 0 && lvalsEq l1 l2) -> + Queries.ID.of_bool (Cilfacade.get_ikind t) false (* c < 0 => (! x-c < x) *) + | Lval l1, BinOp(MinusA, Lval l2, Const(CInt(i,_,_)), _) when (Z.compare i Z.zero > 0 && lvalsEq l1 l2) -> + Queries.ID.of_bool (Cilfacade.get_ikind t) false (* c > 0 => (! x < x-c) *) + | _ -> + Queries.ID.top () + end + | Queries.EvalInt (BinOp (Eq, e1, e2, t)) when not (isFloat e1) -> + begin + match e1,e2 with + | BinOp(PlusA, Lval l1, Const(CInt(i,_,_)), _), Lval l2 + | Lval l2, BinOp(PlusA, Lval l1, Const(CInt(i,_,_)), _) + | BinOp(MinusA, Lval l1, Const(CInt(i,_,_)), _), Lval l2 + | Lval l2, BinOp(MinusA, Lval l1, Const(CInt(i,_,_)), _) when Z.compare i Z.zero <> 0 && (lvalsEq l1 l2) -> + Queries.ID.of_bool (Cilfacade.get_ikind t) false + | _ -> + Queries.ID.top () + end + | _ -> Queries.Result.top q +end diff --git a/src/queryProviders/queryProvider.ml b/src/queryProviders/queryProvider.ml new file mode 100644 index 0000000000..fbb949800a --- /dev/null +++ b/src/queryProviders/queryProvider.ml @@ -0,0 +1,6 @@ +(** Interface for stateless providers which answer analysis queries. *) + +module type S = sig + val name : unit -> string + val query : 'a Queries.t -> 'a Queries.result +end diff --git a/tests/regression/00-sanity/33-hoare-over-paths.t b/tests/regression/00-sanity/33-hoare-over-paths.t index 9f88f836b0..6fe9e9605f 100644 --- a/tests/regression/00-sanity/33-hoare-over-paths.t +++ b/tests/regression/00-sanity/33-hoare-over-paths.t @@ -9,8 +9,7 @@ $ cat pretty.txt Mapping { 33-hoare-over-paths.c:9:7-9:8(main) -> - PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[expRelation:(), - mallocWrapper:(wrapper call:Unknown node, unique calls:{}), + PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[mallocWrapper:(wrapper call:Unknown node, unique calls:{}), base:({ Global { m -> mutex @@ -31,8 +30,7 @@ assert:(), pthreadMutexType:()], map:{})} 33-hoare-over-paths.c:10:5-10:10(main) -> - PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[expRelation:(), - mallocWrapper:(wrapper call:Unknown node, unique calls:{}), + PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[mallocWrapper:(wrapper call:Unknown node, unique calls:{}), base:({ Global { m -> mutex @@ -54,8 +52,7 @@ assert:(), pthreadMutexType:()], map:{})} 33-hoare-over-paths.c:11:5-11:24(main) -> - PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[expRelation:(), - mallocWrapper:(wrapper call:Unknown node, unique calls:{}), + PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[mallocWrapper:(wrapper call:Unknown node, unique calls:{}), base:({ Global { m -> mutex @@ -76,8 +73,7 @@ assert:(), pthreadMutexType:()], map:{})} 33-hoare-over-paths.c:15:5-15:27(main) -> - PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[expRelation:(), - mallocWrapper:(wrapper call:Unknown node, unique calls:{}), + PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[mallocWrapper:(wrapper call:Unknown node, unique calls:{}), base:({ Global { m -> mutex @@ -98,8 +94,7 @@ assert:(), pthreadMutexType:()], map:{})} 33-hoare-over-paths.c:16:5-16:24(main) -> - PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[expRelation:(), - mallocWrapper:(wrapper call:Unknown node, unique calls:{}), + PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[mallocWrapper:(wrapper call:Unknown node, unique calls:{}), base:({ Global { m -> mutex @@ -120,8 +115,7 @@ assert:(), pthreadMutexType:()], map:{})} 33-hoare-over-paths.c:33:10-33:11(main) -> - PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[expRelation:(), - mallocWrapper:(wrapper call:Unknown node, unique calls:{}), + PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[mallocWrapper:(wrapper call:Unknown node, unique calls:{}), base:({ Global { m -> mutex @@ -141,8 +135,7 @@ mhp:(), assert:(), pthreadMutexType:()], map:{}), - (MCP.D:[expRelation:(), - mallocWrapper:(wrapper call:Unknown node, unique calls:{}), + (MCP.D:[mallocWrapper:(wrapper call:Unknown node, unique calls:{}), base:({ Global { m -> mutex @@ -163,8 +156,7 @@ assert:(), pthreadMutexType:()], map:{})} 33-hoare-over-paths.c:7:1-34:1(main) -> - PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[expRelation:(), - mallocWrapper:(wrapper call:Unknown node, unique calls:{}), + PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[mallocWrapper:(wrapper call:Unknown node, unique calls:{}), base:({ Global { m -> mutex @@ -182,8 +174,7 @@ assert:(), pthreadMutexType:()], map:{})} 33-hoare-over-paths.c:7:1-34:1(main) -> - PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[expRelation:(), - mallocWrapper:(wrapper call:Unknown node, unique calls:{}), + PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[mallocWrapper:(wrapper call:Unknown node, unique calls:{}), base:({ Global { m -> mutex @@ -203,8 +194,7 @@ mhp:(), assert:(), pthreadMutexType:()], map:{}), - (MCP.D:[expRelation:(), - mallocWrapper:(wrapper call:Unknown node, unique calls:{}), + (MCP.D:[mallocWrapper:(wrapper call:Unknown node, unique calls:{}), base:({ Global { m -> mutex diff --git a/tests/regression/02-base/83-evalint-mustbeequal.c b/tests/regression/02-base/83-evalint-mustbeequal.c index df0edd654a..56c881f19a 100644 --- a/tests/regression/02-base/83-evalint-mustbeequal.c +++ b/tests/regression/02-base/83-evalint-mustbeequal.c @@ -1,4 +1,3 @@ -// PARAM: --set ana.activated[+] expRelation #include #include @@ -21,4 +20,4 @@ int main() { // base eval_rv_ask_mustbeequal via expRelation __goblint_check(p - p == 0); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/02-base/84-evalint-maybeequal.c b/tests/regression/02-base/84-evalint-maybeequal.c index d517098e78..6336bef057 100644 --- a/tests/regression/02-base/84-evalint-maybeequal.c +++ b/tests/regression/02-base/84-evalint-maybeequal.c @@ -1,4 +1,3 @@ -// PARAM: --set ana.activated[+] expRelation #include #include @@ -11,4 +10,4 @@ int main() { __goblint_check(!(x - 1 == x)); __goblint_check(!(x == x - 1)); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/02-base/85-evalint-maybeless.c b/tests/regression/02-base/85-evalint-maybeless.c index 1f339ea8b6..1dce76ad3b 100644 --- a/tests/regression/02-base/85-evalint-maybeless.c +++ b/tests/regression/02-base/85-evalint-maybeless.c @@ -1,4 +1,3 @@ -// PARAM: --set ana.activated[+] expRelation #include #include @@ -11,4 +10,4 @@ int main() { __goblint_check(!(x - (-1) < x)); __goblint_check(!(x < x - 1)); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/36-apron/34-large-bigint.c b/tests/regression/36-apron/34-large-bigint.c index 1eead3a1d4..d8a3b5404c 100644 --- a/tests/regression/36-apron/34-large-bigint.c +++ b/tests/regression/36-apron/34-large-bigint.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[-] expRelation +// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --disable ana.queryproviders.exprelation #include void main() { diff --git a/tests/regression/witness/violation.t/run.t b/tests/regression/witness/violation.t/run.t index 1fc408635e..6a4e061f7a 100644 --- a/tests/regression/witness/violation.t/run.t +++ b/tests/regression/witness/violation.t/run.t @@ -20,7 +20,7 @@ Violation witness for a correct program can be refuted by proving the program co If a correct progtam cannot be proven correct, return `unknown` for the violation witness: - $ goblint --set ana.activated[-] expRelation --enable ana.sv-comp.functions --enable ana.sv-comp.enabled --set witness.yaml.entry-types[+] violation_sequence --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )" correct-hard.c --set witness.yaml.validate correct-hard.yml + $ goblint --disable ana.queryproviders.exprelation --enable ana.sv-comp.functions --enable ana.sv-comp.enabled --set witness.yaml.entry-types[+] violation_sequence --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )" correct-hard.c --set witness.yaml.validate correct-hard.yml [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) ) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7