Output loop_transition_invariant-s to YAML witnesses

Author: sim642

src/analyses/apron/relationAnalysis.apron.ml

@@ -317,12 +317,11 @@ struct
       |> Seq.fold_left (fun acc x -> Invariant.(acc && of_exp x)) Invariant.none
     in
     Logs.debug "inv: %a" Invariant.pretty inv;
-    ()
+    inv
 
   let branch man e b =
     let st = man.local in
     let ask = Analyses.ask_of_man man in
-    query_invariant_transition man;
     let res = assign_from_globals_wrapper ask man.global st e (fun rel' e' ->
         (* not an assign, but must remove g#in-s still *)
         RD.assert_inv ask rel' e' (not b) (no_overflow ask e)
@@ -704,6 +703,7 @@ struct
       let vf' x = vf (Obj.repr x) in
       Priv.iter_sys_vars man.global vq vf'
     | Queries.Invariant context -> query_invariant man context
+    | Queries.InvariantTransition _context -> query_invariant_transition man
     | Queries.InvariantGlobal g ->
       let g: V.t = Obj.obj g in
       query_invariant_global man g

src/config/options.schema.json

@@ -2824,7 +2824,8 @@
                 "type": "string",
                 "enum": [
                   "location_invariant",
-                  "loop_invariant"
+                  "loop_invariant",
+                  "loop_transition_invariant"
                 ]
               },
               "default": [

src/domains/queries.ml

@@ -131,6 +131,7 @@ type _ t =
   | MustProtectedVars: mustprotectedvars -> VS.t t
   | MustProtectingLocks: mustprotectinglocks -> LockDomain.MustLockset.t t
   | Invariant: invariant_context -> Invariant.t t
+  | InvariantTransition: invariant_context -> Invariant.t t
   | InvariantGlobal: Obj.t -> Invariant.t t (** Argument must be of corresponding [Spec.V.t]. *)
   | WarnGlobal: Obj.t -> Unit.t t (** Argument must be of corresponding [Spec.V.t]. *)
   | IterSysVars: VarQuery.t * Obj.t VarQuery.f -> Unit.t t (** [iter_vars] for [Constraints.FromSpec]. [Obj.t] represents [Spec.V.t]. *)
@@ -206,6 +207,7 @@ struct
     | MustProtectedVars _ -> (module VS)
     | MustProtectingLocks _ -> (module LockDomain.MustLockset)
     | Invariant _ -> (module Invariant)
+    | InvariantTransition _ -> (module Invariant)
     | InvariantGlobal _ -> (module Invariant)
     | WarnGlobal _ -> (module Unit)
     | IterSysVars _ -> (module Unit)
@@ -280,6 +282,7 @@ struct
     | MustProtectedVars _ -> VS.top ()
     | MustProtectingLocks _ -> LockDomain.MustLockset.top ()
     | Invariant _ -> Invariant.top ()
+    | InvariantTransition _ -> Invariant.top ()
     | InvariantGlobal _ -> Invariant.top ()
     | WarnGlobal _ -> Unit.top ()
     | IterSysVars _ -> Unit.top ()
@@ -366,6 +369,7 @@ struct
     | Any (MustProtectingLocks _) -> 61
     | Any (GhostVarAvailable _) -> 62
     | Any InvariantGlobalNodes -> 63
+    | Any (InvariantTransition _) -> 64
 
   let rec compare a b =
     let r = Stdlib.compare (order a) (order b) in
@@ -413,6 +417,7 @@ struct
       | Any (EvalJumpBuf e1), Any (EvalJumpBuf e2) -> CilType.Exp.compare e1 e2
       | Any (WarnGlobal vi1), Any (WarnGlobal vi2) -> Stdlib.compare (Hashtbl.hash vi1) (Hashtbl.hash vi2)
       | Any (Invariant i1), Any (Invariant i2) -> compare_invariant_context i1 i2
+      | Any (InvariantTransition i1), Any (InvariantTransition i2) -> compare_invariant_context i1 i2
       | Any (InvariantGlobal vi1), Any (InvariantGlobal vi2) -> Stdlib.compare (Hashtbl.hash vi1) (Hashtbl.hash vi2)
       | Any (YamlEntryGlobal (vi1, task1)), Any (YamlEntryGlobal (vi2, task2)) -> Stdlib.compare (Hashtbl.hash vi1) (Hashtbl.hash vi2) (* TODO: compare task *)
       | Any (IterSysVars (vq1, vf1)), Any (IterSysVars (vq2, vf2)) -> VarQuery.compare vq1 vq2 (* not comparing fs *)
@@ -461,6 +466,7 @@ struct
     | Any (EvalJumpBuf e) -> CilType.Exp.hash e
     | Any (WarnGlobal vi) -> Hashtbl.hash vi
     | Any (Invariant i) -> hash_invariant_context i
+    | Any (InvariantTransition i) -> hash_invariant_context i
     | Any (MutexType m) -> Mval.Unit.hash m
     | Any (InvariantGlobal vi) -> Hashtbl.hash vi
     | Any (YamlEntryGlobal (vi, task)) -> Hashtbl.hash vi (* TODO: hash task *)
@@ -522,6 +528,7 @@ struct
     | Any (MustProtectedVars m) -> Pretty.dprintf "MustProtectedVars _"
     | Any (MustProtectingLocks g) -> Pretty.dprintf "MustProtectingLocks _"
     | Any (Invariant i) -> Pretty.dprintf "Invariant _"
+    | Any (InvariantTransition i) -> Pretty.dprintf "InvariantTransition _"
     | Any (WarnGlobal vi) -> Pretty.dprintf "WarnGlobal _"
     | Any (IterSysVars _) -> Pretty.dprintf "IterSysVars _"
     | Any (InvariantGlobal i) -> Pretty.dprintf "InvariantGlobal _"

src/witness/yamlWitness.ml

@@ -118,6 +118,16 @@ struct
         };
     }
 
+  let loop_transition_invariant' ~location ~(invariant): InvariantSet.InvariantKind.t =
+    Invariant {
+      invariant_type = LoopTransitionInvariant {
+          location;
+          value = invariant;
+          format = "ext_c_expression";
+          labels = None;
+        };
+    }
+
   let invariant_set ~task ~(invariants): Entry.t = {
     entry_type = InvariantSet {
         content = invariants;
@@ -572,6 +582,40 @@ struct
             invariants
         in
 
+        (* Generate loop transition invariants *)
+        let invariants =
+          if entry_type_enabled YamlWitnessType.InvariantSet.entry_type && invariant_type_enabled YamlWitnessType.InvariantSet.LoopTransitionInvariant.invariant_type then (
+            LH.fold (fun loc ns acc ->
+                if WitnessInvariant.emit_loop_head then ( (* TODO: remove double condition? *)
+                  let inv = List.fold_left (fun acc n ->
+                      let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in
+                      Invariant.(acc || R.ask_local_node n ~local (InvariantTransition Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
+                    ) (Invariant.bot ()) ns
+                  in
+                  match inv with
+                  | `Lifted inv ->
+                    let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *)
+                    let location_function = fundec.svar.vname in
+                    let location = Entry.location ~location:loc ~location_function in
+                    (* let invs = WitnessUtil.InvariantExp.process_exp inv in *)
+                    let invs = [inv] in (* TODO: not processing because original_name replacement removes \at names *)
+                    List.fold_left (fun acc inv ->
+                        let invariant = CilType.Exp.show inv in
+                        let invariant = Entry.loop_transition_invariant' ~location ~invariant in
+                        incr cnt_loop_invariant; (* TODO: separate counter? *)
+                        invariant :: acc
+                      ) acc invs
+                  | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
+                    acc
+                )
+                else
+                  acc
+              ) (Lazy.force loop_nodes) invariants
+          )
+          else
+            invariants
+        in
+
         (* Generate flow-insensitive invariants as location invariants *)
         let invariants =
           if entry_type_enabled YamlWitnessType.FlowInsensitiveInvariant.entry_type && GobConfig.get_string "witness.invariant.flow_insensitive-as" = "invariant_set-location_invariant" then (