Merge branch 'fix/virgile/loop_assigns_status' into 'master'

status of loop assigns in presence of multiple emitter

See merge request frama-c/frama-c!2725

.Makefile.lint

@@ -52,7 +52,6 @@ ML_LINT_KO+=src/kernel_services/analysis/dataflow2.mli
 ML_LINT_KO+=src/kernel_services/analysis/dataflows.ml
 ML_LINT_KO+=src/kernel_services/analysis/dataflows.mli
 ML_LINT_KO+=src/kernel_services/analysis/dominators.ml
-ML_LINT_KO+=src/kernel_services/analysis/exn_flow.ml
 ML_LINT_KO+=src/kernel_services/analysis/interpreted_automata.ml
 ML_LINT_KO+=src/kernel_services/analysis/interpreted_automata.mli
 ML_LINT_KO+=src/kernel_services/analysis/logic_interp.ml

src/kernel_internals/typing/allocates.ml

@@ -35,7 +35,7 @@ let add_allocates_loop stmt =
   let all_default = Annotations.fold_code_annot all_default stmt true in
   if all_default then
     let ca = AAllocation ([], FreeAlloc ([], [])) in
-    Annotations.add_code_annot Emitter.kernel stmt
+    Annotations.add_code_annot ~keep_empty:false Emitter.kernel stmt
       (Logic_const.new_code_annotation ca)
 
 let add_allocates_nothing_funspec kf =

src/kernel_internals/typing/asm_contracts.ml

@@ -184,7 +184,7 @@ class visit_assembly =
            let ca =
              Logic_const.new_code_annotation (AStmtSpec ([],spec))
            in
-           Annotations.add_code_annot emitter ~kf stmt ca;
+           Annotations.add_code_annot ~keep_empty:false emitter ~kf stmt ca;
            if not mem_clobbered && Kernel.AsmContractsAutoValidate.get()
            then begin
              let active = [] in

src/kernel_services/ast_data/annotations.mli

@@ -261,6 +261,7 @@ val fold_decreases:
 (**************************************************************************)
 
 val add_code_annot:
+  ?keep_empty:bool ->
   Emitter.t -> ?kf:kernel_function -> stmt -> code_annotation -> unit
 (** Add a new code annotation attached to the given statement. If [kf] is
     provided, the function runs faster.
@@ -270,9 +271,16 @@ val add_code_annot:
     Trying to associate more than one will result in a merge of the contracts.
 
     The same things happens with loop assigns and allocates/frees.
+    The [keep_empty] argument is only used for loop assigns
+    and loop allocates, where it is used to decide whether to add the given
+    code annot in case the corresponding category was empty. It defaults to
+    [true], which is sound wrt ACSL semantics of equating an absence of
+    annotation with assigns/allocates \everything.
 
     There can be at most one loop variant registered per statement.
     Attempting to register a second one will result in a fatal error.
+
+    @modify Frama-C+dev: add keep_empty argument
  *)
 
 val add_assert:

src/kernel_services/ast_queries/file.ml

@@ -701,7 +701,7 @@ let emit_all_statuses _ =
 let () = Ast.apply_after_computed emit_all_statuses
 
 let add_annotation kf st a =
-  Annotations.add_code_annot Emitter.end_user ~kf st a;
+  Annotations.add_code_annot ~keep_empty:false Emitter.end_user ~kf st a;
   (* Now check if the annotation is valid by construction
      (provided normalization is correct). *)
   match a.annot_content with
@@ -741,7 +741,7 @@ let synchronize_source_annot has_new_stmt kf =
                       st_ann.skind <- (Block (Cil.mkBlockNonScoping [st]));
                       has_new_stmt := true;
                       Annotations.add_code_annot
-                        Emitter.end_user ~kf st_ann annot;
+                        ~keep_empty:false Emitter.end_user ~kf st_ann annot;
                       (true, st_ann)
                     end else begin
                       add_annotation kf st annot;

src/kernel_services/ast_queries/logic_utils.ml

@@ -676,6 +676,18 @@ let rec add_attribute_glob_annot a g =
   | Dcustom_annot(c,n,al,l) -> Dcustom_annot(c,n,Cil.addAttribute a al, l)
   | Dextended (e,al,l) -> Dextended(e,Cil.addAttribute a al,l)
 
+let behavior_has_only_assigns bhvs =
+  bhvs.b_requires = [] && bhvs.b_assumes = [] &&
+  bhvs.b_post_cond = [] && bhvs.b_allocation = FreeAllocAny &&
+  bhvs.b_extended = []
+
+let funspec_has_only_assigns spec =
+  List.for_all behavior_has_only_assigns spec.spec_behavior &&
+  spec.spec_variant = None &&
+  spec.spec_terminates = None &&
+  spec.spec_complete_behaviors = [] &&
+  spec.spec_disjoint_behaviors = []
+
 let is_same_list f l1 l2 =
   try List.for_all2 f l1 l2 with Invalid_argument _ -> false
 

src/kernel_services/ast_queries/logic_utils.mli

@@ -312,6 +312,18 @@ val is_annot_next_stmt: code_annotation -> bool
 val add_attribute_glob_annot:
   attribute -> global_annotation -> global_annotation
 
+(** {2 Contracts } *)
+
+(** [true] if the behavior has only an assigns clause.
+    @since Frama-C+dev
+*)
+val behavior_has_only_assigns: behavior -> bool
+
+(** [true] if the only non-empty fields of the contract are assigns clauses
+    @since Frama-C+dev
+*)
+val funspec_has_only_assigns: funspec -> bool
+
 (** {2 Structural equality between annotations} *)
 
 val is_same_list: ('a -> 'a -> bool) -> 'a list -> 'a list -> bool

src/kernel_services/ast_transformations/inline.ml

@@ -123,7 +123,7 @@ let inline_call loc caller callee return args =
              fd.sbody.bstmts <- inits @ fd.sbody.bstmts;
            end else begin
              (* put a statement contract on top of the function's body,
-                but only after we have assigned the formals. Not that there
+                but only after we have assigned the formals. Note that there
                 is no need to rename behaviors: they will only shadow behaviors
                 of the caller within callee's body, just as we need.
              *)

src/kernel_services/visitors/visitor.ml

@@ -124,7 +124,8 @@ object(self)
                remove;
              List.iter
                (fun (e, a) ->
-                  Annotations.add_code_annot e ~kf:new_kf stmt a)
+                  Annotations.add_code_annot
+                    ~keep_empty:false e ~kf:new_kf stmt a)
                add)
           self#get_filling_actions
       end

src/plugins/aorai/aorai_visitors.ml

@@ -272,7 +272,10 @@ let update_loop_assigns kf stmt state vi code_annot =
         (AAssigns (bhvs, Logic_utils.concat_assigns old_assigns assigns))
     | _ -> Aorai_option.fatal "Expecting an assigns clause here"
   in
-  Annotations.add_code_annot Aorai_option.emitter ~kf stmt new_assigns
+  (* we're putting the annotation on a new statement, with an empty
+     loop assigns by construction. Don't keep_empty *)
+  Annotations.add_code_annot
+    ~keep_empty:false Aorai_option.emitter ~kf stmt new_assigns
 
 let get_action_post_cond kf ?init_trans return_states =
   let to_consider pre_state int_states =

src/plugins/aorai/tests/aorai/oracle/assigns.0.res.oracle

@@ -275,8 +275,8 @@ int main(void)
   /*@ ghost main_pre_func(); */
   /*@ assigns X; */
   X ++;
-  /*@ assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
-              in_main, X;
+  /*@ assigns X, aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+              in_main;
   */
   f();
   /*@ ghost main_post_func(X); */

src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle

@@ -213,7 +213,7 @@ int main(void)
   /*@ ghost main_pre_func(); */
   /*@ assigns X; */
   X ++;
-  /*@ assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, X; */
+  /*@ assigns X, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates; */
   f();
   /*@ ghost main_post_func(X); */
   return X;

src/plugins/e-acsl/src/code_generator/label.ml

@@ -48,7 +48,7 @@ let move kf ~old new_stmt =
     List.iter
       (fun (e, ca) ->
          Annotations.remove_code_annot ~kf e old ca;
-         Annotations.add_code_annot ~kf e new_stmt ca)
+         Annotations.add_code_annot ~keep_empty:false ~kf e new_stmt ca)
       l;
     (* update the gotos of the function jumping to one of the labels *)
     let f =

tests/spec/loop_assigns_generated.i

@@ -7,4 +7,6 @@ void f() {
   int i = 0;
   /*@ loop assigns i; */
   while (i< 10) { i++; }
+
+  while (i>0) { i--; }
 }

tests/spec/loop_assigns_generated.ml

@@ -3,7 +3,7 @@ open Cil_types
 let e1 = Emitter.(create "emitter1" [ Code_annot ] [] [])
 let e2 = Emitter.(create "emitter2" [ Code_annot ] [] [])
 
-let add_assigns e kf stmt v =
+let mk_assigns e v =
   let lv = Cil.cvar_to_lvar v in
   let term_v  = Logic_const.tvar lv in
   let named_term_v =
@@ -11,12 +11,15 @@ let add_assigns e kf stmt v =
       term_name = ("added_by_"^(Emitter.get_name e))::term_v.term_name }
   in
   let id_v = Logic_const.new_identified_term named_term_v  in
-  Annotations.add_code_annot e ~kf stmt
+  Writes[id_v,FromAny]
+
+let add_assigns ?(keep_empty=false) e kf stmt v =
+  Annotations.add_code_annot ~keep_empty e ~kf stmt
     (Logic_const.new_code_annotation
-       (AAssigns ([], Writes [id_v, FromAny])));
+       (AAssigns ([], mk_assigns e v)));
   Filecheck.check_ast ("after insertion of loop assigns " ^ v.vname)
 
-let add_allocates e kf stmt v =
+let mk_allocates e v =
   let lv = Cil.cvar_to_lvar v in
   let term_v = Logic_const.tvar lv in
   let named_term_v =
@@ -24,11 +27,23 @@ let add_allocates e kf stmt v =
       term_name = ("added_by_"^(Emitter.get_name e))::term_v.term_name }
   in
   let id_v = Logic_const.new_identified_term named_term_v in
-  Annotations.add_code_annot e ~kf stmt
-    (Logic_const.new_code_annotation
-       (AAllocation([],FreeAlloc ([],[id_v]))));
+  FreeAlloc ([],[id_v])
+
+let add_allocates ?(keep_empty=false) e kf stmt v =
+  Annotations.add_code_annot ~keep_empty e ~kf stmt
+    (Logic_const.new_code_annotation (AAllocation([],mk_allocates e v)));
   Filecheck.check_ast ("after insertion of loop allocates " ^ v.vname )
 
+let check_only_one f =
+  let seen = ref false in
+  fun _ a ->
+    if f a then begin
+      assert (not !seen);
+      seen := true
+    end
+
+let filter_category f _ a acc = if f a then a :: acc else acc
+
 let main () =
   Ast.compute();
   let kf = Globals.Functions.find_by_name "f" in
@@ -37,14 +52,44 @@ let main () =
     List.find
       (fun s -> match s.skind with Loop _ -> true | _ -> false) def.sallstmts
   in
+  let s2 =
+    List.find
+      (fun s' -> s!=s' && (match s'.skind with Loop _ -> true | _ -> false))
+      def.sallstmts
+  in
+  let s3 = Kernel_function.find_return kf in
   let j = Cil.makeLocalVar def ~insert:true "j" Cil.intType in
   let k = Cil.makeLocalVar def ~insert:true "k" Cil.intType in
+  let l = Cil.makeLocalVar def ~insert:true "l" Cil.intType in
   let p = Cil.makeLocalVar def ~insert:true "p" Cil.intPtrType in
   let q = Cil.makeLocalVar def ~insert:true "q" Cil.intPtrType in
+  let r = Cil.makeLocalVar def ~insert:true "r" Cil.intPtrType in
   add_assigns e1 kf s j;
   add_assigns e2 kf s k;
+  add_assigns e1 kf s l;
+  add_assigns ~keep_empty:true e2 kf s2 j;
+  Annotations.add_assigns ~keep_empty:true e1 kf ~stmt:s3 (mk_assigns e1 k);
   add_allocates e1 kf s p;
   add_allocates e2 kf s q;
+  add_allocates e1 kf s r;
+  add_allocates ~keep_empty:true e2 kf s2 p;
+  Annotations.add_allocates ~keep_empty:true e1 kf ~stmt:s3 (mk_allocates e1 k);
+  Annotations.iter_code_annot (check_only_one Logic_utils.is_assigns) s;
+  Annotations.iter_code_annot (check_only_one Logic_utils.is_allocation) s;
+  let lassigns =
+    Annotations.fold_code_annot (filter_category Logic_utils.is_assigns) s []
+  in
+  assert (List.length lassigns = 1);
+  let lalloc =
+    Annotations.fold_code_annot (filter_category Logic_utils.is_allocation) s []
+  in
+  assert (List.length lalloc = 1);
+  ignore
+    (Property_status.get
+       (Property.ip_of_code_annot_single kf s (List.hd lassigns)));
+  ignore
+    (Property_status.get
+       (Property.ip_of_code_annot_single kf s (List.hd lalloc)));
   File.pretty_ast ()
 
 let () = Db.Main.extend main

tests/spec/oracle/assigns_array.res.oracle

@@ -36,8 +36,8 @@ int h(int reset, int n)
   int i;
   int r = 0;
   i = 0;
-  /*@ for bar: loop assigns \nothing;
-      for foo: loop assigns Tab[0 .. i]; */
+  /*@ for foo: loop assigns Tab[0 .. i];
+      for bar: loop assigns \nothing; */
   while (i < n) {
     r += Tab[i];
     if (reset) Tab[i] = 0;

tests/spec/oracle/bts0578.res.oracle

@@ -7,11 +7,11 @@ void main(void)
   int i;
   int t[10];
   i = 0;
-  /*@ loop invariant \true;
-      loop assigns t[0 .. i];
+  /*@ loop assigns t[0 .. i];
+      loop invariant \true;
+      for foo: loop assigns t[0 .. i];
       for foo: loop invariant \true;
       for foo: loop invariant \true;
-      for foo: loop assigns t[0 .. i];
       loop variant 0;
   */
   while (i < 10) {

tests/spec/oracle/loop_assigns_generated.res.oracle

@@ -2,15 +2,20 @@
 /* Generated by Frama-C */
 void f(void)
 {
+  int *r;
   int *q;
   int *p;
+  int l;
   int k;
   int j;
   int i = 0;
-  /*@ loop allocates (added_by_emitter1: p), (added_by_emitter2: q);
-      loop assigns i, (added_by_emitter1: j), (added_by_emitter2: k);
+  /*@ loop assigns i, (added_by_emitter1: j), (added_by_emitter1: l),
+                   (added_by_emitter2: k);
+      loop allocates
+      (added_by_emitter1: p), (added_by_emitter1: r), (added_by_emitter2: q);
   */
   while (i < 10) i ++;
+  while (i > 0) i --;
   return;
 }