Merge branch 'feature/wp/float-extensions' into 'master'

[wp] float extensions

See merge request frama-c/frama-c!2385

src/plugins/wp/Cfloat.ml

@@ -175,6 +175,69 @@ let code_lit ulp value original =
   | Real , _ , None -> F.e_float value
   | Real , _ , Some r -> F.e_real (parse_literal ~model:Real value r)
 
+(* -------------------------------------------------------------------------- *)
+(* --- Literal Output                                                     --- *)
+(* -------------------------------------------------------------------------- *)
+
+let printers = [
+  Printf.sprintf "%.0g" ;
+  Printf.sprintf "%.1g" ;
+  Printf.sprintf "%.2g" ;
+  Printf.sprintf "%.3g" ;
+  Printf.sprintf "%.4g" ;
+  Printf.sprintf "%.5g" ;
+  Printf.sprintf "%.6g" ;
+  Printf.sprintf "%.9g" ;
+  Printf.sprintf "%.12g" ;
+  Printf.sprintf "%.15g" ;
+  Printf.sprintf "%.18g" ;
+  Printf.sprintf "%.21g" ;
+  Printf.sprintf "%.32g" ;
+  Printf.sprintf "%.64g" ;
+]
+
+let re_int = Str.regexp "[0-9]+"
+
+let force_float r =
+  if Str.string_match re_int r 0 &&
+     Str.match_end () = String.length r
+  then (r ^ ".0") else r
+
+let float_lit ulp (q : Q.t) =
+  let v = match ulp with
+    | Float32 -> rfloat @@ Transitioning.Q.to_float q
+    | Float64 -> Transitioning.Q.to_float q in
+  let reparse ulp r =
+    match ulp with
+    | Float32 -> rfloat @@ float_of_string r
+    | Float64 -> float_of_string r
+  in
+  let rec lookup ulp v = function
+    | [] -> Pretty_utils.to_string Floating_point.pretty v
+    | pp::pps ->
+        let r = force_float @@ pp v in
+        if reparse ulp r = v then r else
+          lookup ulp v pps
+  in lookup ulp v printers
+
+(* -------------------------------------------------------------------------- *)
+(* --- Finites                                                            --- *)
+(* -------------------------------------------------------------------------- *)
+
+let fclass value _args =
+  match Context.get model with
+  | Real -> F.e_bool value
+  | Float -> raise Not_found
+
+let () = Context.register
+    begin fun () ->
+      LogicBuiltins.hack "\\is_finite"         (fclass true) ;
+      LogicBuiltins.hack "\\is_NaN"            (fclass false) ;
+      LogicBuiltins.hack "\\is_infinite"       (fclass false) ;
+      LogicBuiltins.hack "\\is_plus_infinity"  (fclass false) ;
+      LogicBuiltins.hack "\\is_minus_infinity" (fclass false) ;
+    end
+
 (* -------------------------------------------------------------------------- *)
 (* --- Computations                                                       --- *)
 (* -------------------------------------------------------------------------- *)
@@ -186,13 +249,23 @@ let rec exact e =
   | Qed.Logic.Fun( f , [ q ] ) when f == fq32 || f == fq64 -> exact q
   | _ -> raise Not_found
 
-let compute op ulp xs =
+let round ulp e =
+  match F.repr e with
+  | Qed.Logic.Fun( f , [ b ] ) ->
+      begin
+        match find f with
+        | REAL , ulp2 when ulp2 = ulp -> b
+        | _ -> qmake ulp (exact e )
+      end
+  | _ -> qmake ulp (exact e)
+
+let compute_float op ulp xs =
   match op , xs with
   | NEG , [ x ] -> qmake ulp (Q.neg (exact x))
   | ADD , [ x ; y ] -> qmake ulp (Q.add (exact x) (exact y))
   | MUL , [ x ; y ] -> qmake ulp (Q.mul (exact x) (exact y))
   | DIV , [ x ; y ] -> qmake ulp (Q.div (exact x) (exact y))
-  | ROUND , [ x ] -> qmake ulp (exact x)
+  | ROUND , [ x ] -> round ulp x
   | REAL , [ x ] -> F.e_real (exact x)
   | LE , [ x ; y ] -> F.e_bool (Q.leq (exact x) (exact y))
   | LT , [ x ; y ] -> F.e_bool (Q.lt (exact x) (exact y))
@@ -200,6 +273,24 @@ let compute op ulp xs =
   | NE , [ x ; y ] -> F.e_bool (not (Q.equal (exact x) (exact y)))
   | _ -> raise Not_found
 
+let compute_real op xs =
+  match op , xs with
+  | NEG , [ x ] -> F.e_opp x
+  | ADD , [ x ; y ] -> F.e_add x y
+  | MUL , [ x ; y ] -> F.e_mul x y
+  | DIV , [ x ; y ] -> F.e_div x y
+  | (ROUND|REAL) , [ x ] -> x
+  | LE , [ x ; y ] -> F.e_leq x y
+  | LT , [ x ; y ] -> F.e_lt x y
+  | EQ , [ x ; y ] -> F.e_eq x y
+  | NE , [ x ; y ] -> F.e_neq x y
+  | _ -> raise Not_found
+
+let compute op ulp xs =
+  match Context.get model with
+  | Real -> compute_real op xs
+  | Float -> compute_float op ulp xs
+
 (* -------------------------------------------------------------------------- *)
 (* --- Operations                                                         --- *)
 (* -------------------------------------------------------------------------- *)
@@ -250,35 +341,34 @@ let register_builtin_comparison suffix ft =
     add_builtin ("\\le_" ^ suffix) signature (flt_le ft) ;
     add_builtin ("\\gt_" ^ suffix) signature gt ;
     add_builtin ("\\ge_" ^ suffix) signature ge ;
-    Context.register
-      begin fun () ->
-        let converse phi x y = e_fun phi [y;x] in
-        Lang.F.set_builtin_2 gt (converse (flt_lt ft)) ;
-        Lang.F.set_builtin_2 ge (converse (flt_le ft)) ;
-      end
+    let converse phi x y = e_fun phi [y;x] in
+    Lang.F.set_builtin_2 gt (converse (flt_lt ft)) ;
+    Lang.F.set_builtin_2 ge (converse (flt_le ft)) ;
   end
 
 let () =
-  begin
-    register_builtin_comparison "float" Float32 ;
-    register_builtin_comparison "double" Float64 ;
-  end
+  Context.register
+    begin fun () ->
+      register_builtin_comparison "float" Float32 ;
+      register_builtin_comparison "double" Float64 ;
+    end
 
 (* -------------------------------------------------------------------------- *)
 (* --- Models                                                             --- *)
 (* -------------------------------------------------------------------------- *)
 
 let () =
-  begin
-    let open LogicBuiltins in
-    let register_builtin ft =
-      add_builtin "\\model" [F ft] (f_model ft) ;
-      add_builtin "\\delta" [F ft] (f_delta ft) ;
-      add_builtin "\\epsilon" [F ft] (f_epsilon ft) ;
-    in
-    register_builtin Float32 ;
-    register_builtin Float64 ;
-  end
+  Context.register
+    begin fun () ->
+      let open LogicBuiltins in
+      let register_builtin ft =
+        add_builtin "\\model" [F ft] (f_model ft) ;
+        add_builtin "\\delta" [F ft] (f_delta ft) ;
+        add_builtin "\\epsilon" [F ft] (f_epsilon ft) ;
+      in
+      register_builtin Float32 ;
+      register_builtin Float64 ;
+    end
 
 (* -------------------------------------------------------------------------- *)
 (* --- Conversion Symbols                                                 --- *)

src/plugins/wp/Cfloat.mli

@@ -57,6 +57,9 @@ val find : lfun -> op * c_float
 
 val code_lit : c_float -> float -> string option -> term
 val acsl_lit : Cil_types.logic_real -> term
+val float_lit : c_float -> Q.t -> string
+(** Returns a string literal in decimal notation (without suffix)
+    that reparses to the same value (when added suffix). *)
 
 val float_of_int : c_float -> unop
 val float_of_real : c_float -> unop

src/plugins/wp/GuiGoal.ml

@@ -69,6 +69,17 @@ class iformat =
       ]
   end
 
+class rformat =
+  object inherit [Plang.rformat] menu
+      ~key:"GuiGoal.rformat"
+      ~default:`Ratio
+      ~data:[
+        `Ratio , "Real" , "REAL" ;
+        `Float , "Float (32 bits)" , "F32" ;
+        `Double , "Float (64 bits)" , "F64" ;
+      ]
+  end
+
 (* -------------------------------------------------------------------------- *)
 (* --- Goal Panel                                                         --- *)
 (* -------------------------------------------------------------------------- *)
@@ -101,6 +112,7 @@ class pane (enabled : GuiConfig.enabled) =
     ~icon:`SAVE ~tooltip:"Save Script" () in
   let autofocus = new autofocus in
   let iformat = new iformat in
+  let rformat = new rformat in
   let strategies = new GuiTactic.strategies () in
   object(self)
 
@@ -113,7 +125,7 @@ class pane (enabled : GuiConfig.enabled) =
         let toolbar =
           Wbox.(toolbar
                   [ w prev ; w next ; w cancel ; w forward ;
-                    w autofocus ; w iformat ;
+                    w autofocus ; w iformat ; w rformat ;
                     w play_script ; w save_script ;
                     w ~padding:6 icon ; h ~padding:6 status ]
                   [ w help ; w delete ]) in
@@ -151,6 +163,7 @@ class pane (enabled : GuiConfig.enabled) =
         play_script#connect (fun () -> self#play_script) ;
         autofocus#connect self#autofocus ;
         iformat#connect self#iformat ;
+        rformat#connect self#rformat ;
         composer#connect (fun () -> self#update) ;
         browser#connect (fun () -> self#update) ;
         help#connect (fun () -> self#open_help) ;
@@ -220,6 +233,7 @@ class pane (enabled : GuiConfig.enabled) =
           | `Main | `Internal _ -> ()
 
     method private iformat f = printer#set_iformat f ; self#update
+    method private rformat f = printer#set_rformat f ; self#update
 
     method private autofocus = function
       | `Autofocus ->

src/plugins/wp/GuiSequent.ml

@@ -529,6 +529,9 @@ class focused (wtext : Wtext.text) =
     method set_iformat = plang#set_iformat
     method get_iformat = plang#get_iformat
 
+    method set_rformat = plang#set_rformat
+    method get_rformat = plang#get_rformat
+
     method selected =
       begin
         self#set_target self#selection ;

src/plugins/wp/GuiSequent.mli

@@ -37,9 +37,13 @@ class focused : Wtext.text ->
     method set_focus_mode : bool -> unit
     method get_state_mode : bool
     method set_state_mode : bool -> unit
+
     method get_iformat : Plang.iformat
     method set_iformat : Plang.iformat -> unit
 
+    method get_rformat : Plang.rformat
+    method set_rformat : Plang.rformat -> unit
+
     method selected : unit
     method unselect : target
     method restore : target -> unit

src/plugins/wp/LogicBuiltins.ml

@@ -141,7 +141,14 @@ let hacks = Hashtbl.create 8
 let hack name phi = Hashtbl.replace hacks name phi
 
 let lookup name kinds =
-  try HACK (Hashtbl.find hacks name)
+  try
+    let hack = Hashtbl.find hacks name in
+    let compute es =
+      try hack es with Not_found ->
+      match lookup_driver name kinds with
+      | ACSLDEF | HACK _ -> Warning.error "No fallback for hacked '%s'" name
+      | LFUN p -> F.e_fun p es
+    in HACK compute
   with Not_found -> lookup_driver name kinds
 
 let register ?source name kinds link =
@@ -285,11 +292,11 @@ let builtin_driver = {
 }
 
 let add_builtin name kinds lfun =
-  begin
-    Context.set driver builtin_driver;
-    register name kinds (LFUN lfun);
-    Context.clear driver;
-  end
+  let phi = LFUN lfun in
+  if Context.defined driver then
+    register name kinds phi
+  else
+    Context.bind driver builtin_driver (register name kinds) phi
 
 let create ~id ?(descr=id) ?(includes=[]) () =
   {
@@ -303,3 +310,5 @@ let create ~id ?(descr=id) ?(includes=[]) () =
 
 let init ~id ?descr ?includes () =
   Context.set driver (create ~id ?descr ?includes ())
+
+(* -------------------------------------------------------------------------- *)

src/plugins/wp/Plang.ml

@@ -68,6 +68,7 @@ module Env = E.Env
 
 type scope = Qed.Engine.scope
 type iformat = [ `Dec | `Hex | `Bin ]
+type rformat = [ `Ratio | `Float | `Double ]
 let sanitizer = Qed.Export.sanitize ~to_lowercase:false
 
 class engine =
@@ -76,10 +77,6 @@ class engine =
     inherit Lang.idprinting
     method infoprover w = w.altergo
 
-    val mutable iformat : iformat = `Dec
-    method get_iformat = iformat
-    method set_iformat (f : iformat) = iformat <- f
-
     (* --- Types --- *)
 
     method t_int = "Z"
@@ -98,11 +95,17 @@ class engine =
     method pp_datatype a fmt ts =
       Qed.Plib.pp_call_var ~f:(self#datatype a) self#pp_tau fmt ts
 
-    (* --- Primitives --- *)
+    (* --- Booleans --- *)
 
     method e_true _ = "true"
     method e_false _ = "false"
 
+    (* --- Integers --- *)
+
+    val mutable iformat : iformat = `Dec
+    method get_iformat = iformat
+    method set_iformat (f : iformat) = iformat <- f
+
     method pp_int _ fmt z =
       try
         let n = Integer.to_int z in
@@ -116,6 +119,12 @@ class engine =
       | `Hex -> Integer.pp_hex ~sep:"," fmt z
       | `Bin -> Integer.pp_bin ~sep:"," fmt z
 
+    (* --- Reals --- *)
+
+    val mutable rformat : rformat = `Ratio
+    method get_rformat = rformat
+    method set_rformat (f : rformat) = rformat <- f
+
     method pp_real fmt q =
       match Q.classify q with
       | Q.ZERO -> Format.pp_print_string fmt ".0"
@@ -123,11 +132,19 @@ class engine =
       | Q.MINF -> Format.pp_print_string fmt "(-1/.0)"
       | Q.UNDEF -> Format.pp_print_string fmt "(.0/.0)"
       | Q.NZERO ->
-          let { Q.num = num ; Q.den = den } = q in
-          if Z.equal den Z.one then
-            Format.fprintf fmt "%s.0" (Z.to_string num)
-          else
-            Format.fprintf fmt "(%s.0/%s)" (Z.to_string num) (Z.to_string den)
+          match rformat with
+          | `Ratio ->
+              let { Q.num = num ; Q.den = den } = q in
+              if Z.equal den Z.one then
+                Format.fprintf fmt "%s.0" (Z.to_string num)
+              else
+                Format.fprintf fmt "(%s.0/%s)"
+                  (Z.to_string num)
+                  (Z.to_string den)
+          | `Float ->
+              Format.fprintf fmt "%sf" (Cfloat.float_lit Ctypes.Float32 q)
+          | `Double ->
+              Format.fprintf fmt "%sd" (Cfloat.float_lit Ctypes.Float64 q)
 
     (* --- Atomicity --- *)
 

src/plugins/wp/Plang.mli

@@ -37,12 +37,15 @@ val alloc_domain : pool -> Vars.t
 val sanitizer : string -> string
 
 type iformat = [ `Hex | `Dec | `Bin ]
+type rformat = [ `Ratio | `Float | `Double ]
 
 class engine :
   object
     inherit [Z.t,ADT.t,Field.t,Fun.t,tau,var,term,Env.t] Qed.Engine.engine
     method get_iformat : iformat
     method set_iformat : iformat -> unit
+    method get_rformat : rformat
+    method set_rformat : rformat -> unit
     method marks : Env.t * Lang.F.marks
     method pp_pred : Format.formatter -> pred -> unit
     method lookup : term -> scope

src/plugins/wp/tests/wp_acsl/classify_float.c

@@ -2,6 +2,7 @@
    OPT: -wp-prover alt-ergo
    OPT: -wp-prover why3:alt-ergo
    OPT: -wp-prover coq -wp-coq-script tests/wp_acsl/classify_float.script
+   OPT: -wp-model real
  */
 
 /*@

src/plugins/wp/tests/wp_acsl/float_compare.i

 /* run.config_qualif
    OPT: -wp-prover why3:alt-ergo
+   OPT: -wp-model real
  */
 
 /*@ lemma test_float_compare:

src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle

@@ -121,13 +121,13 @@ Prove: lt_f64(a_1, b) <-> (r < of_f64(b)).
 
 ------------------------------------------------------------
 
-Goal Assertion (file tests/wp_acsl/float_compare.i, line 62):
+Goal Assertion (file tests/wp_acsl/float_compare.i, line 63):
 Assume { (* Pre-condition *) Have: is_finite_f32(a) /\ is_finite_f64(b). }
 Prove: is_finite_f64(to_f64(of_f32(a))).
 
 ------------------------------------------------------------
 
-Goal Assertion (file tests/wp_acsl/float_compare.i, line 63):
+Goal Assertion (file tests/wp_acsl/float_compare.i, line 64):
 Let r = of_f32(a).
 Let a_1 = to_f64(r).
 Assume {

src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle

+# frama-c -wp -wp-model 'Typed (Real)' [...]
+[kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] 3 goals scheduled
+[wp] [Qed] Goal typed_real_lemma_InfN_not_finite : Valid
+[wp] [Qed] Goal typed_real_lemma_InfP_not_finite : Valid
+[wp] [Qed] Goal typed_real_lemma_NaN_not_finite : Valid
+[wp] Proved goals:    3 / 3
+  Qed:             3
+[wp] Report in:  'tests/wp_acsl/oracle_qualif/classify_float.3.report.json'
+[wp] Report out: 'tests/wp_acsl/result_qualif/classify_float.3.report.json'
+-------------------------------------------------------------
+Axiomatics          WP     Alt-Ergo        Total   Success
+Lemma                3     -                 3       100%
+-------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.res.oracle

+# frama-c -wp -wp-model 'Typed (Real)' [...]
+[kernel] Parsing tests/wp_acsl/float_compare.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 19 goals scheduled
+[wp] [Qed] Goal typed_real_lemma_finite_32_64 : Valid
+[wp] [Qed] Goal typed_real_lemma_finite_32_64_real : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_real_lemma_test_double_compare : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_real_lemma_test_double_compare_greater : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_real_lemma_test_float_compare : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_real_lemma_test_float_compare_greater : Valid
+[wp] [Qed] Goal typed_real_cmp_dd_ensures_DEF : Valid
+[wp] [Qed] Goal typed_real_cmp_dd_ensures_REL1 : Valid
+[wp] [Qed] Goal typed_real_cmp_dd_ensures_REL2 : Valid
+[wp] [Qed] Goal typed_real_cmp_fd_ensures_DEF : Valid
+[wp] [Qed] Goal typed_real_cmp_fd_ensures_REL1 : Valid
+[wp] [Qed] Goal typed_real_cmp_fd_ensures_REL2 : Valid
+[wp] [Qed] Goal typed_real_cmp_fd_assert : Valid
+[wp] [Qed] Goal typed_real_cmp_fd_assert_2 : Valid
+[wp] [Qed] Goal typed_real_cmp_ff_ensures_DEF : Valid
+[wp] [Qed] Goal typed_real_cmp_ff_ensures_REL1 : Valid
+[wp] [Qed] Goal typed_real_cmp_ff_ensures_REL2 : Valid
+[wp] [Qed] Goal typed_real_cmp_fnan_ensures_POS : Valid
+[wp] [Qed] Goal typed_real_cmp_fnan_ensures_NEG : Valid
+[wp] Proved goals:   19 / 19
+  Qed:              15 
+  Alt-Ergo 2.0.0:    4
+[wp] Report in:  'tests/wp_acsl/oracle_qualif/float_compare.1.report.json'
+[wp] Report out: 'tests/wp_acsl/result_qualif/float_compare.1.report.json'
+-------------------------------------------------------------
+Axiomatics          WP     Alt-Ergo        Total   Success
+Lemma                2      4 (1..12)        6       100%
+-------------------------------------------------------------
+Functions           WP     Alt-Ergo        Total   Success
+cmp_ff               3     -                 3       100%
+cmp_dd               3     -                 3       100%
+cmp_fd               5     -                 5       100%
+cmp_fnan             2     -                 2       100%
+-------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/0229e4d03dbe5dab56c7710d10ede856.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0057,
+  "steps": 4 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/5a2626cdfff12f90f4c43a8b11ff70fb.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0047,
+  "steps": 4 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/d189bb3b47019848c9af5b14c2febb1c.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0056,
+  "steps": 4 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/e2c00d7a3ff17960fa10dee8b619ee99.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.005,
+  "steps": 4 }

src/plugins/wp/tests/wp_plugin/stmt.c

 /* run.config
-   OPT: -load-module report -then -report 
+   OPT: -load-module report -then -report
 */
 
 /* run.config_qualif
-   OPT: -load-module report -then -report 
-   EXECNOW: LOG stmt.log LOG f.dot LOG f_default_for_stmt_2.dot LOG g.dot LOG g_default_for_stmt_11.dot @frama-c@ -no-autoload-plugins -load-module wp -wp-precond-weakening -wp -wp-model Dump -wp-out tests/wp_plugin/result_qualif @PTEST_FILE@ 1> tests/wp_plugin/result_qualif/stmt.log
+   OPT: -load-module report -then -report
+   EXECNOW: LOG stmt.log LOG f.dot LOG f_default_for_stmt_2.dot LOG g.dot LOG g_default_for_stmt_11.dot @frama-c@ -no-autoload-plugins -load-module wp -wp-precond-weakening -wp -wp-model Dump -wp-out tests/wp_plugin/result_qualif -wp-cache none @PTEST_FILE@ 1> tests/wp_plugin/result_qualif/stmt.log
 */
 
 /*@ ensures a > 0 ==> \result == a + b;