Prototype loop transition invariant generation

src/analyses/apron/relationAnalysis.apron.ml

@@ -265,6 +265,60 @@ struct
     if M.tracing then M.traceu "relation" "-> %a" D.pretty r;
     r
 
+  let query_invariant_transition man =
+    let st = man.local in
+    let ask = Analyses.ask_of_man man in
+    let r1 = RD.keep_filter st.rel (fun var ->
+        match RV.find_metadata var with
+        | Some (Local _) -> true
+        | _ -> false
+      )
+    in
+    Logs.debug "r1: %a" RD.pretty r1;
+    let r1vars = RD.vars r1 in
+    let r1vars' = List.map (fun var ->
+        match RV.find_metadata var with
+        | Some (Local x) -> RV.arg x
+        | _ -> assert false
+      ) r1vars
+    in
+    let r2 = RD.add_vars r1 r1vars' in
+    let r2' = RD.assign_var_parallel' r2 r1vars' r1vars in
+    let r3 = RD.keep_vars r2' r1vars' in
+    Logs.debug "r3: %a" RD.pretty r3;
+    (* let r3' = RD.assr3 in *)
+    (* Logs.debug "r3': %a" RD.pretty r3'; *)
+    let r4 = RD.unify r1 r3 in
+    let r5 =
+      List.fold_left (fun acc var ->
+          match RV.to_cil_varinfo var with
+          | Some vi when TerminationPreprocessing.VarToStmt.mem vi !LoopTermination.loop_counters ->
+            let open Apron in
+            let env = RD.env acc in
+            (* let tcons1 = Tcons1.make Texpr1.(binop Sub (var env (RV.local vi)) (var env (RV.arg vi)) Int Zero) Lincons1.SUP in (* with AnyPrev *) *)
+            let tcons1 = Tcons1.make Texpr1.(binop Sub (binop Sub (var env (RV.local vi)) (var env (RV.arg vi)) Int Zero) (cst env (Coeff.s_of_int 1)) Int Zero) Lincons1.EQ in (* with LastPrev *)
+            let acc' = RD.meet_tcons ask acc tcons1 MyCFG.unknown_exp (lazy false) in
+            RD.remove_vars acc' [RV.local vi; RV.arg vi]
+          | _ ->
+            acc
+        ) r4 r1vars
+    in
+    Logs.debug "r5: %a" RD.pretty r5;
+    let scope = Node.find_fundec man.node in
+    let e_inv = Fun.id in (* TODO: handle globals? *)
+    let inv =
+      RD.invariant r5
+      |> List.to_seq
+      |> Seq.filter_map (fun (lincons1: Apron.Lincons1.t) ->
+          RD.cil_exp_of_lincons1 lincons1
+          |> Option.map e_inv
+          |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp) && InvariantCil.exp_is_in_scope scope exp)
+        )
+      |> 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
@@ -649,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/cdomains/apron/affineEqualityDenseDomain.apron.ml

@@ -526,7 +526,7 @@ struct
       In case of a potential overflow, "no_ov" is set to false
       and Convert.tcons1_of_cil_exp will raise the exception Unsupported_CilExp Overflow *)
 
-  let meet_tcons ask t tcons expr =
+  let meet_tcons ask t tcons expr _ =
     let check_const cmp c = if cmp c Mpqf.zero then bot_env else t in
     let meet_vec e =
       (* Flip the sign of the const. val in coeff vec *)
@@ -575,7 +575,7 @@ struct
   let assert_constraint ask d e negate no_ov =
     if M.tracing then M.tracel "assert_constraint" "assert_constraint with expr: %a %b" d_exp e (Lazy.force no_ov);
     match Convert.tcons1_of_cil_exp ask d d.env e negate no_ov with
-    | tcons1 -> meet_tcons ask d tcons1 e
+    | tcons1 -> meet_tcons ask d tcons1 e ()
     | exception Convert.Unsupported_CilExp _ -> d
 
   let assert_constraint ask d e negate no_ov = timing_wrap "assert_constraint" (assert_constraint ask d e negate) no_ov

src/cdomains/apron/affineEqualityDomain.apron.ml

@@ -477,7 +477,7 @@ struct
       In case of a potential overflow, "no_ov" is set to false
       and Convert.tcons1_of_cil_exp will raise the exception Unsupported_CilExp Overflow *)
 
-  let meet_tcons ask t tcons expr =
+  let meet_tcons ask t tcons expr _ =
     let check_const cmp c = if cmp c Mpqf.zero then bot_env else t in
     let meet_vec e =
       (* Flip the sign of the const. val in coeff vec *)
@@ -526,7 +526,7 @@ struct
   let assert_constraint ask d e negate no_ov =
     if M.tracing then M.tracel "assert_constraint" "assert_constraint with expr: %a %b" d_exp e (Lazy.force no_ov);
     match Convert.tcons1_of_cil_exp ask d d.env e negate no_ov with
-    | tcons1 -> meet_tcons ask d tcons1 e
+    | tcons1 -> meet_tcons ask d tcons1 e ()
     | exception Convert.Unsupported_CilExp _ -> d
 
   let assert_constraint ask d e negate no_ov = timing_wrap "assert_constraint" (assert_constraint ask d e negate) no_ov

src/cdomains/apron/apronDomain.apron.ml

@@ -212,7 +212,7 @@ sig
   val mem_var : t -> Var.t -> bool
   val assign_var_parallel' :
     t -> Var.t list -> Var.t list -> t
-  val meet_tcons : Queries.ask -> t -> Tcons1.t -> exp -> t
+  val meet_tcons : Queries.ask -> t -> Tcons1.t -> exp -> bool Lazy.t -> t
   val to_lincons_array : t -> Lincons1.earray
   val of_lincons_array : Lincons1.earray -> t
 
@@ -391,7 +391,7 @@ struct
     let texpr1 = Texpr1.of_expr (A.env nd) (Var v') in
     A.substitute_texpr_with Man.mgr nd v texpr1 None
 
-  let meet_tcons _ d tcons1 e =
+  let meet_tcons _ d tcons1 e _ =
     let earray = Tcons1.array_make (A.env d) 1 in
     Tcons1.array_set earray 0 tcons1;
     A.meet_tcons_array Man.mgr d earray
@@ -536,7 +536,7 @@ struct
           if M.tracing then M.trace "apron" "assert_constraint %a %a" d_exp e Tcons1.pretty tcons1;
           if M.tracing then M.trace "apron" "assert_constraint st: %a" D.pretty d;
           if M.tracing then M.trace "apron" "assert_constraint tcons1: %a" Tcons1.pretty tcons1;
-          let r = meet_tcons ask d tcons1 e in
+          let r = meet_tcons ask d tcons1 e () in
           if M.tracing then M.trace "apron" "assert_constraint r: %a" D.pretty r;
           r
         | exception Convert.Unsupported_CilExp reason ->
@@ -918,7 +918,8 @@ struct
   let substitute_var_with (b, d) v1 v2 =
     BoxD.substitute_var_with b v1 v2;
     D.substitute_var_with d v1 v2
-  let meet_tcons ask (b, d) c e = (BoxD.meet_tcons ask b c e, D.meet_tcons ask d c e)
+  let env (b, d) = BoxD.env b
+  let meet_tcons ask (b, d) c e q = (BoxD.meet_tcons ask b c e q, D.meet_tcons ask d c e q)
   let to_lincons_array (_, d) = D.to_lincons_array d
   let of_lincons_array a = (BoxD.of_lincons_array a, D.of_lincons_array a)
 

src/cdomains/apron/relationDomain.apron.ml

@@ -128,6 +128,8 @@ sig
   val marshal: t -> marshal
   val unmarshal: marshal -> t
   val mem_var: t -> var -> bool
+  val env: t -> Environment.t
+  val meet_tcons: Queries.ask -> t -> Tcons1.t -> exp -> bool Lazy.t -> t
   val assert_inv : Queries.ask -> t -> exp -> bool -> bool Lazy.t -> t
   val eval_int : Queries.ask -> t -> exp -> bool Lazy.t -> Queries.ID.t
 end

src/cdomains/apron/sharedFunctions.apron.ml

@@ -210,12 +210,12 @@ struct
       texpr1_expr_of_cil_exp exp
     in
     let exp = Cil.constFold false exp in
-    if M.tracing then 
+    if M.tracing then
       match conv exp with
-      | exception Unsupported_CilExp ex -> 
+      | exception Unsupported_CilExp ex ->
         M.tracel "rel-texpr-cil-conv" "unsuccessfull: %s" (show_unsupported_cilExp ex);
         raise (Unsupported_CilExp ex)
-      | res -> 
+      | res ->
         M.trace "relation" "texpr1_expr_of_cil_exp: %a -> %a (%b)" d_plainexp exp Texpr1.Expr.pretty res (Lazy.force no_ov);
         M.tracel "rel-texpr-cil-conv" "successfull: Good";
         res
@@ -296,6 +296,14 @@ struct
   let cil_exp_of_linexpr1_term ~scalewith (c: Coeff.t) v =
     match V.to_cil_varinfo v with
     | Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[]))   ->
+      let vinfo =
+        match V.find_metadata v with
+        | Some (Arg v') ->
+          (* {v' with vname = ("\\at(" ^ v'.vname ^ ", AnyPrev)")} (* with i - i' > 0*) *)
+          {v' with vname = ("\\at(" ^ v'.vname ^ ", LastPrev)")} (* with i - i' - 1 = 0 *)
+        | _ ->
+          vinfo
+      in
       let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
       let flip, coeff = coeff_to_const ~scalewith c in
       let prod = BinOp(Mult, coeff, var, longlong) in
@@ -461,7 +469,7 @@ struct
   let add_vars t vars = Vector.timing_wrap "add_vars" (add_vars t) vars
 
   let remove_vars t vars =
-    let t = copy t in 
+    let t = copy t in
     let env' = Environment.remove_vars t.env vars in
     dimchange2_remove t env'
 
@@ -514,6 +522,7 @@ sig
 
   val env: t -> Environment.t
 
+  val meet_tcons: Queries.ask -> t -> Tcons1.t -> exp -> bool Lazy.t -> t
   val assert_constraint: Queries.ask -> t -> exp -> bool -> bool Lazy.t -> t
   val eval_interval : Queries.ask -> t -> Texpr1.t -> Z.t option * Z.t option
 end

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 (