diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index a3518b7469..e336da6a63 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -696,21 +696,41 @@ struct let query man (type a) (q: a Queries.t): a Queries.result = let open Queries in + let ask = Analyses.ask_of_man man in let st = man.local in let eval_int e no_ov = let esimple = replace_deref_exps man.ask e in read_from_globals_wrapper - (Analyses.ask_of_man man) + ask man.global st esimple - (fun rel' e' -> RD.eval_int (Analyses.ask_of_man man) rel' e' no_ov) + (fun rel' e' -> RD.eval_int ask rel' e' no_ov) + in + let eval_transition_int e no_ov = + let e = visitCilExpr TransitionInvariant.extvar_localize_visitor e in (* RichVarinfo-s are global by default, but make AnyPrev-s of locals local for Apron expression conversion *) + let esimple = replace_deref_exps man.ask e in + read_from_globals_wrapper + ask + man.global st esimple + (fun rel' e' -> + let rel' = transition_state ask rel' in + if M.tracing then M.trace "evaltransitionint" "relation transition rel': %a" RD.pretty rel'; + RD.eval_int ask rel' e' no_ov + ) in match q with | EvalInt e -> if M.tracing then M.traceli "evalint" "relation query %a (%a)" d_exp e d_plainexp e; if M.tracing then M.trace "evalint" "relation st: %a" D.pretty man.local; - let r = eval_int e (no_overflow (Analyses.ask_of_man man) e) in + let r = eval_int e (no_overflow ask e) in if M.tracing then M.traceu "evalint" "relation query %a -> %a" d_exp e ID.pretty r; r + | EvalTransitionInt e -> + let e = Cilfacade.stripOuterBoolCast e in (* For normal EvalInt these are stripped by base *) + if M.tracing then M.traceli "evaltransitionint" "relation query %a (%a)" d_exp e d_plainexp e; + if M.tracing then M.trace "evaltransitionint" "relation st: %a" D.pretty man.local; + let r = eval_transition_int e (no_overflow ask e) in + if M.tracing then M.traceu "evaltransitionint" "relation query %a -> %a" d_exp e ID.pretty r; + r | Queries.IterSysVars (vq, vf) -> let vf' x = vf (Obj.repr x) in Priv.iter_sys_vars man.global vq vf' diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index 7847892753..c1a70038ce 100644 --- a/src/common/util/cilfacade.ml +++ b/src/common/util/cilfacade.ml @@ -477,6 +477,11 @@ let exp_is_boolean = function | BinOp ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), _, _, _) -> true | _ -> false +let stripOuterBoolCast = function + | CastE (_, TInt (IBool, _), e) -> e (* TODO: keep explicit cast? *) + | Const (CInt (b, IBool, s)) -> Const (CInt (b, IInt, s)) + | e -> e + (** Remove {!PointerConversion} casts from {!BinOp} operands, if present. CIL adds these casts for pointer comparisons. *) let remove_binop_pointer_conversions e1 e2 = diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 0b67a85e1e..c5a34e3a28 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -107,6 +107,7 @@ type _ t = | MayBeThreadReturn: MayBool.t t | EvalFunvar: exp -> AD.t t | EvalInt: exp -> ID.t t + | EvalTransitionInt: exp -> ID.t t | EvalStr: exp -> SD.t t | EvalLength: exp -> SizeDomain.t t (* length of an array or string *) | EvalValue: exp -> VD.t t @@ -193,6 +194,7 @@ struct | MustBeSingleThreaded _ -> (module MustBool) | MustBeUniqueThread -> (module MustBool) | EvalInt _ -> (module ID) + | EvalTransitionInt _ -> (module ID) | EvalLength _ -> (module SizeDomain) | EvalMutexAttr _ -> (module MutexAttrDomain) | EvalValue _ -> (module VD) @@ -273,6 +275,7 @@ struct | MustBeSingleThreaded _ -> MustBool.top () | MustBeUniqueThread -> MustBool.top () | EvalInt _ -> ID.top () + | EvalTransitionInt _ -> ID.top () | EvalLength _ -> SizeDomain.top () | EvalMutexAttr _ -> MutexAttrDomain.top () | EvalValue _ -> VD.top () @@ -357,6 +360,7 @@ struct | Any (MustBeProtectedBy x1), Any (MustBeProtectedBy x2) -> compare_mustbeprotectedby x1 x2 | Any (EvalFunvar e1), Any (EvalFunvar e2) -> CilType.Exp.compare e1 e2 | Any (EvalInt e1), Any (EvalInt e2) -> CilType.Exp.compare e1 e2 + | Any (EvalTransitionInt e1), Any (EvalTransitionInt e2) -> CilType.Exp.compare e1 e2 | Any (EvalStr e1), Any (EvalStr e2) -> CilType.Exp.compare e1 e2 | Any (EvalLength e1), Any (EvalLength e2) -> CilType.Exp.compare e1 e2 | Any (EvalMutexAttr e1), Any (EvalMutexAttr e2) -> CilType.Exp.compare e1 e2 @@ -419,6 +423,7 @@ struct | Any (MustBeProtectedBy x) -> hash_mustbeprotectedby x | Any (EvalFunvar e) -> CilType.Exp.hash e | Any (EvalInt e) -> CilType.Exp.hash e + | Any (EvalTransitionInt e) -> CilType.Exp.hash e | Any (EvalStr e) -> CilType.Exp.hash e | Any (EvalLength e) -> CilType.Exp.hash e | Any (EvalMutexAttr e) -> CilType.Exp.hash e @@ -479,6 +484,7 @@ struct | Any MayBeThreadReturn -> Pretty.dprintf "MayBeThreadReturn" | Any (EvalFunvar e) -> Pretty.dprintf "EvalFunvar %a" CilType.Exp.pretty e | Any (EvalInt e) -> Pretty.dprintf "EvalInt %a" CilType.Exp.pretty e + | Any (EvalTransitionInt e) -> Pretty.dprintf "EvalTransitionInt %a" CilType.Exp.pretty e | Any (EvalStr e) -> Pretty.dprintf "EvalStr %a" CilType.Exp.pretty e | Any (EvalLength e) -> Pretty.dprintf "EvalLength %a" CilType.Exp.pretty e | Any (EvalValue e) -> Pretty.dprintf "EvalValue %a" CilType.Exp.pretty e @@ -552,6 +558,12 @@ let eval_bool (ask: ask) e: BoolDomain.FlatBool.t = | v when ID.is_bot v || ID.is_bot_ikind v -> `Bot | v -> BatOption.map_default (fun b -> `Lifted b) `Top (ID.to_bool v) +let eval_transition_bool (ask: ask) e: BoolDomain.FlatBool.t = + let e' = CastE (Internal, TInt (IBool, []), e) in + match ask.f (EvalTransitionInt e') with + | v when ID.is_bot v || ID.is_bot_ikind v -> `Bot + | v -> BatOption.map_default (fun b -> `Lifted b) `Top (ID.to_bool v) + module Set = BatSet.Make (Any) module Hashtbl = BatHashtbl.Make (Any) diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index 90a01e1c3a..2fc8349f39 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -16,11 +16,6 @@ let intmax_t = lazy ( !res ) -let stripOuterBoolCast = function - | CastE (_, TInt (IBool, _), e) -> e (* TODO: keep explicit cast? *) - | Const (CInt (b, IBool, s)) -> Const (CInt (b, IInt, s)) - | e -> e - (** C standard library functions. These are specified by the C standard. *) let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ @@ -907,9 +902,9 @@ let linux_kernel_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ (** Goblint functions. *) let goblint_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__goblint_unknown", unknown [drop' [w]]); - ("__goblint_check", special [__ "exp" []] @@ fun exp -> Assert { exp = stripOuterBoolCast exp; check = true; refine = false }); - ("__goblint_assume", special [__ "exp" []] @@ fun exp -> Assert { exp = stripOuterBoolCast exp; check = false; refine = true }); - ("__goblint_assert", special [__ "exp" []] @@ fun exp -> Assert { exp = stripOuterBoolCast exp; check = true; refine = get_bool "sem.assert.refine" }); + ("__goblint_check", special [__ "exp" []] @@ fun exp -> Assert { exp = Cilfacade.stripOuterBoolCast exp; check = true; refine = false }); + ("__goblint_assume", special [__ "exp" []] @@ fun exp -> Assert { exp = Cilfacade.stripOuterBoolCast exp; check = false; refine = true }); + ("__goblint_assert", special [__ "exp" []] @@ fun exp -> Assert { exp = Cilfacade.stripOuterBoolCast exp; check = true; refine = get_bool "sem.assert.refine" }); ("__goblint_globalize", special [__ "ptr" []] @@ fun ptr -> Globalize ptr); ("__goblint_split_begin", unknown [drop "exp" []]); ("__goblint_split_end", unknown [drop "exp" []]); diff --git a/src/witness/transitionInvariant.ml b/src/witness/transitionInvariant.ml index 5e21f8e493..d6624f5292 100644 --- a/src/witness/transitionInvariant.ml +++ b/src/witness/transitionInvariant.ml @@ -50,3 +50,57 @@ let exp_is_suitable ?scope e = let e = visitCilExpr var_replace_with_original_visitor e in (* replace extended vars with originals, so scope check passes (RichVarinfo-s are all global) *) not (exp_contains_tmp e || exp_contains_anon_comp_offset e) && GobOption.for_all (fun scope -> exp_is_in_scope scope e) scope + +let extvar_localize_visitor = object + inherit nopCilVisitor + + method! vvrbl (vi: varinfo) = + match ExtVarMap.from_varinfo vi with + | None -> SkipChildren + | Some (AnyPrev vi') -> ChangeTo {vi with vglob = vi'.vglob} (* still ExtVar but with original locality *) +end + + +module InvariantParser (Base: module type of WitnessUtil.InvariantParser) = +struct + open GobResult.Syntax + + let anyprev_regexp = Str.regexp {|\\at( *\([A-Za-z_][A-Za-z0-9_]*\) *, *AnyPrev *)|} + let anyprev_vname var = Printf.sprintf "__at_%s_AnyPrev__" var + + module StringSet = Set.Make (String) + + let parse_cabs inv = + let anyprev_vars = ref StringSet.empty in (* collect (replaced) AnyPrev variable names from invariant *) + (* regex replace AnyPrev syntax with a corresponding valid C variable name *) + let inv' = Str.global_substitute anyprev_regexp (fun m -> + let var = Str.matched_group 1 m in + anyprev_vars := StringSet.add var !anyprev_vars; + anyprev_vname var + ) inv + in + let+ inv_cabs = Base.parse_cabs inv' in + (inv_cabs, !anyprev_vars) + + let extvar_fix_visitor = object + inherit nopCilVisitor + + method! vvrbl (vi: varinfo) = + match ExtVarMap.from_varinfo vi with + | None -> SkipChildren + | Some v -> ChangeTo (ExtVarMap.to_varinfo v) (* replace ExtVar vi with the original version of itself (after modifying vname below) *) + end + + let parse_cil inv_parser ?check ~fundec ~loc (inv_cabs, anyprev_vars) = + (* TODO: support AnyPrev on locals and globals *) + let locals' = + StringSet.fold (fun var acc -> + match List.find (fun local -> local.vname = var) fundec.slocals with (* TODO: List.find isn't the most efficient *) + | local -> {(ExtVarMap.to_varinfo (AnyPrev local)) with vname = anyprev_vname var} :: acc (* override vname so Base.parse_cil would use the regex replaced name *) + | exception Not_found -> failwith "AnyPrev variable isn't local" + ) anyprev_vars fundec.slocals + in + let fundec' = {fundec with slocals = locals'} in + let+ e = Base.parse_cil inv_parser ?check ~fundec:fundec' ~loc inv_cabs in + visitCilExpr extvar_fix_visitor e (* replace ExtVar varinfos with overridden vname with original unrenamed ExtVars varinfos *) +end diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index b9ad772bf2..ccd2a85934 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -532,6 +532,7 @@ struct module LvarS = Locator.ES module WitnessInvariant = WitnessUtil.YamlInvariant (FileCfg) module InvariantParser = WitnessUtil.InvariantParser + module TransitionInvariantParser = TransitionInvariant.InvariantParser (InvariantParser) module VR = ValidationResult module FundecH = GobHashtbl.Make (CilType.Fundec) @@ -618,6 +619,56 @@ struct M.info ~category:Witness ~loc:msgLoc "invariant has invalid syntax: %s" inv in + let validate_lvars_transition_invariant ~loc ~lvars inv = + let msgLoc: M.Location.t = CilLocation loc in + + match TransitionInvariantParser.parse_cabs inv with + | Ok inv_cabs -> + (* do parse_cil at most once per function *) + let memo = FundecH.create 1 in (* loc should just be in one function *) + let parse_cil fundec = + TransitionInvariantParser.parse_cil inv_parser ~fundec ~loc inv_cabs + in + + let result = LvarS.fold (fun ((n, _) as lvar) (acc: VR.t) -> + let fundec = Node.find_fundec n in + + let result: VR.result = match FundecH.find_or_add_default_delayed ~default:parse_cil memo fundec with + | Ok inv_exp -> + begin match Queries.eval_transition_bool {f = (fun (type a) (q: a Queries.t) -> ask_local lvar q)} inv_exp with + | `Bot -> Option.get (VR.result_of_enum (VR.bot ())) (* dead code *) + | `Lifted true -> Confirmed + | `Lifted false -> Refuted + | `Top -> Unconfirmed + end + | Error e -> + ParseError + in + VR.join acc (VR.result_to_enum result) + ) lvars (VR.bot ()) + in + + begin match Option.get (VR.result_of_enum result) with + | Confirmed -> + incr cnt_confirmed; + M.success ~category:Witness ~loc:msgLoc "invariant confirmed: %s" inv + | Unconfirmed -> + incr cnt_unconfirmed; + M.warn ~category:Witness ~loc:msgLoc "invariant unconfirmed: %s" inv + | Refuted -> + incr cnt_refuted; + M.error ~category:Witness ~loc:msgLoc "invariant refuted: %s" inv + | ParseError -> + incr cnt_error; + M.error ~category:Witness ~loc:msgLoc "CIL couldn't parse invariant: %s" inv; + M.info ~category:Witness ~loc:msgLoc "invariant has undefined variables or side effects: %s" inv + end + | Error e -> + incr cnt_error; + M.error ~category:Witness ~loc:msgLoc "Frontc couldn't parse invariant: %s" inv; + M.info ~category:Witness ~loc:msgLoc "invariant has invalid syntax: %s" inv + in + let validate_invariant_set (invariant_set: YamlWitnessType.InvariantSet.t) = let validate_location_invariant (location_invariant: YamlWitnessType.InvariantSet.LocationInvariant.t) = @@ -644,6 +695,18 @@ struct M.warn ~category:Witness ~loc:(CilLocation loc) "couldn't locate invariant: %s" inv; in + let validate_loop_transition_invariant (loop_transition_invariant: YamlWitnessType.InvariantSet.LoopTransitionInvariant.t) = + let loc = loc_of_location loop_transition_invariant.location in + let inv = loop_transition_invariant.value in + + match Locator.find_opt loop_locator loc with + | Some lvars -> + validate_lvars_transition_invariant ~loc ~lvars inv + | None -> + incr cnt_error; + M.warn ~category:Witness ~loc:(CilLocation loc) "couldn't locate invariant: %s" inv; + in + let validate_invariant (invariant: YamlWitnessType.InvariantSet.Invariant.t) = let target_type = YamlWitnessType.InvariantSet.InvariantType.invariant_type invariant.invariant_type in match invariant_type_enabled target_type, invariant.invariant_type with @@ -651,7 +714,9 @@ struct validate_location_invariant x | true, LoopInvariant ({labels = (None | Some []); _} as x) -> validate_loop_invariant x - | false, (LocationInvariant _ | LoopInvariant _) -> + | true, LoopTransitionInvariant ({labels = (None | Some []); _} as x) -> + validate_loop_transition_invariant x + | false, (LocationInvariant _ | LoopInvariant _ | LoopTransitionInvariant _) -> incr cnt_disabled; M.info_noloc ~category:Witness "disabled invariant of type %s" target_type | _ -> diff --git a/tests/regression/56-witness/80-terminating-program-example.t b/tests/regression/56-witness/80-terminating-program-example.t index 5517367f6a..b233906952 100644 --- a/tests/regression/56-witness/80-terminating-program-example.t +++ b/tests/regression/56-witness/80-terminating-program-example.t @@ -81,14 +81,14 @@ [Success][Witness] invariant confirmed: i <= 5 (80-terminating-program-example.c:15:5) [Success][Witness] invariant confirmed: j <= 3 (80-terminating-program-example.c:15:5) [Success][Witness] invariant confirmed: (long long )j + (long long )i == 6LL (80-terminating-program-example.c:15:5) - [Warning][Witness] cannot validate invariant of type loop_transition_invariant + [Success][Witness] invariant confirmed: (long long )\at(i, AnyPrev) >= (long long )i + 1LL (80-terminating-program-example.c:15:5) [Info][Witness] witness validation summary: - confirmed: 5 + confirmed: 6 unconfirmed: 0 refuted: 0 error: 0 unchecked: 0 - unsupported: 1 + unsupported: 0 disabled: 0 total validation entries: 6 @@ -98,13 +98,13 @@ live: 7 dead: 0 total lines: 7 - [Warning][Witness] cannot validate invariant of type loop_transition_invariant + [Success][Witness] invariant confirmed: \at(i, AnyPrev) > i (80-terminating-program-example.c:15:5) [Info][Witness] witness validation summary: - confirmed: 0 + confirmed: 1 unconfirmed: 0 refuted: 0 error: 0 unchecked: 0 - unsupported: 1 + unsupported: 0 disabled: 0 total validation entries: 1 diff --git a/tests/regression/78-termination/01-simple-loop-terminating.t b/tests/regression/78-termination/01-simple-loop-terminating.t index 4c09d90cd8..8f9562ae4d 100644 --- a/tests/regression/78-termination/01-simple-loop-terminating.t +++ b/tests/regression/78-termination/01-simple-loop-terminating.t @@ -42,3 +42,23 @@ function: main value: (long long )i >= (long long )\at(i, AnyPrev) + 1LL format: ext_c_expression + + + $ goblint --set ana.activated[+] termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra --set witness.yaml.validate witness.yml --set witness.yaml.invariant-types "['loop_invariant', 'loop_transition_invariant']" 01-simple-loop-terminating.c + [Warning] termination analysis implicitly activates threadflag analysis and set sem.int.signed_overflow to assume_none + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 6 + dead: 0 + total lines: 6 + [Success][Witness] invariant confirmed: 1U <= i (01-simple-loop-terminating.c:8:3) + [Success][Witness] invariant confirmed: i <= 11U (01-simple-loop-terminating.c:8:3) + [Success][Witness] invariant confirmed: (long long )i >= (long long )\at(i, AnyPrev) + 1LL (01-simple-loop-terminating.c:8:3) + [Info][Witness] witness validation summary: + confirmed: 3 + unconfirmed: 0 + refuted: 0 + error: 0 + unchecked: 0 + unsupported: 0 + disabled: 0 + total validation entries: 3