Prototype loop transition invariant validation

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'

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 =

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)

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" []]);

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

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,14 +695,28 @@ 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
           | true, LocationInvariant ({labels = (None | Some []); _} as x) ->
             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
           | _ ->

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

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