From 65e0e5779aea9e529c436466a995269f97375674 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 2 Mar 2020 17:12:39 +0100
Subject: [PATCH] [constfold] constfold unary - on float
also minor refactoring of smart constructor for float constants
---
src/kernel_services/ast_queries/cil.ml | 91 +++++++++++--------
tests/syntax/compile_constant.c | 4 +
.../syntax/oracle/compile_constant.res.oracle | 2 +
3 files changed, 57 insertions(+), 40 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 6db513bc25a..d792b7e40ff 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -3051,7 +3051,16 @@ let integer_constant i = CInt64(Integer.of_int i, IInt, None)
(* Construct an integer. Use only for values that fit on 31 bits *)
let integer ~loc (i: int) = new_exp ~loc (Const (integer_constant i))
-let kfloat ~loc k f = new_exp ~loc (Const (CReal(f,k,None)))
+let kfloat ~loc k f =
+ let is_single_precision =
+ match k with FFloat -> true | FDouble | FLongDouble -> false
+ in
+ let f =
+ if is_single_precision then
+ Floating_point.round_to_single_precision_float f
+ else f
+ in
+ new_exp ~loc (Const (CReal(f,k,None)))
let zero ~loc = integer ~loc 0
let one ~loc = integer ~loc 1
@@ -4407,29 +4416,43 @@ and constFold (machdep: bool) (e: exp) : exp =
let loc = e.eloc in
match e.enode with
BinOp(bop, e1, e2, tres) -> constFoldBinOp ~loc machdep bop e1 e2 tres
- | UnOp(unop, e1, tres) -> begin
- try
- let tk =
- match unrollTypeSkel tres with
- | TInt(ik, _) -> ik
- | TEnum (ei,_) -> ei.ekind
- | _ -> raise Not_found (* probably a float *)
- in
- let e1c = constFold machdep e1 in
- match e1c.enode with
- Const(CInt64(i,_ik,repr)) -> begin
- match unop with
- Neg ->
- let repr = Extlib.opt_map (fun s -> "-" ^ s) repr in
- kinteger64 ~loc ?repr ~kind:tk (Integer.neg i)
- | BNot -> kinteger64 ~loc ~kind:tk (Integer.lognot i)
- | LNot ->
- if Integer.equal i Integer.zero then one ~loc
- else zero ~loc
- end
- | _ -> if e1 == e1c then e else new_exp ~loc (UnOp(unop, e1c, tres))
- with Not_found -> e
+ | UnOp(unop, e1, tres) when isIntegralType tres -> begin
+ let tk =
+ match unrollTypeSkel tres with
+ | TInt(ik, _) -> ik
+ | TEnum (ei,_) -> ei.ekind
+ | _ -> assert false (* tres is an integral type *)
+ in
+ let e1c = constFold machdep e1 in
+ match e1c.enode with
+ Const(CInt64(i,_ik,repr)) -> begin
+ match unop with
+ Neg ->
+ let repr = Extlib.opt_map (fun s -> "-" ^ s) repr in
+ kinteger64 ~loc ?repr ~kind:tk (Integer.neg i)
+ | BNot -> kinteger64 ~loc ~kind:tk (Integer.lognot i)
+ | LNot ->
+ if Integer.equal i Integer.zero then one ~loc
+ else zero ~loc
+ end
+ | _ -> if e1 == e1c then e else new_exp ~loc (UnOp(unop, e1c, tres))
end
+ | UnOp(unop, e1, tres) when isArithmeticType tres -> begin
+ let tk =
+ match unrollTypeSkel tres with
+ | TFloat(fk,_) -> fk
+ | _ -> assert false (*tres is arithmetic but not integral, i.e. Float *)
+ in
+ let e1c = constFold machdep e1 in
+ match e1c.enode with
+ | Const (CReal(f,_,_)) -> begin
+ match unop with
+ | Neg -> kfloat ~loc tk (-. f)
+ | _ -> if e1 == e1c then e else new_exp ~loc (UnOp(unop,e1c,tres))
+ end
+ | _ -> if e1 == e1c then e else new_exp ~loc (UnOp(unop,e1c,tres))
+ end
+ | UnOp _ -> e
(* Characters are integers *)
| Const(CChr c) -> new_exp ~loc (Const(charConstToIntConstant c))
| Const(CEnum {eival = v}) -> constFold machdep v
@@ -4706,28 +4729,16 @@ and constFoldBinOp ~loc (machdep: bool) bop e1 e2 tres =
| TFloat(fk,_) -> fk
| _ -> Kernel.fatal "constFoldBinOp: not a floating type"
in
- let is_single_precision =
- match tk with
- | FFloat -> true
- | FDouble | FLongDouble -> false
- in
- let mkFloat f =
- let f =
- if is_single_precision then
- Floating_point.round_to_single_precision_float f
- else f
- in
- new_exp ~loc (Const (CReal(f,tk,None)))
- in
match bop, e1'.enode, e2'.enode with
| PlusA, Const(CReal(f1,fk1,_)), Const(CReal(f2,fk2,_)) when fk1 = fk2 ->
- mkFloat (f1 +. f2)
+ kfloat ~loc tk (f1 +. f2)
| MinusA, Const(CReal(f1,fk1,_)), Const(CReal(f2,fk2,_)) when fk1 = fk2 ->
- mkFloat (f1 -. f2)
+ kfloat ~loc tk (f1 -. f2)
| Mult, Const(CReal(f1,fk1,_)), Const(CReal(f2,fk2,_)) when fk1 = fk2 ->
- mkFloat (f1 *. f2)
+ kfloat ~loc tk (f1 *. f2)
| Div, Const(CReal(f1,fk1,_)), Const(CReal(f2,fk2,_)) when fk1 = fk2 ->
- mkFloat (f1 /. f2) (*might be infinity or NaN, but that's still a float*)
+ (*might be infinity or NaN, but that's still a float*)
+ kfloat ~loc tk (f1 /. f2)
| _ -> new_exp ~loc (BinOp(bop,e1',e2',tres))
end else
new_exp ~loc (BinOp(bop, e1', e2', tres))
diff --git a/tests/syntax/compile_constant.c b/tests/syntax/compile_constant.c
index dc2acdcdd52..2570c1a0849 100644
--- a/tests/syntax/compile_constant.c
+++ b/tests/syntax/compile_constant.c
@@ -1,2 +1,6 @@
#define M0(x) (x)*(x)<4.0?0.0:1.0
char pixels[] = {M0(0.0), M0(1), M0(2.0f)};
+
+char test_neg = { (-0.) ? 1. : 2. };
+
+char test_ge = { ((-1.) >= 0.) ? 1. : 2. };
diff --git a/tests/syntax/oracle/compile_constant.res.oracle b/tests/syntax/oracle/compile_constant.res.oracle
index d5b6a340f31..f0dc821e08e 100644
--- a/tests/syntax/oracle/compile_constant.res.oracle
+++ b/tests/syntax/oracle/compile_constant.res.oracle
@@ -1,4 +1,6 @@
[kernel] Parsing tests/syntax/compile_constant.c (with preprocessing)
/* Generated by Frama-C */
char pixels[3] = {(char)0.0, (char)0.0, (char)1.0};
+char test_neg = (char)2.;
+char test_ge = (char)2.;
--
GitLab