From 1c7acc37c44f914f60a27164b2bacb4e099db049 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 25 Mar 2020 16:10:05 +0100
Subject: [PATCH] [wp] upgrade float literals wrt Why3 api
---
src/plugins/wp/ProverWhy3.ml | 52 ++++++++++---------
.../wp_acsl/oracle/float_const.res.oracle | 18 +++----
.../frama_c_hashtbl_solved.res.oracle | 4 +-
3 files changed, 38 insertions(+), 36 deletions(-)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 520183929b0..bb567fd2468 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -236,51 +236,55 @@ let rec of_tau ~cnv (t:Lang.F.tau) =
| Record _ ->
why3_failure "Type %a not (yet) convertible" Lang.F.pp_tau t
-module Literal = struct
+module Literal =
+struct
+
+ open Why3
+
let const_int (z:Z.t) =
- Why3.(Term.t_const Constant.(const_of_big_int (BigInt.of_string (Z.to_string z)))) Why3.Ty.ty_int
+ let k = BigInt.of_string (Z.to_string z) in
+ Term.t_const (Constant.int_const k) Ty.ty_int
- let why3_real ty ~use_hex sign integer decimal exp =
- let rc = Why3.Number.ConstReal {
- rc_negative = sign ;
- rc_abs =
- if use_hex then Why3.Number.real_const_hex integer decimal exp
- else Why3.Number.real_const_dec integer decimal exp
- } in
- Why3.Term.t_const rc ty
+ let why3_real ty ~radix ~neg ~int ?(frac="") ?exp () =
+ let rc = Number.real_literal ~radix ~neg ~int ~frac ~exp in
+ Term.t_const (Constant.ConstReal rc) ty
let const_real ~cnv (q:Q.t) =
let mk_real_int z =
- let use_hex = false in
- let str = Z.to_string (Z.abs z) in
- why3_real Why3.Ty.ty_real ~use_hex (Z.sign z < 0) str "" None
+ let neg = Z.sign z < 0 in
+ let int = Z.to_string (Z.abs z) in
+ why3_real Why3.Ty.ty_real ~radix:10 ~neg ~int ()
in
if Z.equal Z.one q.den
then mk_real_int q.num
else
- t_app ~cnv ~f:["real"] ~l:"Real" ~p:["infix /"] [mk_real_int q.num;mk_real_int q.den]
+ t_app ~cnv ~f:["real"] ~l:"Real" ~p:["infix /"]
+ [mk_real_int q.num;mk_real_int q.den]
let cfloat_of_tau tau =
if Lang.F.Tau.equal tau Cfloat.t32 then Ctypes.Float32
else if Lang.F.Tau.equal tau Cfloat.t64 then Ctypes.Float64
else raise Not_found
+ let re_float = Str.regexp
+ "-?0x\\([0-9a-f]+\\).\\([0-9a-f]+\\)?0*p?\\([+-]?[0-9a-f]+\\)?$"
+
let float_literal_from_q ~cnv tau q =
let use_hex = true in
+ let qf = Q.to_float q in
let f = match cfloat_of_tau tau with
- | Float32 -> Floating_point.round_to_single_precision_float (Q.to_float q)
- | Float64 -> Q.to_float q
- in
- let s = Format.asprintf "%a" (Floating_point.pretty_normal ~use_hex) f in
- let re_float =
- Str.regexp "-?0x\\([0-9a-f]+\\).\\([0-9a-f]+\\)?p?\\([+-]?[0-9a-f]+\\)?$"
+ | Float32 -> Floating_point.round_to_single_precision_float qf
+ | Float64 -> qf
in
+ let s = Pretty_utils.to_string (Floating_point.pretty_normal ~use_hex) f in
+ let s = String.lowercase_ascii s in
if Str.string_match re_float s 0 then
let group n r = try Str.matched_group n r with Not_found -> "" in
- let (i,d,e) = (group 1 s), (group 2 s), (group 3 s) in
- let e = if String.equal e "" then None else Some e in
- let t = Extlib.the (of_tau ~cnv tau) in
- why3_real t ~use_hex (Q.sign q < 0) i d e
+ let neg = Q.sign q < 0 in
+ let int,frac,exp = (group 1 s), (group 2 s), (group 3 s) in
+ let exp = if String.equal exp "" then None else Some exp in
+ let ty = Extlib.the (of_tau ~cnv tau) in
+ why3_real ty ~radix:16 ~neg ~int ~frac ?exp ()
else raise Not_found
let const_float ~cnv tau (repr:Lang.F.QED.repr) =
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle
index 36c2f74c363..d1a648f8189 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/float_const.res.oracle
@@ -37,7 +37,7 @@
goal wp_goal :
forall f:t.
let r = of_f32 (to_f32 (of_f64 f)) in
- eq_f64 f (0x1.999999999999ap-4:t) -> of_f64 (to_f64 r) = r
+ eq_f64 f (0x1.999999999999Ap-4:t) -> of_f64 (to_f64 r) = r
end
[wp:print-generated]
theory WP1
@@ -67,7 +67,7 @@
goal wp_goal :
forall f:t.
- eq_f64 f (0x1.999999999999ap-4:t) ->
+ eq_f64 f (0x1.999999999999Ap-4:t) ->
not of_f64 f = (13421773.0 / 134217728.0)
end
[wp:print-generated]
@@ -98,7 +98,7 @@
goal wp_goal :
forall f:t.
- eq_f64 f (0x1.999999999999ap-4:t) ->
+ eq_f64 f (0x1.999999999999Ap-4:t) ->
of_f64 f = (3602879701896397.0 / 36028797018963968.0)
end
[wp:print-generated]
@@ -129,7 +129,7 @@
goal wp_goal :
forall f:t.
- eq_f64 f (0x1.999999999999ap-4:t) -> not of_f64 f = (1.0 / 10.0)
+ eq_f64 f (0x1.999999999999Ap-4:t) -> not of_f64 f = (1.0 / 10.0)
end
[wp:print-generated]
theory WP4
@@ -160,7 +160,7 @@
goal wp_goal :
forall f:t1.
let r = of_f321 f in
- eq_f32 f (0x1.99999a0000000p-4:t1) ->
+ eq_f32 f (0x1.99999Ap-4:t1) ->
of_f321 (to_f321 (of_f641 (to_f641 r))) = r
end
[wp:print-generated]
@@ -191,7 +191,7 @@
goal wp_goal :
forall f:t1.
- eq_f32 f (0x1.99999a0000000p-4:t1) ->
+ eq_f32 f (0x1.99999Ap-4:t1) ->
not of_f321 f = (3602879701896397.0 /' 36028797018963968.0)
end
[wp:print-generated]
@@ -222,8 +222,7 @@
goal wp_goal :
forall f:t1.
- eq_f32 f (0x1.99999a0000000p-4:t1) ->
- of_f321 f = (13421773.0 /' 134217728.0)
+ eq_f32 f (0x1.99999Ap-4:t1) -> of_f321 f = (13421773.0 /' 134217728.0)
end
[wp:print-generated]
theory WP7
@@ -252,8 +251,7 @@
(* use frama_c_wp.cfloat.Cfloat1 *)
goal wp_goal :
- forall f:t1.
- eq_f32 f (0x1.99999a0000000p-4:t1) -> not of_f321 f = (1.0 /' 10.0)
+ forall f:t1. eq_f32 f (0x1.99999Ap-4:t1) -> not of_f321 f = (1.0 /' 10.0)
end
[wp] 8 goals generated
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
index edd11a46ad8..6e3fc54c35c 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
@@ -109,7 +109,7 @@
[wp] [Qed] Goal typed_size_assigns : Valid
[wp] Proved goals: 102 / 102
Qed: 69
- Script: 1
+ Script: 1
Alt-Ergo: 32
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
@@ -273,7 +273,7 @@
[wp] [Qed] Goal typed_size_assigns : Valid
[wp] Proved goals: 74 / 143
Qed: 16
- Script: 1
+ Script: 1
Alt-Ergo: 57
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
--
GitLab