diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 7eb80e74d5a03dbb1bf3bb1771ae9c88a7adc34e..e287cf0048d750ab14e40fc7920d047f348ebbcf 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -5290,8 +5290,10 @@ let constFoldVisitor (machdep: bool) = new constFoldVisitorClass machdep
let rec constFoldTermNodeAtTop = function
| TSizeOf typ as t ->
- (try integer_lconstant (bytesSizeOf typ)
- with SizeOfError _ -> t)
+ begin
+ try integer_lconstant (bytesSizeOf typ)
+ with SizeOfError _ -> t
+ end
| TSizeOfStr str -> integer_lconstant (String.length str + 1)
| TAlignOf typ as t ->
begin
@@ -5304,14 +5306,68 @@ let rec constFoldTermNodeAtTop = function
| TSizeOfE _ | TAlignOfE _ ->
assert false (* sizeof/alignof of logic types are rejected
by typing anyway. *)
+ | TUnOp (op, ({ term_node = n1 } as t1)) ->
+ begin
+ let constFoldTermUnOp int_unop =
+ match constFoldTermNodeAtTop n1 with
+ | TConst (Integer (i, _)) -> TConst (Integer (int_unop i, None))
+ | n1 -> TUnOp (op, {t1 with term_node = n1})
+ in
+ match op with
+ | Neg -> constFoldTermUnOp Integer.neg
+ | BNot -> constFoldTermUnOp Integer.lognot
+ | LNot -> constFoldTermUnOp
+ (fun i -> if Integer.is_zero i
+ then Integer.one else Integer.zero)
+ end
+ | TBinOp (op, ({term_node = n1} as t1), ({term_node = n2} as t2)) ->
+ begin
+ let n1 = constFoldTermNodeAtTop n1 in
+ let n2 = constFoldTermNodeAtTop n2 in
+ let constFoldTermBinOp int_bop =
+ match n1, n2 with
+ | TConst (Integer (i1, _)), TConst (Integer (i2, _)) ->
+ TConst (Integer (int_bop i1 i2, None))
+ | n1, n2 ->
+ TBinOp (op, {t1 with term_node = n1}, {t2 with term_node = n2})
+
+ in
+ match op with
+ | PlusA -> constFoldTermBinOp Integer.add
+ | MinusA -> constFoldTermBinOp Integer.sub
+ | Mult -> constFoldTermBinOp Integer.mul
+ | Shiftlt -> constFoldTermBinOp Integer.shift_left
+ | Shiftrt -> (* right-shifting Lintegers is always arithmetic *)
+ constFoldTermBinOp Integer.shift_right
+ | BAnd -> constFoldTermBinOp Integer.logand
+ | BXor -> constFoldTermBinOp Integer.logxor
+ | BOr -> constFoldTermBinOp Integer.logor
+ | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr ->
+ let bool_op = match op with
+ | Lt -> Integer.lt
+ | Gt -> Integer.gt
+ | Le -> Integer.le
+ | Ge -> Integer.ge
+ | Eq -> Integer.equal
+ | Ne -> (fun i1 i2 -> not (Integer.equal i1 i2))
+ | LAnd ->
+ (fun i1 i2 -> not (Integer.is_zero i1) && not (Integer.is_zero i2))
+ | LOr ->
+ (fun i1 i2 -> not (Integer.is_zero i1) || not (Integer.is_zero i2))
+ | _ -> assert false
+ in
+ constFoldTermBinOp
+ (fun i1 i2 -> if bool_op i1 i2 then Integer.one else Integer.zero)
+ | _ ->
+ TBinOp (op, {t1 with term_node = n1}, {t2 with term_node = n2})
+ end
| t -> t
-let constFoldTerm machdep t =
+let constFoldTerm t =
let visitor = object
inherit nopCilVisitor
method! vterm_node t =
- if machdep then ChangeToPost (t,constFoldTermNodeAtTop)
- else DoChildren
+ ChangeToPost (t, constFoldTermNodeAtTop)
end
in
visitCilTerm visitor t
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index aed2f84c7513a397e2e64affce3de2af76c96ac6..ca938f4a42d4e4e7db53f65ac8393fe5f3facc5e 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1079,10 +1079,9 @@ val constFoldToInt: ?machdep:bool -> exp -> Integer.t option
val constFoldTermNodeAtTop: term_node -> term_node
(** Do constant folding on an term.
- If the first argument is true then
- will also compute compiler-dependent expressions such as [sizeof]
- and [alignof]. *)
-val constFoldTerm: bool -> term -> term
+ @before Frama-C+Dev takes a boolean [machdep] to decide if we actually do
+ the fold or not. *)
+val constFoldTerm: term -> term
(** Do constant folding on a {!Cil_types.offset}. If the second argument is true
then will also compute compiler-dependent expressions such as [sizeof]. *)
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 73ffd560c652f480073875c191ca29376bd6748a..d6c1c106a215b6873d4e92e6f5d29e4a63a84b43 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -263,8 +263,8 @@ let isCrossableAtInit tr func =
end
in
let eval_rel_at_init rel t1 t2 =
- let t1 = eval_term_at_init (Cil.constFoldTerm true t1) in
- let t2 = eval_term_at_init (Cil.constFoldTerm true t2) in
+ let t1 = eval_term_at_init (Cil.constFoldTerm t1) in
+ let t2 = eval_term_at_init (Cil.constFoldTerm t2) in
let comp =
match rel with
| Req -> ((=) 0)
diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml
index 47b4dd0ae16239aa763f316bceb53747d7b6f635..b661c99d40603029704486f60a2649440de460ee 100644
--- a/src/plugins/eva/legacy/eval_terms.ml
+++ b/src/plugins/eva/legacy/eval_terms.ml
@@ -1198,7 +1198,7 @@ let rec eval_term ~alarm_mode env t =
tcond ttrue tfalse
| TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _ | TAlignOfE _ ->
- let e = Cil.constFoldTerm true t in
+ let e = Cil.constFoldTerm t in
let v = match e.term_node with
| TConst (Integer (v, _)) -> Cvalue.V.inject_int v
| _ -> V.top_int
diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index 828bb2ab9a59650de96a6c913ed358ec51e5f60c..eb5550382a16e41c745b25763a32a690c7147d6b 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -65,7 +65,7 @@ and constant_exp e =
| _ -> Warning.error "constant(%a)" Printer.pp_exp e
and constant_term t =
- let e = Cil.constFoldTerm true t in
+ let e = Cil.constFoldTerm t in
match e.term_node with
| TConst c -> logic_constant c
| _ -> Warning.error "constant(%a)" Printer.pp_term t
diff --git a/tests/spec/const_fold_term.i b/tests/spec/const_fold_term.i
new file mode 100644
index 0000000000000000000000000000000000000000..dcabf3bd580cb2b7f73e8026240336341dd6388b
--- /dev/null
+++ b/tests/spec/const_fold_term.i
@@ -0,0 +1,22 @@
+/* run.config
+ MODULE: @PTEST_NAME@
+ STDOPT: -print
+*/
+
+void unop(int a) {
+ //@ assert -(21 + 21);
+ //@ assert ~21;
+ //@ assert -a;
+}
+
+void binop(int a) {
+ //@ assert 21 + 21 + a == 42;
+ //@ assert 84 - 42 == 42;
+ //@ assert 6 * 7 == 42;
+ //@ assert 21 << 1 == 42;
+ //@ assert 672 >> sizeof(int) == 42;
+ //@ assert (58 & 47) == 42;
+ //@ assert (34 | sizeof("frama-c")) == 42;
+ //@ assert (63 ^ 21) == 42;
+ //@ assert 168 / sizeof(a) == 42;
+}
diff --git a/tests/spec/const_fold_term.ml b/tests/spec/const_fold_term.ml
new file mode 100644
index 0000000000000000000000000000000000000000..fe52ad8ac04840bd99a60ada938da688e40078e5
--- /dev/null
+++ b/tests/spec/const_fold_term.ml
@@ -0,0 +1,51 @@
+open Cil_types
+
+let fold t =
+ match t.term_node with
+ | TSizeOf _ | TSizeOfStr _ | TSizeOfE _ | TAlignOf _ | TAlignOfE _
+ | TUnOp _ | TBinOp _ ->
+ let t' = Cil.constFoldTerm t in
+ Format.printf " %a folds to %a@." Cil_printer.pp_term t Cil_printer.pp_term t'
+ | _ -> ()
+
+class visitTerm prj = object(_)
+ inherit Visitor.frama_c_copy prj
+
+ method! vterm t =
+ fold t;
+ Cil.JustCopy
+
+end
+
+let test_terms () =
+ let open Cil_builder.Exp in
+ let loc = Cil_datatype.Location.unknown in
+ let e1 = lognot ((of_int 21) + (of_int 21)) in
+ let e2 = lognot ((of_int 21) - (of_int 21)) in
+ let e3 = lt zero (logand (of_int 42) (of_int 21)) in
+ let e4 = gt one (logor zero (of_int 21)) in
+ let e5 = ne zero (le zero (logand (of_int 42) (of_int 21))) in
+ let e6 = eq one (ge one (logor one zero)) in
+ let t1 = cil_term ~loc e1 in
+ let t2 = cil_term ~loc e2 in
+ let t3 = cil_term ~loc e3 in
+ let t4 = cil_term ~loc e4 in
+ let t5 = cil_term ~loc e5 in
+ let t6 = cil_term ~loc e6 in
+ Format.printf "Custom terms :@.";
+ fold t1;
+ fold t2;
+ fold t3;
+ fold t4;
+ fold t5;
+ fold t6
+
+let startup () =
+ test_terms ();
+ Format.printf "File terms :@.";
+ let prj = File.create_project_from_visitor "test_const_fold"
+ (fun prj -> new visitTerm prj)
+ in
+ Project.set_current prj
+
+let () = Boot.Main.extend startup
diff --git a/tests/spec/oracle/const_fold_term.res.oracle b/tests/spec/oracle/const_fold_term.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..61d1b054b90db6295840d234120d6fe05db78d81
--- /dev/null
+++ b/tests/spec/oracle/const_fold_term.res.oracle
@@ -0,0 +1,21 @@
+[kernel] Parsing const_fold_term.i (no preprocessing)
+Custom terms :
+ !(21 + 21) folds to 0
+ !(21 - 21) folds to 1
+ 0 < (42 ∧ 21) folds to 1
+ 1 > (0 ∨ 21) folds to 0
+ 0 ≢ (0 ≤ (42 ∧ 21)) folds to 1
+ 1 ≡ (1 ≥ (1 ∨ 0)) folds to 1
+File terms :
+ -(21 + 21) folds to -42
+ ~21 folds to -22
+ -a folds to -a
+ (21 + 21) + a folds to 42 + a
+ 84 - 42 folds to 42
+ 6 * 7 folds to 42
+ 21 << 1 folds to 42
+ 672 >> sizeof(int) folds to 42
+ 58 & 47 folds to 42
+ 34 | sizeof("frama-c") folds to 42
+ 63 ^ 21 folds to 42
+ 168 / sizeof(a) folds to 168 / 4