Merge branch 'feature/blanchard/ghost-pretty-printing' into 'master'

[AST Printing] Changes handling of ghost code

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

src/kernel_services/ast_printing/cil_printer.ml

@@ -454,6 +454,12 @@ let rec has_unprotected_local_init s =
   | Block { bscoping = false; bstmts = s :: _ } -> has_unprotected_local_init s
   | _ -> false
 
+(** Annotation context in which the Printer is *)
+type annot_ctxt =
+  | Not_in_annot     (** not in annotation *)
+  | In_simple_annot  (** in /*@ ... */ annotation *)
+  | In_nested_annot  (** in /@ ... @/ annotation *)
+
 class cil_printer () = object (self)
 
   val mutable logic_printer_enabled = true
@@ -462,13 +468,51 @@ class cil_printer () = object (self)
 
   method pp_keyword fmt s = pp_print_string fmt s
   method pp_acsl_keyword = self#pp_keyword
+
+  val mutable annot_ctxt = Not_in_annot
+
   method pp_open_annotation ?(block=true) ?(pre=format_of_string "/*@@") fmt =
+    let pre = match annot_ctxt with
+      | Not_in_annot -> annot_ctxt <- In_simple_annot ; pre
+      | In_simple_annot -> annot_ctxt <- In_nested_annot ; format_of_string "/@@"
+      | _ -> assert false (* cannot enter an annotation in a internal annotation *)
+    in
     (if block then Pretty_utils.pp_open_block else Format.fprintf)
       fmt "%(%)" pre
   method pp_close_annotation ?(block=true) ?(suf=format_of_string "*/") fmt =
+    let suf = match annot_ctxt with
+      | In_nested_annot -> annot_ctxt <- In_simple_annot ; format_of_string "@@/"
+      | In_simple_annot -> annot_ctxt <- Not_in_annot ; suf
+      | _ -> assert false (* we should not have to close an annotation that is not open *)
+    in
     (if block then Pretty_utils.pp_close_block else Format.fprintf)
       fmt "%(%)" suf
 
+  val mutable verbose = false
+  (* Do not add a value that depends on a
+     non-constant variable of the kernel here (e.g. [Kernel.Debug.get ()]). Due
+     to the way the pretty-printing class is instantiated, this value would be
+     evaluated too soon. Override the [reset] method instead. *)
+
+  (* indicates whether we are printing ghost elements *)
+  val mutable is_ghost = false
+  method private display_comment () = not is_ghost || verbose
+
+  method private in_ghost_if_needed fmt ghost_flag ~post_fmt ?block do_it =
+    let display_ghost = ghost_flag && not is_ghost in
+    if display_ghost then begin
+      is_ghost <- true ;
+      Format.fprintf fmt "%t %a@ "
+        (fun fmt -> self#pp_open_annotation ?block fmt)
+        self#pp_acsl_keyword "ghost"
+    end ;
+    do_it () ;
+    if display_ghost then begin
+      is_ghost <- false;
+      Format.fprintf fmt post_fmt
+        (fun fmt -> self#pp_close_annotation ?block fmt)
+    end
+
   method without_annot:
     'a. (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a -> unit =
     fun f fmt x ->
@@ -487,12 +531,6 @@ class cil_printer () = object (self)
       let finally () = force_brace <- tmp in
       Extlib.try_finally ~finally f fmt x;
 
-  val mutable verbose = false
-  (* Do not add a value that depends on a
-     non-constant variable of the kernel here (e.g. [Kernel.Debug.get ()]). Due
-     to the way the pretty-printing class is instantiated, this value would be
-     evaluated too soon. Override the [reset] method instead. *)
-
   val current_stmt = Stack.create ()
 
   val mutable current_function = None
@@ -1094,10 +1132,6 @@ class cil_printer () = object (self)
 
   method fundec fmt fd =  fprintf fmt "%a" self#varinfo fd.svar
 
-  (* number of opened ghost code *)
-  val mutable is_ghost = false
-  method private display_comment () = not is_ghost || verbose
-
   method annotated_stmt (next: stmt) fmt (s: stmt) =
     pp_open_hvbox fmt 0;
     self#stmt_labels fmt s;
@@ -1105,18 +1139,8 @@ class cil_printer () = object (self)
     if Cil.is_skip s.skind && not s.ghost && s.sattr = [] then begin
       if verbose || s.labels <> [] then fprintf fmt ";"
     end else begin
-      let was_ghost = is_ghost in
-      let display_ghost = s.ghost && not was_ghost in
-      if display_ghost then begin
-        is_ghost <- true;
-        Format.fprintf fmt "%t %a "
-          (fun fmt -> self#pp_open_annotation fmt) self#pp_acsl_keyword "ghost"
-      end;
-      self#stmtkind s.sattr next fmt s.skind ;
-      if display_ghost then begin
-        is_ghost <- false;
-        self#pp_close_annotation fmt
-      end
+      self#in_ghost_if_needed fmt s.ghost ~post_fmt:"%t"
+        (fun () -> self#stmtkind s.sattr next fmt s.skind)
     end;
     pp_close_box fmt ()
 
@@ -1190,18 +1214,10 @@ class cil_printer () = object (self)
     | _ -> false
 
   method private vdecl_complete fmt v =
-    let display_ghost = v.vghost && not is_ghost in
-    Format.fprintf fmt "@[<hov 0>%t%a;%t@]"
-      (if display_ghost then (fun fmt ->
-           Format.fprintf fmt "%t %a@ "
-             (fun fmt -> self#pp_open_annotation ~block:false fmt)
-             self#pp_acsl_keyword "ghost")
-       else ignore)
-      self#vdecl v
-      (if display_ghost
-       then (fun fmt -> Format.fprintf fmt "@ %t"
-                (fun fmt -> self#pp_close_annotation ~block:false fmt))
-       else ignore)
+    Format.fprintf fmt "@[<hov 0>" ;
+    self#in_ghost_if_needed fmt v.vghost ~post_fmt:"@ %t" ~block:false
+      (fun () -> Format.fprintf fmt "%a;" self#vdecl v) ;
+    Format.fprintf fmt "@]"
 
   (* no box around the block *)
   method private unboxed_block
@@ -1541,22 +1557,24 @@ class cil_printer () = object (self)
       match g with
       | GFun (fundec, l) ->
         self#in_current_function fundec.svar;
-        (* If the function has attributes then print a prototype because
-         * GCC cannot accept function attributes in a definition *)
-        let oldattr = fundec.svar.vattr in
-        let oldattr = List.filter keep_attr oldattr in
-        (* Always print the file name before function declarations *)
-        (* Prototype first *)
-        if oldattr <> [] then
-          (self#line_directive fmt l;
-           fprintf fmt "%a@\n"
-             self#vdecl_complete fundec.svar);
-        (* Temporarily remove the function attributes *)
-        fundec.svar.vattr <- [];
-        (* Body now *)
-        self#line_directive ~forcefile:true fmt l;
-        self#fundecl fmt fundec;
-        fundec.svar.vattr <- oldattr;
+        self#in_ghost_if_needed fmt fundec.svar.vghost ~post_fmt:"%t@\n"
+          (fun () ->
+             (* If the function has attributes then print a prototype because
+              * GCC cannot accept function attributes in a definition *)
+             let oldattr = fundec.svar.vattr in
+             let oldattr = List.filter keep_attr oldattr in
+             (* Always print the file name before function declarations *)
+             (* Prototype first *)
+             if oldattr <> [] then
+               (self#line_directive fmt l;
+                fprintf fmt "%a@\n"
+                  self#vdecl_complete fundec.svar);
+             (* Temporarily remove the function attributes *)
+             fundec.svar.vattr <- [];
+             (* Body now *)
+             self#line_directive ~forcefile:true fmt l;
+             self#fundecl fmt fundec;
+             fundec.svar.vattr <- oldattr) ;
         fprintf fmt "@\n";
         self#out_current_function
 
@@ -1610,21 +1628,16 @@ class cil_printer () = object (self)
       | GVar (vi, io, l) ->
         self#line_directive ~forcefile:true fmt l;
         Format.fprintf fmt "@[<hov 2>";
-        if vi.vghost then
-          Format.fprintf fmt "%t %a@ "
-            (fun fmt -> self#pp_open_annotation ~block:false fmt)
-            self#pp_acsl_keyword "ghost";
-        self#vdecl fmt vi;
-        (match io.init with
-         | None -> ()
-         | Some i ->
-           fprintf fmt " =@ ";
-           self#init fmt i;
-        );
-        fprintf fmt ";";
-        if vi.vghost then
-          Format.fprintf fmt "@ %t"
-            (fun fmt -> self#pp_close_annotation ~block:false fmt);
+        self#in_ghost_if_needed fmt vi.vghost ~post_fmt:"@ %t" ~block:false
+          (fun () ->
+             self#vdecl fmt vi;
+             (match io.init with
+              | None -> ()
+              | Some i ->
+                fprintf fmt " =@ ";
+                self#init fmt i;
+             );
+             fprintf fmt ";") ;
         fprintf fmt "@]@\n";
 
         (* print global variable 'extern' declarations *)
@@ -1724,26 +1737,13 @@ class cil_printer () = object (self)
 
   method private fundecl fmt f =
     (* declaration. *)
-    let was_ghost = is_ghost in
-    let entering_ghost = f.svar.vghost && not was_ghost in
-    fprintf fmt "@[%t%a@\n@[<v 2>"
-      (if entering_ghost then (fun fmt ->
-           Format.fprintf fmt "%t %a@ "
-             (fun fmt -> self#pp_open_annotation ~block:false fmt)
-             self#pp_acsl_keyword "ghost")
-       else ignore)
-      self#vdecl f.svar;
-    (* We take care of locals in blocks. *)
-    (*List.iter (fprintf fmt "@\n%a;" self#vdecl) f.slocals ;*)
-    (* body. *)
-    if entering_ghost then is_ghost <- true;
-    self#unboxed_block Body fmt f.sbody;
-    if entering_ghost then is_ghost <- false;
-    fprintf fmt "@]%t@]@."
-      (if entering_ghost
-       then (fun fmt -> Format.fprintf fmt "@ %t"
-                (fun fmt -> self#pp_close_annotation ~block:false fmt))
-       else ignore)
+    fprintf fmt "@[";
+    self#in_ghost_if_needed fmt f.svar.vghost ~post_fmt:"@ %t" ~block:false
+      (fun () ->
+         fprintf fmt "%a@\n@[<v 2>" self#vdecl f.svar;
+         self#unboxed_block Body fmt f.sbody;
+         fprintf fmt "@]") ;
+    fprintf fmt "@]@."
 
   (***** PRINTING DECLARATIONS and TYPES ****)
 

src/kernel_services/ast_printing/printer.ml

@@ -167,12 +167,10 @@ class printer_with_annot () = object (self)
     super#global fmt glob
 
   method private begin_annotation fmt =
-    let pre = if is_ghost then Some ("@@/": Pretty_utils.sformat) else None in
-    self#pp_open_annotation ~block:false ?pre fmt
+    self#pp_open_annotation ~block:false fmt
 
   method private end_annotation fmt =
-    let suf = if is_ghost then Some ("@@/": Pretty_utils.sformat) else None in
-    self#pp_close_annotation ~block:false ?suf fmt
+    self#pp_close_annotation ~block:false fmt
 
   method private loop_annotations fmt annots =
     if annots <> [] then
@@ -215,35 +213,22 @@ class printer_with_annot () = object (self)
           Cil_datatype.Code_annotation.compare
           (Annotations.code_annot s)
       in
-      let pGhost fmt s =
-        let was_ghost = is_ghost in
-        if not was_ghost && s.ghost then begin
-          Format.fprintf fmt "%t %a "
-            (fun fmt -> self#pp_open_annotation ~pre:"@[/*@@" fmt)
-            self#pp_acsl_keyword "ghost";
-          is_ghost <- true
-        end;
-        self#stmtkind s.sattr next fmt s.skind;
-        if not was_ghost && s.ghost then begin
-          self#pp_close_annotation ~suf:"@,*/@]" fmt;
-          is_ghost <- false;
-        end
-      in
-      (match all_annot with
-       | [] -> pGhost fmt s
-       | [ a ] when Cil.is_skip s.skind && not s.ghost ->
-         Format.fprintf fmt "@[<hv>@[%t@ %a@;<1 1>%t@]@ %a@]"
-           (fun fmt -> self#pp_open_annotation ~block:false fmt)
-           self#code_annotation a
-           (fun fmt -> self#pp_close_annotation ~block:false fmt)
-           (self#stmtkind s.sattr next) s.skind;
-       | _ ->
-         let loop_annot, stmt_annot =
-           List.partition Logic_utils.is_loop_annot all_annot
-         in
-         self#annotations fmt stmt_annot;
-         self#loop_annotations fmt loop_annot;
-         pGhost fmt s)
+      self#in_ghost_if_needed fmt s.ghost ~post_fmt:"%t"
+        (fun () -> match all_annot with
+           | [] ->  self#stmtkind s.sattr next fmt s.skind;
+           | [ a ] when Cil.is_skip s.skind && not s.ghost ->
+             Format.fprintf fmt "@[<hv>@[%t@ %a@;<1 1>%t@]@ %a@]"
+               self#begin_annotation
+               self#code_annotation a
+               self#end_annotation
+               (self#stmtkind s.sattr next) s.skind;
+           | _ ->
+             let loop_annot, stmt_annot =
+               List.partition Logic_utils.is_loop_annot all_annot
+             in
+             self#annotations fmt stmt_annot;
+             self#loop_annotations fmt loop_annot;
+             self#stmtkind s.sattr next fmt s.skind) ;
     end else
       self#stmtkind s.sattr next fmt s.skind;
     Format.pp_close_box fmt ()

src/kernel_services/ast_printing/printer_api.mli

@@ -78,6 +78,22 @@ class type extensible_printer_type = object
   method private has_annot: bool
   (** [true] if [current_stmt] has some annotations attached to it. *)
 
+  method private in_ghost_if_needed:
+    Format.formatter ->
+    bool ->
+    post_fmt:(((Format.formatter -> unit) -> unit, Format.formatter, unit) format) ->
+    ?block:bool ->
+    (unit -> unit)
+    -> unit
+  (** Open a ghost context if the the first [bool] is true and we are not
+      already in a ghost context. [post_fmt] is a format like ["%t"] and is used
+      to define the format at the end of the ghost context. [block] indicates
+      whether we should open a C block or not (defaults to [true]). The last
+      parameter is the function to be applied in the ghost context (generally
+      some AST element).
+
+      @since 19.0-Potassium+dev *)
+
   method private current_stmt: stmt option
   (** @return the [stmt] being printed *)
 

tests/pretty_printing/annotations.i

+/*@ axiomatic A {
+    predicate P(integer x) reads \nothing ;
+  }
+*/
+
+//@ ghost int global_decl ;
+//@ ghost int global_def = 42 ;
+
+/*@
+  requires P(x) && x > 0 ;
+  ensures P(x) ;
+*/
+void function_no_ghost(int x) {
+  int y = 0;
+
+  /*@ loop invariant 0 <= y <= x ;
+      loop assigns y ;
+      loop variant x - y ; */
+  while (y < x) {
+    /*@ assert y < x ; */
+    y++;
+    /*@ assert y <= x ; */
+  }
+
+  //@ assert y == x ;
+
+  /*@ requires y == x ;
+      assigns y ;
+      ensures y != x ;
+  */ {
+    y -- ;
+    y *= 2 ;
+  }
+
+  //@ requires y >= 0 ;
+  y /= y ;
+}
+
+/*@
+  requires P(x) && x > 0 ;
+  ensures P(x) ;
+*/
+void function_with_ghost(int x) {
+  //@ ghost int y = 0;
+
+  /*@ ghost
+    /@ loop invariant 0 <= y <= x ;
+       loop assigns y ;
+       loop variant x - y ; @/
+    while (y < x) {
+      /@ assert y < x ; @/
+      y++;
+      /@ assert y <= x ; @/
+    }
+  */
+
+  //@ assert y == x ;
+
+  /*@ ghost
+    /@ requires y == x ;
+       assigns y ;
+       ensures y != x ;
+    @/ {
+      y -- ;
+      y *= 2 ;
+    }
+  */
+
+  /*@ ghost
+    //@ requires y >= 0 ;
+    y /= y ;
+  */
+}
+
+/* @ ghost TODO: reactivate this test when ghost-functions are supported
+  /@
+    requires P(x) && x > 0 ;
+    ensures P(x) ;
+  @/
+  void ghost_function(int x) {
+    int y = 0;
+
+    /@ loop invariant 0 <= y <= x ;
+       loop assigns y ;
+       loop variant x - y ; @/
+    while (y < x) {
+      /@ assert y < x ; @/
+      y++;
+      /@ assert y <= x ; @/
+    }
+    
+    /@ assert y == x ; @/
+
+    /@ requires y == x ;
+       assigns y ;
+       ensures y != x ;
+    @/ {
+      y -- ;
+      y *= 2 ;
+    }
+
+    //@ requires y >= 0 ;
+    y /= y ;
+}
+*/
+
+/* @ ghost TODO: reactivate this test when ghost-functions are supported
+  void function_declaration(int variable) ;
+*/
+
+void reference_function(void){
+  // @ ghost function_declaration(42) ;
+}

tests/pretty_printing/oracle/annotations.res.oracle

+[kernel] Parsing tests/pretty_printing/annotations.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ axiomatic A {
+      predicate P(ℤ x) 
+        reads \nothing;
+      
+      }
+ */
+/*@ ghost int global_decl; */
+/*@ ghost int global_def = 42; */
+/*@ requires P(x) ∧ x > 0;
+    ensures P(\old(x)); */
+void function_no_ghost(int x)
+{
+  int y = 0;
+  /*@ loop invariant 0 ≤ y ≤ x;
+      loop assigns y;
+      loop variant x - y; */
+  while (y < x) {
+    /*@ assert y < x; */ ;
+    y ++;
+    /*@ assert y ≤ x; */ ;
+  }
+  /*@ assert y ≡ x; */ ;
+  /*@ requires y ≡ x;
+      ensures y ≢ x;
+      assigns y; */
+  {
+    y --;
+    y *= 2;
+  }
+  /*@ requires y ≥ 0; */
+  y /= y;
+  return;
+}
+
+/*@ requires P(x) ∧ x > 0;
+    ensures P(\old(x)); */
+void function_with_ghost(int x)
+{
+  /*@ ghost int y = 0; */
+  /*@ ghost
+    /@ loop invariant 0 ≤ y ≤ x;
+       loop assigns y;
+       loop variant x - y; @/
+    while (y < x) {
+      /@ assert y < x; @/
+      ;
+      y ++;
+      /@ assert y ≤ x; @/
+      ;
+    }
+  */
+  /*@ assert y ≡ x; */ ;
+  /*@ ghost
+    /@ requires y ≡ x;
+       ensures y ≢ x;
+       assigns y; @/
+    {
+      y --;
+      y *= 2;
+    }
+  */
+  /*@ ghost /@ requires y ≥ 0; @/
+    y /= y; */
+  return;
+}
+
+void reference_function(void)
+{
+  return;
+}
+
+
+[kernel] Parsing tests/pretty_printing/result/annotations.c (with preprocessing)
+[kernel] Parsing tests/pretty_printing/annotations.i (no preprocessing)
+[kernel] tests/pretty_printing/annotations.i:13: Warning: 
+  def'n of func function_no_ghost at tests/pretty_printing/annotations.i:13 (sum 9297192) conflicts with the one at tests/pretty_printing/result/annotations.c:12 (sum 14988159); keeping the one at tests/pretty_printing/result/annotations.c:12.
+[kernel] tests/pretty_printing/annotations.i:43: Warning: 
+  def'n of func function_with_ghost at tests/pretty_printing/annotations.i:43 (sum 9297192) conflicts with the one at tests/pretty_printing/result/annotations.c:38 (sum 14988159); keeping the one at tests/pretty_printing/result/annotations.c:38.
+[kernel] tests/pretty_printing/annotations.i:111: Warning: 
+  dropping duplicate def'n of func reference_function at tests/pretty_printing/annotations.i:111 in favor of that at tests/pretty_printing/result/annotations.c:68
+/* Generated by Frama-C */
+/*@ axiomatic A {
+      predicate P(ℤ x) 
+        reads \nothing;
+      
+      }
+ */
+/*@ ghost int global_decl; */
+/*@ ghost int global_def = 42; */
+/*@ requires P(x) ∧ x > 0;
+    ensures P(\old(x)); */
+void function_no_ghost(int x)
+{
+  int y = 0;
+  /*@ loop invariant 0 ≤ y ≤ x;
+      loop assigns y;
+      loop variant x - y; */
+  while (y < x) {
+    /*@ assert y < x; */ ;
+    y ++;
+    /*@ assert y ≤ x; */ ;
+  }
+  /*@ assert y ≡ x; */ ;
+  /*@ requires y ≡ x;
+      ensures y ≢ x;
+      assigns y; */
+  {
+    y --;
+    y *= 2;
+  }
+  /*@ requires y ≥ 0; */
+  y /= y;
+  return;
+}
+
+/*@ requires P(x) ∧ x > 0;
+    ensures P(\old(x)); */
+void function_with_ghost(int x)
+{
+  /*@ ghost int y = 0; */
+  /*@ ghost
+    /@ loop invariant 0 ≤ y ≤ x;
+       loop assigns y;
+       loop variant x - y; @/
+    while (y < x) {
+      /@ assert y < x; @/
+      ;
+      y ++;
+      /@ assert y ≤ x; @/
+      ;
+    }
+  */
+  /*@ assert y ≡ x; */ ;
+  /*@ ghost
+    /@ requires y ≡ x;
+       ensures y ≢ x;
+       assigns y; @/
+    {
+      y --;
+      y *= 2;
+    }
+  */
+  /*@ ghost /@ requires y ≥ 0; @/
+    y /= y; */
+  return;
+}
+
+void reference_function(void)
+{
+  return;
+}
+
+

tests/syntax/oracle/ghost_multiline_annot.0.res.oracle

@@ -3,12 +3,14 @@
 int main(int c)
 {
   int __retres;
-  /*@ requires c ≥ 0; */
-  /*@ ghost int x = c; */
-  /*@ loop invariant x ≥ 0;
-      loop assigns x;
-      loop variant x; */
-  /*@ ghost while (x > 0) x --; */
+  /*@ ghost /@ requires c ≥ 0; @/
+    int x = c; */
+  /*@ ghost
+    /@ loop invariant x ≥ 0;
+       loop assigns x;
+       loop variant x; @/
+    while (x > 0) x --;
+  */
   __retres = 0;
   return __retres;
 }

tests/syntax/oracle/ghost_multiline_annot.6.res.oracle

@@ -4,9 +4,10 @@ int main(void)
 {
   int __retres;
   /*@ ghost int x = 10; */
-  /*@ loop invariant x ≥ 0;
-      loop variant x; */
-  /*@ ghost while (x > 0) x --; */
+  /*@ ghost /@ loop invariant x ≥ 0;
+               loop variant x; @/
+            while (x > 0) x --;
+  */
   __retres = 0;
   return __retres;
 }

tests/syntax/oracle/ghost_multiline_annot.7.res.oracle

@@ -3,12 +3,14 @@
 int main(int c)
 {
   int __retres;
-  /*@ requires c ≥ 0; */
-  /*@ ghost int x = c; */
-  /*@ loop invariant x ≥ 0;
-      loop invariant x ≡ x;
-      loop variant x; */
-  /*@ ghost while (x > 0) x --; */
+  /*@ ghost /@ requires c ≥ 0; @/
+    int x = c; */
+  /*@ ghost
+    /@ loop invariant x ≥ 0;
+       loop invariant x ≡ x;
+       loop variant x; @/
+    while (x > 0) x --;
+  */
   __retres = 0;
   return __retres;
 }

tests/syntax/oracle/ghost_multiline_annot.8.res.oracle

@@ -3,12 +3,14 @@
 int main(int c)
 {
   int __retres;
-  /*@ requires c ≥ 0; */
-  /*@ ghost int x = c; */
-  /*@ loop invariant x ≥ 0;
-      loop invariant x ≡ x;
-      loop variant x; */
-  /*@ ghost while (x > 0) x --; */
+  /*@ ghost /@ requires c ≥ 0; @/
+    int x = c; */
+  /*@ ghost
+    /@ loop invariant x ≥ 0;
+       loop invariant x ≡ x;
+       loop variant x; @/
+    while (x > 0) x --;
+  */
   __retres = 0;
   return __retres;
 }