From ce7bf0772650c315f70a21330d5b75f9fd03ea3c Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 11 Jan 2021 19:45:37 +0100
Subject: [PATCH] [aorai] avoid using logical operators in C code if
LogicOperator is off
---
src/plugins/aorai/aorai_utils.ml | 43 ++++-
.../aorai/tests/ya/logical_operators.i | 9 +
.../aorai/tests/ya/logical_operators.ya | 3 +
.../ya/oracle/logical_operators.res.oracle | 161 ++++++++++++++++++
.../oracle_prove/logical_operators.res.oracle | 4 +
5 files changed, 219 insertions(+), 1 deletion(-)
create mode 100644 src/plugins/aorai/tests/ya/logical_operators.i
create mode 100644 src/plugins/aorai/tests/ya/logical_operators.ya
create mode 100644 src/plugins/aorai/tests/ya/oracle/logical_operators.res.oracle
create mode 100644 src/plugins/aorai/tests/ya/oracle_prove/logical_operators.res.oracle
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index dd533767fdd..2acc111a6f0 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -1982,8 +1982,49 @@ let mk_transitions_stmt generated_kf loc f st res trans =
trans
([],[],Cil_datatype.Varinfo.Set.empty, Cil.zero ~loc, [])
+let mk_goto loc b =
+ let ghost = true in
+ match b.bstmts with
+ | [] -> Cil.mkBlock []
+ | [ { skind = Instr i } ] ->
+ let s = mkStmtOneInstr ~ghost i in
+ Cil.mkBlock [s]
+ | [ { skind = Goto (s,_) }] ->
+ let s' = mkStmt ~ghost (Goto (ref !s,loc)) in
+ Cil.mkBlock [s']
+ | s::_ ->
+ s.labels <-
+ (Label(Data_for_aorai.get_fresh "__aorai_label",loc,false)):: s.labels;
+ let s' = mkStmt ~ghost (Goto (ref s,loc)) in
+ Cil.mkBlock [s']
+
+let normalize_condition loc cond block1 block2 =
+ let rec aux cond b1 b2 =
+ match cond.enode with
+ | UnOp(LNot,e,_) -> aux e b2 b1
+ | BinOp(LAnd,e1,e2,_) ->
+ let b2' = mk_goto loc b2 in
+ let b1'= aux e2 b1 b2' in
+ aux e1 b1' b2
+ | BinOp(LOr,e1,e2,_) ->
+ let b1' = mk_goto loc b1 in
+ let b2' = aux e2 b1' b2 in
+ aux e1 b1 b2'
+ | _ ->
+ Cil.mkBlock [ Cil.mkStmt ~ghost:true (If(cond,b1,b2,loc)) ]
+ in
+ let b = aux cond block1 block2 in
+ match b.bstmts with
+ | [] -> Aorai_option.fatal "If normalization failed"
+ | [ s ] -> s
+ | _ -> Cil.mkStmt ~ghost:true (Block b)
+
let mkIfStmt loc exp1 block1 block2 =
- Cil.mkStmt ~ghost:true (If (exp1, block1, block2, loc))
+ if Kernel.LogicalOperators.get() then
+ Cil.mkStmt ~ghost:true (If (exp1, block1, block2, loc))
+ else
+ normalize_condition loc exp1 block1 block2
+
let mk_deterministic_stmt
generated_kf loc auto f fst status ret state
diff --git a/src/plugins/aorai/tests/ya/logical_operators.i b/src/plugins/aorai/tests/ya/logical_operators.i
new file mode 100644
index 00000000000..3a5beaefe1a
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/logical_operators.i
@@ -0,0 +1,9 @@
+/* run.config*
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+*/
+
+void f(int x) {}
+
+void main(int x) {
+ f(x);
+}
diff --git a/src/plugins/aorai/tests/ya/logical_operators.ya b/src/plugins/aorai/tests/ya/logical_operators.ya
new file mode 100644
index 00000000000..5baf089d910
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/logical_operators.ya
@@ -0,0 +1,3 @@
+%init : I;
+
+I: { f().x == 1 } -> I | other -> I;
diff --git a/src/plugins/aorai/tests/ya/oracle/logical_operators.res.oracle b/src/plugins/aorai/tests/ya/oracle/logical_operators.res.oracle
new file mode 100644
index 00000000000..da665d11dd5
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/oracle/logical_operators.res.oracle
@@ -0,0 +1,161 @@
+[kernel] Parsing tests/ya/logical_operators.i (no preprocessing)
+[aorai] Welcome to the Aorai plugin
+[kernel] Parsing TMPDIR/aorai_logical_operators_0.i (no preprocessing)
+/* Generated by Frama-C */
+enum aorai_ListOper {
+ op_f = 1,
+ op_main = 0
+};
+enum aorai_OpStatusList {
+ aorai_Terminated = 1,
+ aorai_Called = 0
+};
+/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
+/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
+/*@ ghost int I = 1; */
+/*@ ghost
+ /@ requires 1 ≡ I;
+ requires 1 ≡ I ⇒ x ≡ 1 ∨ x ≢ 1;
+ ensures aorai_CurOpStatus ≡ aorai_Called;
+ ensures aorai_CurOperation ≡ op_f;
+ assigns aorai_CurOpStatus, aorai_CurOperation, I;
+
+ behavior buch_state_I_in:
+ assumes 1 ≡ I ∧ (x ≡ 1 ∨ x ≢ 1);
+ ensures 1 ≡ I;
+
+ behavior buch_state_I_out:
+ assumes 0 ≡ I ∨ (¬(x ≡ 1) ∧ ¬(x ≢ 1));
+ ensures 0 ≡ I;
+ @/
+ void f_pre_func(int x)
+ {
+ int I_tmp;
+ aorai_CurOpStatus = aorai_Called;
+ aorai_CurOperation = op_f;
+ I_tmp = I;
+ if (I == 1) {
+ if (x != 1) I_tmp = 1; else goto __aorai_label;
+ }
+ else {
+ __aorai_label: ;
+ if (I == 1)
+ if (x == 1) I_tmp = 1; else I_tmp = 0;
+ else I_tmp = 0;
+ }
+ I = I_tmp;
+ return;
+ }
+
+*/
+
+/*@ ghost
+ /@ requires 1 ≡ I;
+ ensures aorai_CurOpStatus ≡ aorai_Terminated;
+ ensures aorai_CurOperation ≡ op_f;
+ assigns aorai_CurOpStatus, aorai_CurOperation, I;
+
+ behavior buch_state_I_in:
+ assumes 1 ≡ I;
+ ensures 1 ≡ I;
+
+ behavior buch_state_I_out:
+ assumes 0 ≡ I;
+ ensures 0 ≡ I;
+ @/
+ void f_post_func(void)
+ {
+ int I_tmp;
+ aorai_CurOpStatus = aorai_Terminated;
+ aorai_CurOperation = op_f;
+ I_tmp = I;
+ if (I == 1) I_tmp = 1; else I_tmp = 0;
+ I = I_tmp;
+ return;
+ }
+
+*/
+
+/*@ requires 1 ≡ I;
+ requires 1 ≡ I ⇒ x ≡ 1 ∨ x ≢ 1;
+
+ behavior Buchi_property_behavior:
+ ensures \true;
+ ensures 1 ≡ I;
+ */
+void f(int x)
+{
+ /*@ ghost f_pre_func(x); */
+ /*@ ghost f_post_func(); */
+ return;
+}
+
+/*@ ghost
+ /@ requires 1 ≡ I;
+ ensures aorai_CurOpStatus ≡ aorai_Called;
+ ensures aorai_CurOperation ≡ op_main;
+ assigns aorai_CurOpStatus, aorai_CurOperation, I;
+
+ behavior buch_state_I_in:
+ assumes 1 ≡ I;
+ ensures 1 ≡ I;
+
+ behavior buch_state_I_out:
+ assumes 0 ≡ I;
+ ensures 0 ≡ I;
+ @/
+ void main_pre_func(int x)
+ {
+ int I_tmp;
+ aorai_CurOpStatus = aorai_Called;
+ aorai_CurOperation = op_main;
+ I_tmp = I;
+ if (I == 1) I_tmp = 1; else I_tmp = 0;
+ I = I_tmp;
+ return;
+ }
+
+*/
+
+/*@ ghost
+ /@ requires 1 ≡ I;
+ ensures aorai_CurOpStatus ≡ aorai_Terminated;
+ ensures aorai_CurOperation ≡ op_main;
+ assigns aorai_CurOpStatus, aorai_CurOperation, I;
+
+ behavior buch_state_I_in:
+ assumes 1 ≡ I;
+ ensures 1 ≡ I;
+
+ behavior buch_state_I_out:
+ assumes 0 ≡ I;
+ ensures 0 ≡ I;
+ @/
+ void main_post_func(void)
+ {
+ int I_tmp;
+ aorai_CurOpStatus = aorai_Terminated;
+ aorai_CurOperation = op_main;
+ I_tmp = I;
+ if (I == 1) I_tmp = 1; else I_tmp = 0;
+ I = I_tmp;
+ return;
+ }
+
+*/
+
+/*@ requires 1 ≡ I;
+
+ behavior Buchi_property_behavior:
+ ensures \true;
+ ensures 1 ≡ I;
+ */
+void main(int x)
+{
+ /*@ ghost main_pre_func(x); */
+ f(x);
+ /*@ ghost main_post_func(); */
+ return;
+}
+
+
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/logical_operators.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/logical_operators.res.oracle
new file mode 100644
index 00000000000..4f152c30c54
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/oracle_prove/logical_operators.res.oracle
@@ -0,0 +1,4 @@
+[kernel] Parsing tests/ya/logical_operators.i (no preprocessing)
+[aorai] Welcome to the Aorai plugin
+[kernel] Parsing TMPDIR/aorai_logical_operators_0.i (no preprocessing)
+[wp] Warning: Missing RTE guards
--
GitLab