Merge pull request kind2-mc#1042 from daniel-larraz/safe-calls-rev

Always instantiate checks on assumptions of called nodes

src/lustre/lustreTransSys.ml

@@ -716,42 +716,45 @@ let call_terms_of_node_call mk_fresh_state_var globals
 
   in
 
-  (* Instantiate all properties of the called node in this node *)
+  (* Instantiate properties of the called node in this node *)
   let node_props =
-    if Flags.check_subproperties () && not (Flags.modular ()) then (
-      properties |> List.fold_left (
-        fun a ({ P.prop_name = n; P.prop_term = t; P.prop_kind } as p) ->
+    properties
+    |> List.filter (fun p ->
+      match P.get_prop_original_source p with
+      | P.Assumption _ -> true
+      | _ -> Flags.check_subproperties () && not (Flags.modular ())
+    )
+    |> List.fold_left (
+      fun a ({ P.prop_name = n; P.prop_term = t; P.prop_kind } as p) ->
 
-          (* Lift name of property *)
-          let prop_name =
-            lift_prop_name call_node_name call_pos n
-          in
+        (* Lift name of property *)
+        let prop_name =
+          lift_prop_name call_node_name call_pos n
+        in
 
-          (* Lift state variable of property
+        (* Lift state variable of property
 
-            Property is a local variable, thus it has been
-            instantiated and is in the map *)
-          let prop_term = lift_term state_var_map_up t in
+          Property is a local variable, thus it has been
+          instantiated and is in the map *)
+        let prop_term = lift_term state_var_map_up t in
 
-          (* Property is instantiated *)
-          let prop_source =
-            match p.P.prop_source with
-            | P.Candidate src -> P.Candidate src
-            | _ -> P.Instantiated (I.to_scope call_node_name, p)
-          in
+        (* Property is instantiated *)
+        let prop_source =
+          match p.P.prop_source with
+          | P.Candidate src -> P.Candidate src
+          | _ -> P.Instantiated (I.to_scope call_node_name, p)
+        in
 
-          (* Property status is unknown *)
-          let prop_status = P.PropUnknown in
+        (* Property status is unknown *)
+        let prop_status = P.PropUnknown in
 
-          (* Create and append property *)
-          { P.prop_name ;
-            P.prop_source ;
-            P.prop_term ;
-            P.prop_status ;
-            P.prop_kind ; } :: a
-      ) node_props
-    )
-    else node_props
+        (* Create and append property *)
+        { P.prop_name ;
+          P.prop_source ;
+          P.prop_term ;
+          P.prop_status ;
+          P.prop_kind ; } :: a
+    ) node_props
   in
 
   (* Instantiate assumptions from contracts in this node. *)

src/property.ml

@@ -302,7 +302,10 @@ let set_prop_unknown p =
 (* Get property status *)
 let get_prop_status { prop_status } = prop_status
 
-
+let rec get_prop_original_source { prop_source } =
+  match prop_source with
+  | Instantiated (_, p) -> get_prop_original_source p
+  | _ -> prop_source
 
 
 (* 

src/property.mli

@@ -1,6 +1,6 @@
 (* This file is part of the Kind 2 model checker.
 
-   Copyright (c) 2014 by the Board of Trustees of the University of Iowa
+   Copyright (c) 2014-2023 by the Board of Trustees of the University of Iowa
 
    Licensed under the Apache License, Version 2.0 (the "License"); you
    may not use this file except in compliance with the License.  You
@@ -126,6 +126,7 @@ val length_of_cex :  (StateVar.t * Model.value list) list -> int
 
 val get_prop_status : t -> prop_status
 
+val get_prop_original_source : t -> prop_source
 
 (* 
    Local Variables:

tests/lustre/contracts/assump-check.lus

@@ -0,0 +1,20 @@
+
+
+node imported C(x: int) returns (y:int);
+(*@contract
+  assume x>=0;
+  guarantee y>0;
+*)
+
+node B(x: int) returns (y: int);
+let
+  y = C(x);
+tel
+
+node A(x: int) returns (y: int);
+var l: int;
+let
+  l = if x>=0 then x else -x;
+  y = B(l);
+  check y>0;
+tel