From 1ef9a31273896d02084875f6933ebdc417ef9330 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 20 Apr 2023 10:48:34 +0200
Subject: [PATCH] [aorai] floating-point automata should use +real WP model
---
src/plugins/aorai/aorai_utils.ml | 19 +++++++++++++++++--
src/plugins/aorai/tests/Aorai_test.ml | 1 +
.../aorai/tests/ya/oracle/floats.res.oracle | 2 +-
.../tests/ya/oracle_prove/floats.res.oracle | 8 --------
4 files changed, 19 insertions(+), 11 deletions(-)
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 62e84f90c70..7ce1e025fb6 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -399,8 +399,14 @@ let rec term_to_exp t res =
| TConst (LWStr l) -> new_exp ~loc (Const (CWStr l))
| TConst (LChr c) -> new_exp ~loc (Const (CChr c))
| TConst (LReal l_real) ->
- (* r_nearest is by definition in double precision. *)
- new_exp ~loc (Const (CReal (l_real.r_nearest, FDouble, None)))
+ let fk,_ = Floating_point.parse l_real.r_literal in
+ let cst =
+ if Cil.isExactFloat fk l_real then
+ (CReal (l_real.r_nearest, fk, Some l_real.r_literal))
+ else (* fallback to double, r_nearest being in that format anyways *)
+ (CReal (l_real.r_nearest, FDouble, None))
+ in
+ new_exp ~loc (Const cst)
| TConst (LEnum e) -> new_exp ~loc (Const (CEnum e))
| TLval tlval -> new_exp ~loc (Lval (tlval_to_lval tlval res))
| TSizeOf ty -> new_exp ~loc (SizeOf ty)
@@ -413,6 +419,15 @@ let rec term_to_exp t res =
| TBinOp (binop, t1, t2)->
new_exp ~loc
(BinOp(binop, term_to_exp t1 res, term_to_exp t2 res, Cil.intType))
+ | TCastE(ty, { term_node = TConst(LReal lreal) })
+ when Cil.isArithmeticType ty && not (Cil.isIntegralType ty) ->
+ (match Cil.unrollType ty with
+ | TFloat(fk,_) ->
+ new_exp ~loc
+ (Const (CReal (lreal.r_nearest,fk,Some lreal.r_literal)))
+ | _ ->
+ Aorai_option.fatal
+ "A floating-point type was expected, got %a." Printer.pp_typ ty)
| TCastE (ty, t) -> new_exp ~loc (CastE (ty, term_to_exp t res))
| TAddrOf tlval -> new_exp ~loc (AddrOf (tlval_to_lval tlval res))
| TStartOf tlval -> new_exp ~loc (StartOf (tlval_to_lval tlval res))
diff --git a/src/plugins/aorai/tests/Aorai_test.ml b/src/plugins/aorai/tests/Aorai_test.ml
index f65b5d988b1..5cd54943e86 100644
--- a/src/plugins/aorai/tests/Aorai_test.ml
+++ b/src/plugins/aorai/tests/Aorai_test.ml
@@ -124,6 +124,7 @@ let extend () =
Wp.Wp_parameters.SplitBranch.on();
Wp.Wp_parameters.SplitConj.on();
Wp.Wp_parameters.SplitMax.set 32;
+ Wp.Wp_parameters.Model.As_string.set "+real";
if not (Wp.Wp_parameters.Verbose.is_set()) then
Wp.Wp_parameters.Verbose.set 0;
Globals.Functions.iter check_auto_func;
diff --git a/src/plugins/aorai/tests/ya/oracle/floats.res.oracle b/src/plugins/aorai/tests/ya/oracle/floats.res.oracle
index a614ddfed92..a5a1b263a40 100644
--- a/src/plugins/aorai/tests/ya/oracle/floats.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/floats.res.oracle
@@ -176,7 +176,7 @@ check lemma B_deterministic_trans{L}:
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_square_root_aux;
if ((unsigned int)1 == aorai_CurStates)
- if (x >= 1.f)
+ if (x >= 1.0f)
if (x <= n) aorai_CurStates = B; else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
else aorai_CurStates = aorai_reject;
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/floats.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/floats.res.oracle
index 1da703e983a..28b4a5aa186 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/floats.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/floats.res.oracle
@@ -85,11 +85,3 @@
----------------------------------------------------------------------------
[kernel] Parsing TMPDIR/aorai_floats_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
-[aorai-test] Warning: Could not prove ensures
- aorai_CurStates ≡ B in automaton function square_root_aux_pre_func
-[aorai-test] Warning: Could not prove ensures
- aorai_CurStates ≡ B in automaton function square_root_aux_pre_func
-[aorai-test] Warning: Could not prove ensures
- aorai_CurStates ≢ aorai_reject in automaton function square_root_aux_pre_func
-[aorai-test] Warning: Could not prove ensures
- aorai_CurStates ≢ aorai_reject in automaton function square_root_aux_pre_func
--
GitLab