From c0239b8a61fdcce3aa26a863b024053819832468 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Mon, 15 Apr 2024 14:19:52 +0200
Subject: [PATCH] [Cil] Keep folded sub-terms
---
src/kernel_services/ast_queries/cil.ml | 19 ++++++++++++-------
1 file changed, 12 insertions(+), 7 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index da1da6f3bd0..21881ba48f9 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -5310,12 +5310,12 @@ let rec constFoldTermNodeAtTop = function
| TSizeOfE _ | TAlignOfE _ ->
assert false (* sizeof/alignof of logic types are rejected
by typing anyway. *)
- | TUnOp (op, { term_node = t1 }) as t ->
+ | TUnOp (op, ({ term_node = n1 } as t1)) ->
begin
let constFoldTermUnOp int_unop =
- match constFoldTermNodeAtTop t1 with
+ match constFoldTermNodeAtTop n1 with
| TConst (Integer (i, _)) -> TConst (Integer (int_unop i, None))
- | _ -> t
+ | n1 -> TUnOp (op, {t1 with term_node = n1})
in
match op with
| Neg -> constFoldTermUnOp Integer.neg
@@ -5324,13 +5324,17 @@ let rec constFoldTermNodeAtTop = function
(fun i -> if Integer.is_zero i
then Integer.one else Integer.zero)
end
- | TBinOp (op, {term_node = t1}, {term_node = t2}) as t ->
+ | 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 constFoldTermNodeAtTop t1, constFoldTermNodeAtTop t2 with
+ match n1, n2 with
| TConst (Integer (i1, _)), TConst (Integer (i2, _)) ->
TConst (Integer (int_bop i1 i2, None))
- | _ -> t
+ | n1, n2 ->
+ TBinOp (op, {t1 with term_node = n1}, {t2 with term_node = n2})
+
in
match op with
| PlusA -> constFoldTermBinOp Integer.add
@@ -5342,7 +5346,8 @@ let rec constFoldTermNodeAtTop = function
| BAnd -> constFoldTermBinOp Integer.logand
| BXor -> constFoldTermBinOp Integer.logxor
| BOr -> constFoldTermBinOp Integer.logor
- | _ -> t
+ | _ ->
+ TBinOp (op, {t1 with term_node = n1}, {t2 with term_node = n2})
end
| t -> t
--
GitLab