From b1355b8bea80908eb3708f4c7524ed2a4c4825b7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 26 Mar 2020 18:18:42 +0100
Subject: [PATCH] [wp] support for float builtins
---
src/plugins/wp/Cfloat.ml | 42 ++++++++++++++++++++++++++--------------
1 file changed, 28 insertions(+), 14 deletions(-)
diff --git a/src/plugins/wp/Cfloat.ml b/src/plugins/wp/Cfloat.ml
index 24d629f9c2c..64e1cfd7065 100644
--- a/src/plugins/wp/Cfloat.ml
+++ b/src/plugins/wp/Cfloat.ml
@@ -360,31 +360,45 @@ let flt_div ft = Compute.get (Context.get model, ft, DIV) |> fst
let flt_of_real ft = Compute.get (Context.get model, ft, ROUND) |> fst
let real_of_flt ft = Compute.get (Context.get model, ft, REAL) |> fst
-
(* -------------------------------------------------------------------------- *)
(* --- Builtins --- *)
(* -------------------------------------------------------------------------- *)
-let make_hack ?(converse=false) ft op xs =
+let builtin kind ft op xs =
let phi, impl = Compute.get ((Context.get model), ft, op) in
- let xs = (if converse then List.rev xs else xs) in
- try impl xs with Not_found -> F.e_fun ~result:Logic.Bool phi xs
-
-let register_builtin ft =
+ let xs = (if kind=`ReV then List.rev xs else xs) in
+ try impl xs with Not_found ->
+ let result = match kind with
+ | `Binop | `Unop -> ftau ft
+ | `Rel | `ReV -> Logic.Bool
+ in F.e_fun ~result phi xs
+
+let register_builtins ft =
begin
let suffix = float_name ft in
- LogicBuiltins.hack ("\\eq_" ^ suffix) (make_hack ft EQ) ;
- LogicBuiltins.hack ("\\ne_" ^ suffix) (make_hack ft NE) ;
- LogicBuiltins.hack ("\\lt_" ^ suffix) (make_hack ~converse:false ft LT) ;
- LogicBuiltins.hack ("\\gt_" ^ suffix) (make_hack ~converse:true ft LT) ;
- LogicBuiltins.hack ("\\le_" ^ suffix) (make_hack ~converse:false ft LE) ;
- LogicBuiltins.hack ("\\ge_" ^ suffix) (make_hack ~converse:true ft LE)
+ let register (prefix,kind,op) =
+ LogicBuiltins.hack
+ (Printf.sprintf "\\%s_%s" prefix suffix)
+ (builtin kind ft op)
+ in List.iter register [
+ "eq",`Rel,EQ ;
+ "ne",`Rel,NE ;
+ "lt",`Rel,LT ;
+ "gt",`ReV,LT ;
+ "le",`Rel,LE ;
+ "ge",`ReV,LE ;
+ "neg",`Unop,NEG ;
+ "add",`Binop,ADD ;
+ "sub",`Binop,SUB ;
+ "mul",`Binop,MUL ;
+ "div",`Binop,DIV ;
+ ] ;
end
let () = Context.register
begin fun () ->
- register_builtin Float32 ;
- register_builtin Float64 ;
+ register_builtins Float32 ;
+ register_builtins Float64 ;
end
(* -------------------------------------------------------------------------- *)
--
GitLab