From 76f4aa1b99dfd76d463221e0fc5647149025a55d Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 9 Sep 2019 11:58:26 +0200
Subject: [PATCH] [AST Printing] Ensures that ghost annotations are correctly
PP
---
src/kernel_services/ast_printing/printer.ml | 65 ++++----
tests/pretty_printing/annotations.i | 113 +++++++++++++
.../oracle/annotations.res.oracle | 155 ++++++++++++++++++
.../oracle/ghost_multiline_annot.0.res.oracle | 14 +-
.../oracle/ghost_multiline_annot.6.res.oracle | 7 +-
.../oracle/ghost_multiline_annot.7.res.oracle | 14 +-
.../oracle/ghost_multiline_annot.8.res.oracle | 14 +-
7 files changed, 328 insertions(+), 54 deletions(-)
create mode 100644 tests/pretty_printing/annotations.i
create mode 100644 tests/pretty_printing/oracle/annotations.res.oracle
diff --git a/src/kernel_services/ast_printing/printer.ml b/src/kernel_services/ast_printing/printer.ml
index 294c40cd742..e4dc9bdfc87 100644
--- a/src/kernel_services/ast_printing/printer.ml
+++ b/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
@@ -191,6 +189,20 @@ class printer_with_annot () = object (self)
fmt
annots
+ method private in_ghost_if_needed fmt ghost_flag 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 fmt)
+ self#pp_acsl_keyword "ghost"
+ end ;
+ do_it () ;
+ if display_ghost then begin
+ is_ghost <- false;
+ Format.fprintf fmt "%t@]" (fun fmt -> self#pp_close_annotation fmt)
+ end
+
method! annotated_stmt next fmt s =
(* To debug location setting:
(let loc = fst (Cil_datatype.Stmt.loc s.skind) in
@@ -215,35 +227,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
+ (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 ()
diff --git a/tests/pretty_printing/annotations.i b/tests/pretty_printing/annotations.i
new file mode 100644
index 00000000000..1d80a03ba03
--- /dev/null
+++ b/tests/pretty_printing/annotations.i
@@ -0,0 +1,113 @@
+/*@ 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) ;
+}
diff --git a/tests/pretty_printing/oracle/annotations.res.oracle b/tests/pretty_printing/oracle/annotations.res.oracle
new file mode 100644
index 00000000000..e0259ac8679
--- /dev/null
+++ b/tests/pretty_printing/oracle/annotations.res.oracle
@@ -0,0 +1,155 @@
+[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;
+}
+
+
diff --git a/tests/syntax/oracle/ghost_multiline_annot.0.res.oracle b/tests/syntax/oracle/ghost_multiline_annot.0.res.oracle
index a1b72856b21..c8071303034 100644
--- a/tests/syntax/oracle/ghost_multiline_annot.0.res.oracle
+++ b/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;
}
diff --git a/tests/syntax/oracle/ghost_multiline_annot.6.res.oracle b/tests/syntax/oracle/ghost_multiline_annot.6.res.oracle
index 2a924d8ae0e..a7859b320dd 100644
--- a/tests/syntax/oracle/ghost_multiline_annot.6.res.oracle
+++ b/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;
}
diff --git a/tests/syntax/oracle/ghost_multiline_annot.7.res.oracle b/tests/syntax/oracle/ghost_multiline_annot.7.res.oracle
index 2019d87badc..6ee6fd7133f 100644
--- a/tests/syntax/oracle/ghost_multiline_annot.7.res.oracle
+++ b/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;
}
diff --git a/tests/syntax/oracle/ghost_multiline_annot.8.res.oracle b/tests/syntax/oracle/ghost_multiline_annot.8.res.oracle
index 2019d87badc..6ee6fd7133f 100644
--- a/tests/syntax/oracle/ghost_multiline_annot.8.res.oracle
+++ b/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;
}
--
GitLab