From 8b3da8d8c97e6ed1f2d9f3dffe4b42856608d75e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Wed, 9 Oct 2019 13:21:10 +0200
Subject: [PATCH] Add conversion from generic floatting point contract to
finite one
---
Makefile | 1 +
headers/header_spec.txt | 2 +
.../contract_finite_float.ml | 83 +++++++++++++++++++
.../contract_finite_float.mli | 21 +++++
.../plugin_entry_points/kernel.ml | 10 +++
.../plugin_entry_points/kernel.mli | 3 +
src/plugins/wp/wpo.mli | 3 +-
tests/float/contract_finite_float.c | 29 +++++++
.../oracle/contract_finite_float.res.oracle | 39 +++++++++
9 files changed, 190 insertions(+), 1 deletion(-)
create mode 100644 src/kernel_services/ast_transformations/contract_finite_float.ml
create mode 100644 src/kernel_services/ast_transformations/contract_finite_float.mli
create mode 100644 tests/float/contract_finite_float.c
create mode 100644 tests/float/oracle/contract_finite_float.res.oracle
diff --git a/Makefile b/Makefile
index 72ee2dfc2f0..083de2d3112 100644
--- a/Makefile
+++ b/Makefile
@@ -612,6 +612,7 @@ KERNEL_CMO=\
src/kernel_services/ast_transformations/filter.cmo \
src/kernel_services/ast_transformations/inline.cmo \
src/kernel_internals/runtime/dump_config.cmo \
+ src/kernel_services/ast_transformations/contract_finite_float.cmo \
src/kernel_internals/runtime/special_hooks.cmo \
src/kernel_internals/runtime/messages.cmo
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index d1e4b57004f..c5a358290cf 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -567,6 +567,8 @@ src/kernel_services/ast_queries/logic_typing.mli: CEA_INRIA_LGPL
src/kernel_services/ast_queries/logic_utils.ml: CEA_INRIA_LGPL
src/kernel_services/ast_queries/logic_utils.mli: CEA_INRIA_LGPL
src/kernel_services/ast_transformations/README.md: .ignore
+src/kernel_services/ast_transformations/contract_finite_float.ml: CEA_LGPL
+src/kernel_services/ast_transformations/contract_finite_float.mli: CEA_LGPL
src/kernel_services/ast_transformations/clone.ml: CEA_LGPL
src/kernel_services/ast_transformations/clone.mli: CEA_LGPL
src/kernel_services/ast_transformations/filter.ml: CEA_LGPL
diff --git a/src/kernel_services/ast_transformations/contract_finite_float.ml b/src/kernel_services/ast_transformations/contract_finite_float.ml
new file mode 100644
index 00000000000..79a908dd694
--- /dev/null
+++ b/src/kernel_services/ast_transformations/contract_finite_float.ml
@@ -0,0 +1,83 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+let rec is_infinite_or_nan pred =
+ match pred.pred_content with
+ | Pand(a,b) -> is_infinite_or_nan a || is_infinite_or_nan b
+ | Papp ({l_var_info = { lv_name = ("\\is_plus_infinity"
+ |"\\is_minus_infinity"
+ |"\\is_infinite"
+ |"\\is_NaN")}},[],[_]) -> true
+ | _ -> false
+
+let visit = object
+ inherit Cil.nopCilVisitor
+
+ method! vspec spec =
+ let requires, behaviors = Extlib.fold_map_opt
+ (fun acc bhv ->
+ let exists = List.exists (function
+ | (Normal,v) ->
+ is_infinite_or_nan v.ip_content
+ | _ -> false
+ )
+ bhv.b_post_cond
+ in
+ if exists
+ then
+ let neg_assumes =
+ List.map (fun e -> (Logic_const.pnot (e.ip_content))) bhv.b_assumes
+ in
+ Logic_const.(new_predicate (pors neg_assumes))::acc
+ , None
+ else acc, Some bhv
+ )
+ [] spec.spec_behavior
+ in
+ spec.spec_behavior <- behaviors;
+ begin match requires with
+ | [] -> ()
+ | _ ->
+ List.iter
+ (fun bhv ->
+ if bhv.b_name = Cil.default_behavior_name then
+ bhv.b_requires <- requires@bhv.b_requires
+ )
+ spec.spec_behavior
+ end;
+ Cil.SkipChildren
+
+end
+
+let run ast =
+ if Kernel.ContractFiniteFloat.get () then
+ Cil.visitCilFileSameGlobals visit ast
+
+let transform =
+ File.register_code_transformation_category "contract_finite_float"
+
+let () =
+ File.add_code_transformation_before_cleanup
+ ~deps:[(module Kernel.ContractFiniteFloat)]
+ transform run
diff --git a/src/kernel_services/ast_transformations/contract_finite_float.mli b/src/kernel_services/ast_transformations/contract_finite_float.mli
new file mode 100644
index 00000000000..fa8f3783c35
--- /dev/null
+++ b/src/kernel_services/ast_transformations/contract_finite_float.mli
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 8b30799b24b..d8db54e0275 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -1320,6 +1320,16 @@ module Constfold =
let help = "fold all constant expressions in the code before analysis"
end)
+let () = Parameter_customize.set_group normalisation
+module ContractFiniteFloat =
+ False
+ (struct
+ let option_name = "-contract-finite-float"
+ let module_name = "ContractFiniteFloat"
+ let help = "Add requires in contract to forbid cases that ensures \
+ infinite or nan behaviors"
+ end)
+
let () = Parameter_customize.set_group normalisation
let () = Parameter_customize.do_not_reset_on_copy ()
module InitializedPaddingLocals =
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index c971c83111f..3490029a550 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -456,6 +456,9 @@ module SimplifyTrivialLoops: Parameter_sig.Bool
module Constfold: Parameter_sig.Bool
(** Behavior of option "-constfold" *)
+module ContractFiniteFloat: Parameter_sig.Bool
+ (** Behavior of option "-contract-finite-float" *)
+
module InitializedPaddingLocals: Parameter_sig.Bool
(** Behavior of option "-initialized-padding-locals" *)
diff --git a/src/plugins/wp/wpo.mli b/src/plugins/wp/wpo.mli
index 580b6469497..9491c8dc3c3 100644
--- a/src/plugins/wp/wpo.mli
+++ b/src/plugins/wp/wpo.mli
@@ -79,7 +79,8 @@ module VC_Annot :
sig
type t = {
- axioms : Definitions.axioms option ;
+ axioms
+ : Definitions.axioms option ;
goal : GOAL.t ;
tags : Splitter.tag list ;
warn : Warning.t list ;
diff --git a/tests/float/contract_finite_float.c b/tests/float/contract_finite_float.c
new file mode 100644
index 00000000000..07cfa158134
--- /dev/null
+++ b/tests/float/contract_finite_float.c
@@ -0,0 +1,29 @@
+/* run.config*
+ OPT: -eva @EVA_CONFIG@ -warn-special-float none -contract-finite-float
+*/
+
+#include <math.h>
+
+
+/*@
+ assigns \result \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ ensures res_finite: \is_finite(\result);
+ ensures positive_result: \result >= 0.;
+ ensures equal_magnitude_result: \result == x || \result == -x;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures res_nan: \is_NaN(\result);
+ behavior infinite:
+ assumes infinite_arg: \is_infinite(x);
+ ensures res_plus_infinity: \is_plus_infinity(\result);
+*/
+extern double myfabs(double x);
+
+volatile double x;
+
+int main(){
+ double z = x;
+ double y = myfabs(x);
+}
diff --git a/tests/float/oracle/contract_finite_float.res.oracle b/tests/float/oracle/contract_finite_float.res.oracle
new file mode 100644
index 00000000000..88888d6b1f3
--- /dev/null
+++ b/tests/float/oracle/contract_finite_float.res.oracle
@@ -0,0 +1,39 @@
+[kernel] Parsing tests/float/contract_finite_float.c (with preprocessing)
+[kernel] Failure: No kernel function for __builtin_va_copy(11)
+[kernel] Current source was: :0
+ The full backtrace is:
+ Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 532, characters 24-31
+ Called from file "src/kernel_services/plugin_entry_points/log.ml", line 1098, characters 17-55
+ Called from file "src/kernel_services/plugin_entry_points/log.ml", line 525, characters 9-23
+ Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 528, characters 9-16
+ Called from file "src/kernel_services/visitors/visitor.ml", line 630, characters 10-68
+ Called from file "src/kernel_services/ast_queries/cil.ml", line 1237, characters 15-31
+ Called from file "src/kernel_services/ast_queries/cil.ml", line 2742, characters 4-52
+ Called from file "src/kernel_services/ast_queries/cil.ml" (inlined), line 5458, characters 16-36
+ Called from file "src/kernel_services/ast_queries/cil.ml", line 5461, characters 13-20
+ Called from file "list.ml", line 106, characters 12-15
+ Called from file "src/kernel_services/ast_queries/cil.ml", line 5108, characters 2-29
+ Called from file "src/kernel_services/ast_queries/cil.ml", line 5459, characters 2-359
+ Called from file "src/kernel_services/ast_queries/cil.ml", line 1182, characters 19-39
+ Called from file "src/kernel_services/ast_queries/cil.ml", line 5492, characters 6-102
+ Called from file "src/kernel_services/visitors/visitor.ml" (inlined), line 853, characters 2-45
+ Called from file "src/kernel_services/ast_transformations/contract_finite_float.ml", line 35, characters 4-48
+ Called from file "src/kernel_services/ast_queries/file.ml", line 1043, characters 2-7
+ Called from file "queue.ml", line 105, characters 6-15
+ Called from file "src/topological.ml", line 137, characters 18-25
+ Called from file "src/kernel_services/ast_queries/file.ml", line 1099, characters 2-36
+ Called from file "src/kernel_services/ast_queries/file.ml", line 1567, characters 2-22
+ Called from file "src/kernel_services/ast_queries/file.ml", line 1645, characters 4-27
+ Called from file "src/kernel_services/ast_data/ast.ml", line 110, characters 2-28
+ Called from file "src/kernel_services/ast_data/ast.ml", line 118, characters 53-71
+ Called from file "src/kernel_internals/runtime/boot.ml", line 29, characters 6-20
+ Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9
+ Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64
+ Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
+
+ Frama-C aborted: internal error.
+ Please report as 'crash' at http://bts.frama-c.com/.
+ Your Frama-C version is 19.1+dev (Potassium).
+ Note that a version and a backtrace alone often do not contain enough
+ information to understand the bug. Guidelines for reporting bugs are at:
+ http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
--
GitLab