Commit 4d7dd217 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Add a new transformation that instantiates the axioms marked with the

meta "instantiate : auto" on as many terms as possible.

The transformation is rather naive, since it doesn't look for term
candidates under quantifiers, if-then-else, let-in, and so on. So it can
only appear late in the transformation pipe.

It is only enabled for Gappa and its target axioms are the ones that state
that any floating-point value is bounded. It was the last transformation
from Why2 still missing in Why3.

Thanks to this transformation, Gappa is now able to prove all the safety
obligations from the following code, including the ones about division and
downcast, which is definitely frightening.

/*@ assigns \nothing;
  @ ensures \result == \abs(x);
extern double fabs(double x);

/*@ requires \valid(AB_Ptr) && \valid(CD_Ptr);
  @ assigns *AB_Ptr, *CD_Ptr;
  @ ensures \abs(*AB_Ptr) <= 6.111111e-2;
  @ ensures \abs(*CD_Ptr) <= 6.111111e-2;
  @ */
void limitValue(float *AB_Ptr, float *CD_Ptr)
   double Fabs_AB, Fabs_CD;
   double max;

   Fabs_AB = fabs (*AB_Ptr);
   Fabs_CD = fabs (*CD_Ptr);

   max = Fabs_AB;
   if (Fabs_CD > Fabs_AB)  max = Fabs_CD;

   if ( max > 6.111111e-2)
      *AB_Ptr = (float) (((*AB_Ptr) * 6.111111e-2) / max);
      *CD_Ptr = (float) (((*CD_Ptr) * 6.111111e-2) / max);
parent 06c33403
......@@ -131,7 +131,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
encoding_explicit encoding_guard encoding_sort \
encoding_instantiate simplify_array filter_trigger \
introduction abstraction close_epsilon lift_epsilon \
eval_match instantiate_predicate
LIB_PRINTER = print_number alt_ergo why3printer smtv1 smtv2 \
coq tptp simplify gappa cvc3 yices
......@@ -24,6 +24,7 @@ transformation "simplify_formula"
transformation "simplify_unknown_lsymbols"
transformation "simplify_trivial_quantification"
transformation "introduce_premises"
transformation "instantiate_predicate"
transformation "abstract_unknown_lsymbols"
theory BuiltIn
......@@ -164,12 +165,14 @@ end
theory floating_point.Single
syntax function round "float<ieee_32,%1>(%2)"
meta "instantiate : auto" prop Bounded_value
theory floating_point.Double
syntax function round "float<ieee_64,%1>(%2)"
meta "instantiate : auto" prop Bounded_value
(* *)
(* Copyright (C) 2011 *)
(* Guillaume Melquiond *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* *)
open Decl
open Term
open Ty
let instantiate_prop expr args values =
let add (mt,mv) x y = ty_match mt x.vs_ty (t_type y), Mvs.add x y mv in
let (mt,mv) = List.fold_left2 add (Mtv.empty, Mvs.empty) args values in
t_ty_subst mt mv expr
(** [trans spr task_hd ((lpr, past), task)] looks in [task_hd] for terms
that can instantiate axioms of [lpr] and does so in [task]; [lpr] is
progressively filled with the axioms of [spr] as they are
encountered; [past] contains terms for which axioms have already been
instantiated, so that they are not duplicated *)
let trans spr task_hd (((lpr, past), task) as current) =
let rec scan_term ((past, task) as current) t =
let current =
if t.t_ty = None || Sterm.mem t past then current else
Sterm.add t past,
List.fold_right (fun (quant, e) task ->
let ax = instantiate_prop e quant [t] in
let pr = create_prsymbol (Ident.id_fresh "auto_instance") in
Task.add_decl task (create_prop_decl Paxiom pr ax)
with TypeMismatch _ -> task
) lpr task
) in
match t.t_node with
| Tapp _ ->
t_fold scan_term current t
| Tbinop (_,f1,f2) ->
t_fold scan_term (t_fold scan_term current f1) f2
| Tnot f ->
t_fold scan_term current f
| _ -> current in
let (current, task) =
match task_hd.Task.task_decl.Theory.td_node with
| Theory.Decl { d_node = Dprop (_,pr,expr) } ->
let (past, task) = scan_term (past, task) expr in
let lpr = if not (Spr.mem pr spr) then lpr else
match expr.t_node with
| Tquant (Tforall,q_expr) ->
let (quant, _, expr) = t_open_quant q_expr in
assert (List.length quant = 1);
(quant, expr) :: lpr
| _ -> assert false in
((lpr, past), task)
| _ -> current in
(current, Task.add_tdecl task task_hd.Task.task_decl)
let meta = Theory.register_meta "instantiate : auto" [Theory.MTprsymbol]
(** all the symbols (unary predicates) that have the "instantiate : auto"
meta are marked for instantiation by the above transformation *)
let () =
Trans.register_transform "instantiate_predicate"
(Trans.on_tagged_pr meta (fun spr ->
Trans.fold_map (trans spr) ([], Sterm.empty) None))
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment