diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 84f577652be9fe9e441826834c0199835914997f..7fd192b397eb99793a3374823b60c8b13786f505 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -435,6 +435,20 @@ let get_float_unop op typ =
| TFloat(fkind,_) , Neg -> float_builtin "neg" fkind
| _ -> None
+let is_boolean_exp e =
+ match e.enode with
+ | BinOp(op,_,_,_) -> is_boolean_binop op
+ | UnOp(LNot,_,_) -> true
+ | _ -> false
+
+let get_bool_kind e =
+ match Cil.isInteger e with
+ | Some i ->
+ if Integer.(equal i zero) then `False else
+ if Integer.(equal i one) then `True else
+ `Term
+ | None -> if is_boolean_exp e then `Bool else `Term
+
let rec expr_to_term ?(coerce=false) e =
let loc = e.eloc in
let typ = Cil.typeOf e in
@@ -444,12 +458,12 @@ let rec expr_to_term ?(coerce=false) e =
| Const c -> TConst (constant_to_lconstant c) , coerce_type typ
| StartOf lv -> TStartOf (lval_to_term_lval lv) , ctyp
| AddrOf lv -> TAddrOf (lval_to_term_lval lv) , ctyp
+ | BinOp (op, _, _, _) when is_boolean_binop op ->
+ let tc = expr_to_boolean e in
+ Tif( tc , Cil.lone ~loc () , Cil.lzero ~loc () ),
+ Linteger
| BinOp (op, a, b, _) ->
- if is_boolean_binop op then
- let tc = expr_to_boolean e in
- Tif( tc , Cil.lone ~loc () , Cil.lzero ~loc () ),
- Linteger
- else begin match get_float_binop op typ with
+ begin match get_float_binop op typ with
| Some phi ->
let va = expr_to_term a in
let vb = expr_to_term b in
@@ -511,17 +525,38 @@ and offset_to_term_offset = function
and expr_to_boolean e =
let open Cil_types in
let tbool n = Logic_const.term n Logic_const.boolean_type in
+ let tnot t = tbool @@ TUnOp(LNot, t) in
+ let tcompare op a b =
+ let va = expr_to_term ~coerce:true a in
+ let vb = expr_to_term ~coerce:true b in
+ tbool @@ TBinOp(op,va,vb)
+ in
match e.enode with
- | UnOp(BNot, a,_) ->
- tbool @@ TUnOp(BNot, expr_to_boolean a)
- | BinOp((BAnd|BOr) as op,a,b,_) ->
+ | UnOp(LNot, a,_) -> tnot (expr_to_boolean a)
+ | BinOp((LAnd|LOr) as op,a,b,_) ->
let va = expr_to_boolean a in
let vb = expr_to_boolean b in
tbool @@ TBinOp(op,va,vb)
- | BinOp(op, a, b, _) when is_boolean_binop op ->
- let va = expr_to_term ~coerce:true a in
- let vb = expr_to_term ~coerce:true b in
- tbool @@ TBinOp(op,va,vb)
+ | BinOp(Eq, a, b, _) ->
+ begin
+ match get_bool_kind a , get_bool_kind b with
+ | `True , `Bool -> expr_to_boolean b
+ | `Bool , `True -> expr_to_boolean a
+ | `False , `Bool -> tnot @@ expr_to_boolean b
+ | `Bool , `False -> tnot @@ expr_to_boolean a
+ | _ -> tcompare Eq a b
+ end
+ | BinOp(Ne, a, b, _) ->
+ begin
+ match get_bool_kind a , get_bool_kind b with
+ | `False , `Bool -> expr_to_boolean b
+ | `Bool , `False -> expr_to_boolean a
+ | `True , `Bool -> tnot @@ expr_to_boolean b
+ | `Bool , `True -> tnot @@ expr_to_boolean a
+ | _ -> tcompare Ne a b
+ end
+ | BinOp((Lt | Gt | Le | Ge) as op, a, b, _) ->
+ tcompare op a b
| _ ->
let t = expr_to_term ~coerce:true e in
if is_zero_comparable t then
@@ -534,6 +569,7 @@ and expr_to_boolean e =
and expr_to_predicate e =
let open Cil_types in
let unamed = Logic_const.unamed ~loc:e.eloc in
+ let pnot p = unamed @@ Pnot p in
let prel r a b =
let va = expr_to_term ~coerce:true a in
let vb = expr_to_term ~coerce:true b in
@@ -543,14 +579,30 @@ and expr_to_predicate e =
| BinOp(Le, a, b, _) -> prel Rle a b
| BinOp(Gt, a, b, _) -> prel Rgt a b
| BinOp(Ge, a, b, _) -> prel Rge a b
- | BinOp(Eq, a, b, _) -> prel Req a b
- | BinOp(Ne, a, b, _) -> prel Rneq a b
- | BinOp(BAnd, a, b, _) ->
+ | BinOp(Eq, a, b, _) ->
+ begin
+ match get_bool_kind a , get_bool_kind b with
+ | `True , `Bool -> expr_to_predicate b
+ | `Bool , `True -> expr_to_predicate a
+ | `False , `Bool -> pnot @@ expr_to_predicate b
+ | `Bool , `False -> pnot @@ expr_to_predicate a
+ | _ -> prel Req a b
+ end
+ | BinOp(Ne, a, b, _) ->
+ begin
+ match get_bool_kind a , get_bool_kind b with
+ | `False , `Bool -> expr_to_predicate b
+ | `Bool , `False -> expr_to_predicate a
+ | `True , `Bool -> pnot @@ expr_to_predicate b
+ | `Bool , `True -> pnot @@ expr_to_predicate a
+ | _ -> prel Rneq a b
+ end
+ | BinOp(LAnd, a, b, _) ->
unamed @@ Pand(expr_to_predicate a,expr_to_predicate b)
- | BinOp(BOr, a, b, _) ->
+ | BinOp(LOr, a, b, _) ->
unamed @@ Por(expr_to_predicate a,expr_to_predicate b)
- | UnOp(BNot, a, _) ->
- unamed @@ Pnot(expr_to_predicate a)
+ | UnOp(LNot, a, _) ->
+ pnot @@ expr_to_predicate a
| _ ->
let t = expr_to_term ~coerce:true e in
if is_zero_comparable t then
diff --git a/tests/spec/expr_to_term.i b/tests/spec/expr_to_term.i
index e0e887144169aea4640bb1f008beabd15bfba32b..88b15b296dc5a2eefe1be5362249a5181c778658 100644
--- a/tests/spec/expr_to_term.i
+++ b/tests/spec/expr_to_term.i
@@ -1,6 +1,6 @@
/* run.config
MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -print
+OPT: -keep-logical-operators -print
*/
@@ -43,3 +43,17 @@ int g() {
int h() {
if (t<5) return 2; else return 3;
}
+
+void expr_to_predicate(int x) { }
+
+
+int z,t;
+/*@ ensures z!=0 && t!=0;
+ ensures !(z<5);
+ ensures (int)(t|5) != 0;
+*/
+void i() {
+ expr_to_predicate(z&&t);
+ expr_to_predicate(!(z<5));
+ expr_to_predicate(t|5);
+}
diff --git a/tests/spec/expr_to_term.ml b/tests/spec/expr_to_term.ml
index 450dd0d0235313762e4a527d5b891776c1db0566..0e05b84eb593d2bf9a9c3c061a469d8096ae6054 100644
--- a/tests/spec/expr_to_term.ml
+++ b/tests/spec/expr_to_term.ml
@@ -24,6 +24,21 @@ let check_expr_term check fct s post =
let post = Logic_const.new_predicate app in
Annotations.add_ensures emitter fct [Normal,post]
+let check_expr_pred fct s post =
+ let exp =
+ match s.skind with
+ | Instr (Call(_,_,[x],_)) -> x
+ | _ -> Kernel.fatal "Unexpected statement %a" Printer.pp_stmt s
+ in
+ let pred = (snd post).ip_content.tp_statement in
+ let pred' = Logic_utils.expr_to_predicate exp in
+ if not (Logic_utils.is_same_predicate pred pred') then
+ Kernel.fatal
+ "translation of C expression %a is %a, inconsistent with predicate %a"
+ Printer.pp_exp exp Printer.pp_predicate pred' Printer.pp_predicate pred;
+ let post = Logic_const.new_predicate pred' in
+ Annotations.add_ensures emitter fct [Normal,post]
+
let treat_fct check fct =
let stmts = (Kernel_function.get_definition fct).sbody.bstmts in
let stmts =
@@ -47,16 +62,31 @@ let treat_fct check fct =
List.iter2 (check_expr_term check fct) stmts ensures;
Filecheck.check_ast "check_expr_to_term"
+let treat_fct_pred fct =
+ let stmts = (Kernel_function.get_definition fct).sbody.bstmts in
+ let stmts =
+ List.filter
+ (fun x -> match x.skind with Instr(Call _) -> true | _ -> false)
+ stmts
+ in
+ let ensures = (List.hd (Annotations.funspec fct).spec_behavior).b_post_cond in
+ if List.length stmts <> List.length ensures then
+ Kernel.fatal "ill-formed test in function %a" Kernel_function.pretty fct;
+ List.iter2 (check_expr_pred fct) stmts ensures;
+ Filecheck.check_ast "check_expr_to_predicate"
+
let compute () =
let main = Globals.Functions.find_by_name "main" in
let f = Globals.Functions.find_by_name "f" in
let g = Globals.Functions.find_by_name "g" in
let h = Globals.Functions.find_by_name "h" in
+ let i = Globals.Functions.find_by_name "i" in
begin
treat_fct true main;
treat_fct false f;
treat_fct true g;
treat_fct true h;
+ treat_fct_pred i;
end
let () = Db.Main.extend compute
diff --git a/tests/spec/oracle/expr_to_term.res.oracle b/tests/spec/oracle/expr_to_term.res.oracle
index fcb612aeeffb7d9c85f1f1ab6724eb0bb42c00e0..3fb984d4c75c4d378aaca08459b24b1229bbaef0 100644
--- a/tests/spec/oracle/expr_to_term.res.oracle
+++ b/tests/spec/oracle/expr_to_term.res.oracle
@@ -76,4 +76,25 @@ int h(void)
return_label: return __retres;
}
+void expr_to_predicate(int x_0)
+{
+ return;
+}
+
+int z;
+/*@ ensures (int)(t | 5) ≢ 0;
+ ensures ¬(z < 5);
+ ensures z ≢ 0 ∧ t ≢ 0;
+ ensures z ≢ 0 ∧ t ≢ 0;
+ ensures ¬(z < 5);
+ ensures (int)(t | 5) ≢ 0;
+ */
+void i(void)
+{
+ expr_to_predicate((z && t) != 0);
+ expr_to_predicate(! (z < 5));
+ expr_to_predicate(t | 5);
+ return;
+}
+