Filter updates on properties that are not in the system

kind2-mc · Jun 5, 2024 · 1cbc4d1 · 1cbc4d1
1 parent 64dd5c6
commit 1cbc4d1
Show file tree

Hide file tree

Showing 3 changed files with 79 additions and 61 deletions.
diff --git a/src/kEvent.ml b/src/kEvent.ml
@@ -2227,82 +2227,97 @@ let update_trans_sys_sub input_sys analysis trans_sys events =
       update_trans_sys' trans_sys invars prop_status tl
 
     (* Property found true for k steps *)
-    | (m, PropStatus (p, (Property.PropKTrue k as s))) :: tl -> 
+    | (m, PropStatus (p, (Property.PropKTrue k as s))) :: tl -> (
 
-      (* Change property status in transition system *)
-      TransSys.set_prop_ktrue trans_sys k p;
+      try
+        (* Change property status in transition system *)
+        TransSys.set_prop_ktrue trans_sys k p;
 
-      (* Continue with propert status added to accumulator *)
-      update_trans_sys'
-        trans_sys
-        invars
-        ((m, (p, s)) :: prop_status) 
-        tl
+        (* Continue with property status added to accumulator *)
+        update_trans_sys'
+          trans_sys
+          invars
+          ((m, (p, s)) :: prop_status)
+          tl
 
+      with TransSys.PropertyNotFound _->
+        (* Continue without changes *)
+        update_trans_sys' trans_sys invars prop_status tl
+    )
     (* Property found invariant *)
-    | (m, PropStatus (p, (Property.PropInvariant cert as s))) :: tl -> 
+    | (m, PropStatus (p, (Property.PropInvariant cert as s))) :: tl -> (
 
-      (* Output proved property *)
-      log_proved m L_warn trans_sys None p;
+      try
+        (* Change property status (of all instances with name [p]) *)
+        TransSys.set_prop_invariant trans_sys p cert;
 
-      (* Change property status (of all instances with name [p]) *)
-      TransSys.set_prop_invariant trans_sys p cert;
+        (* Output proved property *)
+        log_proved m L_warn trans_sys None p;
 
-      let term =
-        TransSys.props_list_of_bound trans_sys Numeral.zero
-        |> List.assoc p
-      in
+        let term =
+          TransSys.props_list_of_bound trans_sys Numeral.zero
+          |> List.assoc p
+        in
 
-      (* Retrieve scope to add to invariants. *)
-      let scope = TransSys.scope_of_trans_sys trans_sys in
+        (* Retrieve scope to add to invariants. *)
+        let scope = TransSys.scope_of_trans_sys trans_sys in
 
-      let invars =
-        try (* Add proved property as invariant *)
-          TransSys.add_invariant trans_sys term cert false
-          |> insert_inv scope invars false
-        with Not_found -> (* Skip if named property not found *)
-          invars
-      in
+        let invars =
+          try (* Add proved property as invariant *)
+            TransSys.add_invariant trans_sys term cert false
+            |> insert_inv scope invars false
+          with Not_found -> (* Skip if named property not found *)
+            invars
+        in
 
-      let invars =
-        (* Get property by name *)
-        let prop = TransSys.property_of_name trans_sys p in
-        match prop.Property.prop_source with
-        | Property.Assumption (_, (_, pos)) -> (
-          (* If property is a contract assumption that a caller had to prove,
-             check whether the other assumptions have been proved invariant too.
-             If so, set SoFar(assumptions) invariant in transition system.
-          *)
-          match check_sofar_invariance trans_sys pos with
-          | Some inv -> insert_inv scope invars false inv
-          | None -> invars
-        )
-        | _ -> invars
-      in
+        let invars =
+          (* Get property by name *)
+          let prop = TransSys.property_of_name trans_sys p in
+          match prop.Property.prop_source with
+          | Property.Assumption (_, (_, pos)) -> (
+            (* If property is a contract assumption that a caller had to prove,
+              check whether the other assumptions have been proved invariant too.
+              If so, set SoFar(assumptions) invariant in transition system.
+            *)
+            match check_sofar_invariance trans_sys pos with
+            | Some inv -> insert_inv scope invars false inv
+            | None -> invars
+          )
+          | _ -> invars
+        in
 
-      (* Continue with property status added to accumulator *)
-      update_trans_sys'
-        trans_sys 
-        invars
-        ( (m, (p, s)) :: prop_status )
-        tl
+        (* Continue with property status added to accumulator *)
+        update_trans_sys'
+          trans_sys
+          invars
+          ( (m, (p, s)) :: prop_status )
+          tl
 
+      with TransSys.PropertyNotFound _->
+        (* Continue without changes *)
+        update_trans_sys' trans_sys invars prop_status tl
+    )
     (* Property found false *)
-    | (m, PropStatus (p, (Property.PropFalse cex as s))) :: tl -> 
+    | (m, PropStatus (p, (Property.PropFalse cex as s))) :: tl -> (
 
-      (* Output disproved property *)
-      log_cex true m L_warn input_sys analysis trans_sys p cex ;
+      try
+        (* Change property status in transition system *)
+        TransSys.set_prop_false trans_sys p cex;
 
-      (* Change property status in transition system *)
-      TransSys.set_prop_false trans_sys p cex;
+        (* Output disproved property *)
+        log_cex true m L_warn input_sys analysis trans_sys p cex ;
 
-      (* Continue with property status added to accumulator *)
-      update_trans_sys' 
-        trans_sys
-        invars
-        ((m, (p, s)) :: prop_status) 
-        tl
+        (* Continue with property status added to accumulator *)
+        update_trans_sys'
+          trans_sys
+          invars
+          ((m, (p, s)) :: prop_status)
+          tl
 
+      with TransSys.PropertyNotFound _->
+        (* Continue without changes *)
+        update_trans_sys' trans_sys invars prop_status tl
+    )
     (* Property found false *)
     | (m, StepCex (p, cex)) :: tl -> 
 

diff --git a/src/transSys.ml b/src/transSys.ml
@@ -22,6 +22,8 @@ module P = Property
 module SVM = StateVar.StateVarMap
 (* module SVS = StateVar.StateVarSet *)
 
+exception PropertyNotFound of string
+
 (* Offset of state variables in initial state constraint *)
 let init_base = Numeral.zero
 
@@ -1401,7 +1403,7 @@ let set_prop_status { properties } p s =
     ) false
   in
 
-  if not found then raise Not_found
+  if not found then raise (PropertyNotFound p)
 
 
 let set_prop_invariant trans_sys p cert = 
@@ -1425,7 +1427,7 @@ let set_prop_unknown { properties } p =
       | _ -> found
     ) false
   in
-  if not found then raise Not_found
+  if not found then raise (PropertyNotFound p)
 
 (* Return current status of all properties *)
 let get_prop_status_all_nocands t = 

diff --git a/src/transSys.mli b/src/transSys.mli
@@ -39,6 +39,7 @@
     @author Adrien Champion
 *)
 
+exception PropertyNotFound of string
 
 (* Dependencies: initial state predicate may occur in the transition
    relation in condacts, and if we support reset. *)