From 414a40b1e047cd77e4a9fe7d3ea7b58c834d456b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 16 Apr 2024 17:50:27 +0200
Subject: [PATCH] [Impact] Uses an ACSL extension instead of impact pragma.
---
src/plugins/impact/register.ml | 73 +++++++++++---------------
src/plugins/impact/register.mli | 4 +-
tests/impact/alias.i | 2 +-
tests/impact/call.i | 8 +--
tests/impact/called.i | 4 +-
tests/impact/depend1.i | 2 +-
tests/impact/depend2.i | 2 +-
tests/impact/depend3.c | 2 +-
tests/impact/depend4.i | 2 +-
tests/impact/depend5.i | 3 +-
tests/impact/first.i | 4 +-
tests/impact/initial.i | 8 +--
tests/impact/loop.i | 4 +-
tests/impact/loop2.i | 2 +-
tests/impact/oracle/slicing.res.oracle | 2 +-
tests/impact/slicing.i | 4 +-
tests/impact/topbot.c | 2 +-
tests/impact/undef_function.i | 2 +-
tests/impact/variadic.i | 12 ++---
tests/value/dead_code.i | 4 +-
20 files changed, 68 insertions(+), 78 deletions(-)
diff --git a/src/plugins/impact/register.ml b/src/plugins/impact/register.ml
index 817fae52b38..5db8ea3d06d 100644
--- a/src/plugins/impact/register.ml
+++ b/src/plugins/impact/register.ml
@@ -98,52 +98,43 @@ let slice (stmts:stmt list) =
Options.feedback ~level:2 "slicing done";
extracted_prj
-let all_pragmas_kf l =
- List.fold_left
- (fun acc (s, a) ->
- match a.annot_content with
- | APragma (Impact_pragma IPstmt) -> s :: acc
- | APragma (Impact_pragma (IPexpr _)) ->
- Options.not_yet_implemented "impact pragmas: expr"
- | _ -> assert false)
- [] l
-
-let compute_pragmas () =
- Ast.compute ();
- let pragmas = ref [] in
- let visitor = object
- inherit Visitor.frama_c_inplace as super
-
- method! vfunc f =
- pragmas := [];
- super#vfunc f
-
- method! vstmt_aux s =
- pragmas :=
- List.map
- (fun a -> s, a)
- (Annotations.code_annot ~filter:Logic_utils.is_impact_pragma s)
- @ !pragmas;
- Cil.DoChildren
- end
+
+(* Register impact ACSL extension. *)
+let () =
+ let typer typing_context loc args =
+ match args with
+ | [] -> Ext_terms []
+ | _ -> typing_context.Logic_typing.error loc "Invalid impact directive"
in
+ Acsl_extension.register_code_annot_next_both
+ ~plugin:"impact" "impact_stmt" typer false
+
+let is_impact_annot code_annot =
+ match code_annot.annot_content with
+ | AExtended (_, _, { ext_name = "impact_stmt"; }) -> true
+ | _ -> false
+
+let compute_annots () =
+ Ast.compute ();
(* fill [pragmas] with all the pragmas of all the selected functions *)
- let pragmas =
- Options.Pragma.fold
- (fun kf acc ->
- (* Pragma option only accept defined functions. *)
- let f = Kernel_function.get_definition kf in
- ignore (Visitor.visitFramacFunction visitor f);
- if !pragmas != [] then (kf, !pragmas) :: acc else acc)
- []
+ let process kf acc =
+ (* Pragma option only accept defined functions. *)
+ let fundec = Kernel_function.get_definition kf in
+ let has_impact_annot stmt =
+ let impact_annots = Annotations.code_annot ~filter:is_impact_annot stmt in
+ not (impact_annots = [])
+ in
+ let impact_stmts = List.filter has_impact_annot fundec.sallstmts in
+ if impact_stmts = [] then acc
+ else (kf, impact_stmts) :: acc
in
+ let impact_stmts = Options.Pragma.fold process [] in
let skip = Compute_impact.skip () in
(* compute impact analyses on each kf *)
let nodes = List.fold_left
- (fun nodes (kf, pragmas) ->
- let pragmas_stmts = all_pragmas_kf pragmas in
- Pdg_aux.NS.union nodes (compute_multiple_stmts skip kf pragmas_stmts)
- ) Pdg_aux.NS.empty pragmas
+ (fun nodes (kf, stmts) ->
+ Pdg_aux.NS.union nodes (compute_multiple_stmts skip kf stmts))
+ Pdg_aux.NS.empty impact_stmts
in
let stmts = Compute_impact.nodes_to_stmts nodes in
if Options.Slicing.get () then ignore (slice stmts);
@@ -158,7 +149,7 @@ let main () =
if Options.is_on () then begin
Options.feedback "beginning analysis";
assert (not (Options.Pragma.is_empty ()));
- ignore (compute_pragmas ());
+ ignore (compute_annots ());
Options.feedback "analysis done"
end
let () = Boot.Main.extend main
diff --git a/src/plugins/impact/register.mli b/src/plugins/impact/register.mli
index 35e476eb808..7a5f7aa71d1 100644
--- a/src/plugins/impact/register.mli
+++ b/src/plugins/impact/register.mli
@@ -24,8 +24,8 @@ open Cil_types
open Pdg_types
-val compute_pragmas: (unit -> stmt list)
-(** Compute the impact analysis from the impact pragma in the program.
+val compute_annots: (unit -> stmt list)
+(** Compute the impact analysis from the impact annotations in the program.
Print and slice the results according to the parameters -impact-print
and -impact-slice.
@return the impacted statements *)
diff --git a/tests/impact/alias.i b/tests/impact/alias.i
index 1b4edfb05d1..b44ead94109 100644
--- a/tests/impact/alias.i
+++ b/tests/impact/alias.i
@@ -6,7 +6,7 @@ int P,c;
/*@ requires \valid(x); */
int f(int *x) {
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
int *y = x+1;
*y = 4;
int a = *(x+1) + 2;
diff --git a/tests/impact/call.i b/tests/impact/call.i
index c2c1e339205..64ee9f379f3 100644
--- a/tests/impact/call.i
+++ b/tests/impact/call.i
@@ -1,5 +1,5 @@
/* run.config
-
+
STDOPT: +"-impact-pragma main"
STDOPT: +"-impact-pragma main2" +"-main main2"
STDOPT: +"-impact-pragma main3" +"-main main3"
@@ -19,7 +19,7 @@ void test (void) {
/* ************************************************************************* */
void main (int x) {
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
X = x;
test ();
}
@@ -31,7 +31,7 @@ void call_test (void) {
}
void main2(int x) {
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
X = x;
call_test ();
}
@@ -50,7 +50,7 @@ void call_test3 (void) {
}
void main3(int x) {
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
X = x;
call_test3 ();
}
diff --git a/tests/impact/called.i b/tests/impact/called.i
index 5971b9e56ba..db29ddef5c3 100644
--- a/tests/impact/called.i
+++ b/tests/impact/called.i
@@ -10,7 +10,7 @@ int f(int x, int y) { X = x; return y; }
void g() {
int a, b, c, d;
b = 0;
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
a = 0;
c = f(a,b);
d = X;
@@ -19,7 +19,7 @@ void g() {
void h() {
int a, b, c, d;
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
b = 0;
a = 0;
c = f(a,b);
diff --git a/tests/impact/depend1.i b/tests/impact/depend1.i
index 6b3b3c0e81f..cb03869b56b 100644
--- a/tests/impact/depend1.i
+++ b/tests/impact/depend1.i
@@ -8,7 +8,7 @@ int find(int x) { return x; }
int main()
{
int a = find(1);
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
int b = find(2);
int c = find(b);
int d = find(3);
diff --git a/tests/impact/depend2.i b/tests/impact/depend2.i
index dbc0a3ccc29..58b27ff58a5 100644
--- a/tests/impact/depend2.i
+++ b/tests/impact/depend2.i
@@ -9,7 +9,7 @@ int apply(int x,int y) { return find(x)+y; }
int main()
{
int a = apply(1,100);
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
int b = apply(2,200);
return a+b ;
}
diff --git a/tests/impact/depend3.c b/tests/impact/depend3.c
index 4f08af95fee..1eb4778f27c 100644
--- a/tests/impact/depend3.c
+++ b/tests/impact/depend3.c
@@ -20,7 +20,7 @@ int apply(int x,int y) { return find(x); }
int main()
{
int a = apply( 1 , 100 );
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
int b = apply( 2 , 200 );
return a+b ;
}
diff --git a/tests/impact/depend4.i b/tests/impact/depend4.i
index 3eefa9de01d..6368d46ea25 100644
--- a/tests/impact/depend4.i
+++ b/tests/impact/depend4.i
@@ -25,7 +25,7 @@ void g2() {
void main () {
g1();
- //@ impact pragma stmt;
+ //@ impact_stmt;
f();
g2();
}
diff --git a/tests/impact/depend5.i b/tests/impact/depend5.i
index 52b560fbce0..e4800e4a54a 100644
--- a/tests/impact/depend5.i
+++ b/tests/impact/depend5.i
@@ -12,7 +12,7 @@ void f() {
}
void g() {
- //@ impact pragma stmt;
+ //@ impact_stmt;
d = 2;
e = d;
f();
@@ -24,4 +24,3 @@ void main () {
a = 0;
g();
}
-
diff --git a/tests/impact/first.i b/tests/impact/first.i
index a210dbb40e8..d99654b37d5 100644
--- a/tests/impact/first.i
+++ b/tests/impact/first.i
@@ -1,12 +1,12 @@
/* run.config
-
+
STDOPT: +"-impact-pragma impact" +"-lib-entry" +"-main impact"
*/
int a, b, c, e, x, y, z, f, w;
void impact() {
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
b = a;
if (c) {
x = b + c;
diff --git a/tests/impact/initial.i b/tests/impact/initial.i
index 9c20d16edba..2d815c5edfb 100644
--- a/tests/impact/initial.i
+++ b/tests/impact/initial.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: also tests the parsing of cmdline options of type string_set
- STDOPT: +"-pdg-verbose 0" +"-main main1 -impact-pragma g1" +"-then -main main2 -impact-pragma='-@all,+g2'" +"-then -main main3 -impact-pragma='-g2,+g3'"
+ STDOPT: +"-pdg-verbose 0" +"-main main1 -impact-pragma g1" +"-then -main main2 -impact-pragma='-@all,+g2'" +"-then -main main3 -impact-pragma='-g2,+g3'"
*/
int x1, x2, y2, z2, x3;
@@ -15,7 +15,7 @@ void f1() {
void g1() {
if (c) {
- //@ impact pragma stmt;
+ //@ impact_stmt;
f1();
}
}
@@ -42,7 +42,7 @@ void aux2() {
void g2() {
if (c) {
- //@ impact pragma stmt;
+ //@ impact_stmt;
f2();
if (c) aux2();
}
@@ -65,7 +65,7 @@ void f3() {
void g3() {
- //@ impact pragma stmt;
+ //@ impact_stmt;
f3();
if (c) {
x3 = x3;
diff --git a/tests/impact/loop.i b/tests/impact/loop.i
index 0f8960d4aee..f1c26e9d35c 100644
--- a/tests/impact/loop.i
+++ b/tests/impact/loop.i
@@ -1,5 +1,5 @@
/* run.config
-
+
STDOPT: +"-impact-pragma loop" +"-lib-entry" +"-main loop"
*/
@@ -9,7 +9,7 @@ void loop () {
while (c) {
z = w + 1;
z = y + 1;
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
x = x + 1;
y = x + 1;
}
diff --git a/tests/impact/loop2.i b/tests/impact/loop2.i
index 431ef94ee5b..c6ff73de8e9 100644
--- a/tests/impact/loop2.i
+++ b/tests/impact/loop2.i
@@ -20,7 +20,7 @@ void f(int i) {
}
void main() {
- //@ impact pragma stmt;
+ //@ impact_stmt;
init ();
for (int i=0; i<10; i++) {
if (t[i]) // should not be selected
diff --git a/tests/impact/oracle/slicing.res.oracle b/tests/impact/oracle/slicing.res.oracle
index bcb4ba87e43..07899df4b03 100644
--- a/tests/impact/oracle/slicing.res.oracle
+++ b/tests/impact/oracle/slicing.res.oracle
@@ -54,7 +54,7 @@ int w;
void impact(void)
{
if (c) a = 18;
- /*@ impact pragma stmt; */
+ /*@ \impact::impact_stmt ; */
b = a;
if (c) {
x = b + c;
diff --git a/tests/impact/slicing.i b/tests/impact/slicing.i
index 93e008b3564..96b55a1278f 100644
--- a/tests/impact/slicing.i
+++ b/tests/impact/slicing.i
@@ -1,5 +1,5 @@
/* run.config
-
+
STDOPT: +"-impact-pragma impact" +"-lib-entry" +"-main impact" +"-impact-slicing" +"-then-on 'impact slicing'" +"-print"
*/
@@ -7,7 +7,7 @@ int a, b, c, e, x, y, z, f, w;
void impact() {
if (c) a = 18; else x = 5;
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
b = a;
if (c) {
x = b + c;
diff --git a/tests/impact/topbot.c b/tests/impact/topbot.c
index 55d424eb28a..60b8397b97d 100644
--- a/tests/impact/topbot.c
+++ b/tests/impact/topbot.c
@@ -7,7 +7,7 @@ void f() { // Bottom PDG
}
void main(int c) {
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
int x = 1;
int y, z;
if (c) {
diff --git a/tests/impact/undef_function.i b/tests/impact/undef_function.i
index 4c7dc4550ca..156bd3e9f53 100644
--- a/tests/impact/undef_function.i
+++ b/tests/impact/undef_function.i
@@ -5,7 +5,7 @@ int y;
void g(int);
int main() {
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
y=2;
g(y);
return y;
diff --git a/tests/impact/variadic.i b/tests/impact/variadic.i
index c08694d9de5..3746a648146 100644
--- a/tests/impact/variadic.i
+++ b/tests/impact/variadic.i
@@ -1,13 +1,13 @@
/* run.config
COMMENT: also tests the parsing of cmdline options of type string_set
- STDOPT: +"-impact-pragma main" +"-then -main main1 -impact-pragma='-main,+main1'" +"-then -main main2 -impact-pragma='-@all,+main2'" +"-then -main main3 -impact-pragma='+aux3,-main2'" +"-then -main main4 -impact-pragma='-aux3,+aux4'"
+ STDOPT: +"-impact-pragma main" +"-then -main main1 -impact-pragma='-main,+main1'" +"-then -main main2 -impact-pragma='-@all,+main2'" +"-then -main main3 -impact-pragma='+aux3,-main2'" +"-then -main main4 -impact-pragma='-aux3,+aux4'"
*/
int f(int, ...);
int main () {
int i=0;
- /*@ impact pragma stmt; */
+ /*@ impact_stmt; */
i++;
f(i);
}
@@ -25,7 +25,7 @@ void g2(int x, ...);
int main1() {
int x = 3;
- //@ impact pragma stmt;
+ //@ impact_stmt;
g1(1, 2, 3);
g1(1, 2);
return y;
@@ -33,7 +33,7 @@ int main1() {
int main2() {
int x = 3;
- //@ impact pragma stmt;
+ //@ impact_stmt;
g2(1, 2, 3);
g2(1, 2);
return y;
@@ -47,7 +47,7 @@ void g3(int , ...);
int aux3(int x, ...) {
int t = 3;
- //@ impact pragma stmt;
+ //@ impact_stmt;
g1(t);
g1(t);
return y;
@@ -60,7 +60,7 @@ int main3() {
}
void aux4(int x) {
- //@ impact pragma stmt;
+ //@ impact_stmt;
y = x;
}
diff --git a/tests/value/dead_code.i b/tests/value/dead_code.i
index e0c5d2be956..42e5d138ea8 100644
--- a/tests/value/dead_code.i
+++ b/tests/value/dead_code.i
@@ -1,8 +1,8 @@
void main(int in) {
int i,j=6,k,l;
-
+
i=10;
- //@ impact pragma stmt;
+
i=1;
L: if (i) {l= 17 ; goto OUT;}
// i--;
--
GitLab