[aorai] avoid using logical operators in C code if LogicOperator is off

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

src/plugins/aorai/tests/ya/logical_operators.i

+/* 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);
+}

src/plugins/aorai/tests/ya/logical_operators.ya

+%init : I;
+
+I: { f().x == 1 } -> I | other -> I;

src/plugins/aorai/tests/ya/oracle/logical_operators.res.oracle

+[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;
+}
+
+

src/plugins/aorai/tests/ya/oracle_prove/logical_operators.res.oracle

+[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