From ecfeaf2499831e663e3f5ddd05ce697ff81f7c9f Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 2 Mar 2020 14:06:23 +0100
Subject: [PATCH] [kernel] Adds sqrt/f ACSL builtin
---
.Makefile.lint | 1 -
share/libc/math.h | 2 +
src/kernel_internals/typing/logic_builtin.ml | 94 ++++++++++----------
tests/idct/oracle/ieee_1180_1990.res.oracle | 52 ++++++-----
tests/libc/oracle/fc_libc.1.res.oracle | 2 +
5 files changed, 81 insertions(+), 70 deletions(-)
diff --git a/.Makefile.lint b/.Makefile.lint
index 20840569b8e..f7d14e2be6e 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -13,7 +13,6 @@ ML_LINT_KO+=src/kernel_internals/typing/allocates.ml
ML_LINT_KO+=src/kernel_internals/typing/asm_contracts.ml
ML_LINT_KO+=src/kernel_internals/typing/frontc.mli
ML_LINT_KO+=src/kernel_internals/typing/infer_annotations.ml
-ML_LINT_KO+=src/kernel_internals/typing/logic_builtin.ml
ML_LINT_KO+=src/kernel_internals/typing/mergecil.mli
ML_LINT_KO+=src/kernel_internals/typing/translate_lightweight.ml
ML_LINT_KO+=src/kernel_internals/typing/translate_lightweight.mli
diff --git a/share/libc/math.h b/share/libc/math.h
index 58f24428a07..6ae90331c2e 100644
--- a/share/libc/math.h
+++ b/share/libc/math.h
@@ -539,6 +539,7 @@ extern long double powl(long double x, long double y);
assigns \result \from x;
ensures finite_result: \is_finite(\result);
ensures positive_result: \result >= -0.;
+ ensures result_value: \result == sqrt(x);
*/
extern double sqrt(double x);
@@ -547,6 +548,7 @@ extern double sqrt(double x);
assigns \result \from x;
ensures finite_result: \is_finite(\result);
ensures positive_result: \result >= -0.;
+ ensures result_value: \result == sqrtf(x);
*/
extern float sqrtf(float x);
diff --git a/src/kernel_internals/typing/logic_builtin.ml b/src/kernel_internals/typing/logic_builtin.ml
index 3f01fbad458..02d4a73809e 100644
--- a/src/kernel_internals/typing/logic_builtin.ml
+++ b/src/kernel_internals/typing/logic_builtin.ml
@@ -25,7 +25,7 @@
open Cil_types
let add = Logic_env.add_builtin_logic_function_gen
- Logic_utils.is_same_builtin_profile
+ Logic_utils.is_same_builtin_profile
let float_type = Ctype Cil.floatType
let double_type = Ctype Cil.doubleType
@@ -40,7 +40,7 @@ let init =
(* Since hooks are not projectified this function must be added exactly
once per session, otherwise we might end up with several built-ins with
the same name.
- *)
+ *)
fun () ->
if !called then (fun () -> ())
else begin
@@ -74,15 +74,15 @@ let init =
List.iter
(fun (typename, constrs) ->
let l =
- List.map
- (fun cname ->
+ List.map
+ (fun cname ->
let c =
{ ctor_name = cname; ctor_type = typename;
ctor_params = [] }
in
- Logic_env.add_builtin_logic_ctor cname c;
- c)
- constrs
+ Logic_env.add_builtin_logic_ctor cname c;
+ c)
+ constrs
in
typename.lt_def <- Some (LTsum l))
[ boolean, ["\\true"; "\\false"];
@@ -91,7 +91,7 @@ let init =
rounding_mode, [ "\\Up"; "\\Down"; "\\ToZero"; "\\NearestAway";
"\\NearestEven" ];
];
- (* logic types used by the builtins *)
+ (* logic types used by the builtins *)
let a_name, a_type = polymorphic_type "a" in
let boolean = Ltype(boolean,[]) in
let sign = Ltype(sign,[]) in
@@ -99,7 +99,7 @@ let init =
let rounding_mode = Ltype(rounding_mode,[]) in
let set_of_integer = Ltype (set, [Linteger]) in
let set_of_a_type = Ltype (set, [a_type]) in
- (* "\list" logic type with its constructors *)
+ (* "\list" logic type with its constructors *)
let list =
{ lt_name="\\list"; lt_params=[a_name]; lt_def=None; lt_attr=[]}
in
@@ -153,22 +153,22 @@ let init =
"\\no_overflow_single", [], [], ["m", rounding_mode; "x", Lreal] ;
"\\no_overflow_double", [], [], ["m", rounding_mode; "x", Lreal] ;
"\\subset", [a_name], [], ["s1", set_of_a_type;
- "s2", set_of_a_type];
+ "s2", set_of_a_type];
"\\pointer_comparable", [], [], [("p1", object_ptr);
- ("p2", object_ptr)];
+ ("p2", object_ptr)];
"\\pointer_comparable", [], [], [("p1", fun_ptr);
- ("p2", fun_ptr)];
+ ("p2", fun_ptr)];
"\\pointer_comparable", [], [], [("p1", fun_ptr);
- ("p2", object_ptr)];
+ ("p2", object_ptr)];
"\\pointer_comparable", [], [], [("p1", object_ptr);
- ("p2", fun_ptr)];
+ ("p2", fun_ptr)];
];
(* functions *)
List.iter
(fun (f,tparams,params,ret_type) ->
add { bl_name = f; bl_params = tparams; bl_profile = params;
bl_type = Some ret_type; bl_labels = []})
- [
+ [
"\\min", [], ["x",Linteger;"y",Linteger], Linteger ;
"\\max", [], ["x",Linteger;"y",Linteger], Linteger ;
"\\min", [], ["x",Lreal;"y",Lreal], Lreal ;
@@ -210,10 +210,12 @@ let init =
"\\pow", [], ["x",Lreal;"y",Lreal], Lreal ;
"\\fmod", [], ["x",Lreal;"y",Lreal], Lreal ;
+ "sqrt", [], ["x",double_type], double_type ;
"atan2", [], ["x",double_type;"y",double_type], double_type ;
"pow", [], ["x",double_type;"y",double_type], double_type ;
"fmod", [], ["x",double_type;"y",double_type], double_type ;
+ "sqrtf", [], ["x",float_type], float_type ;
"atan2f", [], ["x",float_type;"y",float_type], float_type ;
"powf", [], ["x",float_type;"y",float_type], float_type ;
"fmodf", [], ["x",float_type;"y",float_type], float_type ;
@@ -221,41 +223,41 @@ let init =
(* TODO ?
* div() frexp() ldexp()
* ldiv() modf() modf()
- *)
+ *)
"\\sum", [], ["min",Linteger;
- "max", Linteger;
- "f",(Larrow ([Linteger],Linteger))], Linteger ;
+ "max", Linteger;
+ "f",(Larrow ([Linteger],Linteger))], Linteger ;
"\\sum", [], ["min",Linteger;
- "max", Linteger;
- "f",(Larrow ([Linteger],Lreal))], Lreal ;
+ "max", Linteger;
+ "f",(Larrow ([Linteger],Lreal))], Lreal ;
"\\product", [], ["min",Linteger;
- "max", Linteger;
- "f",(Larrow ([Linteger],Linteger))], Linteger ;
+ "max", Linteger;
+ "f",(Larrow ([Linteger],Linteger))], Linteger ;
"\\product", [], ["min",Linteger;
- "max", Linteger;
- "f",(Larrow ([Linteger],Lreal))], Lreal ;
+ "max", Linteger;
+ "f",(Larrow ([Linteger],Lreal))], Lreal ;
"\\min", [], ["min",Linteger;
- "max", Linteger;
- "f",(Larrow ([Linteger],Linteger))], Linteger ;
+ "max", Linteger;
+ "f",(Larrow ([Linteger],Linteger))], Linteger ;
"\\min", [], ["min",Linteger;
- "max", Linteger;
- "f",(Larrow ([Linteger],Lreal))], Lreal ;
+ "max", Linteger;
+ "f",(Larrow ([Linteger],Lreal))], Lreal ;
"\\max", [], ["min",Linteger;
- "max", Linteger;
- "f",(Larrow ([Linteger],Linteger))], Linteger ;
+ "max", Linteger;
+ "f",(Larrow ([Linteger],Linteger))], Linteger ;
"\\max", [], ["min",Linteger;
- "max", Linteger;
- "f",(Larrow ([Linteger],Lreal))], Lreal ;
+ "max", Linteger;
+ "f",(Larrow ([Linteger],Lreal))], Lreal ;
"\\numof", [], ["min",Linteger;
- "max", Linteger;
- "f",(Larrow ([Linteger],boolean))], Linteger ;
+ "max", Linteger;
+ "f",(Larrow ([Linteger],boolean))], Linteger ;
(* for floats special values *)
- "\\round_float", [],
- ["f", float_format; "m", rounding_mode; "x", Lreal], Lreal ;
+ "\\round_float", [],
+ ["f", float_format; "m", rounding_mode; "x", Lreal], Lreal ;
"\\sign", [], ["x",float_type], sign ;
"\\sign", [], ["x",double_type], sign ;
@@ -281,27 +283,27 @@ let init =
"\\relative_error", [], ["x",double_type], Lreal;
(*"\\relative_error", [], ["x",long_double_type], Lreal;*)
- "\\round_float", [],
- ["m", rounding_mode; "x", Lreal], float_type;
- "\\round_double", [],
- ["m", rounding_mode ; "x", Lreal], double_type;
+ "\\round_float", [],
+ ["m", rounding_mode; "x", Lreal], float_type;
+ "\\round_double", [],
+ ["m", rounding_mode ; "x", Lreal], double_type;
"\\plus_infinity", [], [], float_type;
"\\minus_infinity", [], [], float_type;
"\\NaN", [], [], float_type;
- (*"\\round_quad", [],
+ (*"\\round_quad", [],
["m", rounding_mode; "x", Lreal], long_double_type;*)
"\\min", [], ["s", set_of_integer], Linteger;
"\\max", [], ["s", set_of_integer], Linteger;
"\\nth", [a_name],
- ["l", list_of_a_type; "n", Linteger], a_type;
+ ["l", list_of_a_type; "n", Linteger], a_type;
"\\length", [a_name],
- ["l", list_of_a_type], Linteger;
+ ["l", list_of_a_type], Linteger;
"\\concat", [a_name],
- ["l1", list_of_a_type; "l2", list_of_a_type], list_of_a_type;
- "\\repeat", [a_name],
- ["l", list_of_a_type; "n", Linteger], list_of_a_type;
+ ["l1", list_of_a_type; "l2", list_of_a_type], list_of_a_type;
+ "\\repeat", [a_name],
+ ["l", list_of_a_type; "n", Linteger], list_of_a_type;
]
end
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 1b12533c9f8..9cd3bd3d041 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -3324,6 +3324,9 @@
[ Extern ] Post-condition 'positive_result'
ensures positive_result: \result ≥ -0.
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'result_value'
+ ensures result_value: \result ≡ sqrt(\old(x))
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
@@ -3344,10 +3347,13 @@
[ Extern ] Post-condition 'positive_result'
ensures positive_result: \result ≥ -0.
Unverifiable but considered Valid.
+[ Extern ] Post-condition 'result_value'
+ ensures result_value: \result ≡ sqrtf(\old(x))
+ Unverifiable but considered Valid.
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 547)
+[ Extern ] Froms (file share/libc/math.h, line 548)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3367,7 +3373,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 555)
+[ Extern ] Froms (file share/libc/math.h, line 557)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3384,7 +3390,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 578)
+[ Extern ] Froms (file share/libc/math.h, line 580)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3401,7 +3407,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 584)
+[ Extern ] Froms (file share/libc/math.h, line 586)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3418,7 +3424,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 591)
+[ Extern ] Froms (file share/libc/math.h, line 593)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3435,7 +3441,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 597)
+[ Extern ] Froms (file share/libc/math.h, line 599)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3452,7 +3458,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 603)
+[ Extern ] Froms (file share/libc/math.h, line 605)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3469,7 +3475,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 609)
+[ Extern ] Froms (file share/libc/math.h, line 611)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3486,7 +3492,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 631)
+[ Extern ] Froms (file share/libc/math.h, line 633)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3503,7 +3509,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 637)
+[ Extern ] Froms (file share/libc/math.h, line 639)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3520,7 +3526,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 643)
+[ Extern ] Froms (file share/libc/math.h, line 645)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3537,7 +3543,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 657)
+[ Extern ] Froms (file share/libc/math.h, line 659)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3554,7 +3560,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 663)
+[ Extern ] Froms (file share/libc/math.h, line 665)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3571,7 +3577,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 669)
+[ Extern ] Froms (file share/libc/math.h, line 671)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3588,7 +3594,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 676)
+[ Extern ] Froms (file share/libc/math.h, line 678)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3605,7 +3611,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 683)
+[ Extern ] Froms (file share/libc/math.h, line 685)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3622,7 +3628,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 704)
+[ Extern ] Froms (file share/libc/math.h, line 706)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3639,7 +3645,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 711)
+[ Extern ] Froms (file share/libc/math.h, line 713)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3656,7 +3662,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 718)
+[ Extern ] Froms (file share/libc/math.h, line 720)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3673,7 +3679,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 766)
+[ Extern ] Froms (file share/libc/math.h, line 768)
assigns \result \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3690,7 +3696,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 772)
+[ Extern ] Froms (file share/libc/math.h, line 774)
assigns \result \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -4054,7 +4060,7 @@
--------------------------------------------------------------------------------
179 Completely validated
16 Locally validated
- 484 Considered valid
+ 486 Considered valid
56 To be validated
- 735 Total
+ 737 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 26025f53b3f..705dcf5c78c 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3256,6 +3256,7 @@ extern float powf(float x, float y);
requires arg_positive: x ≥ -0.;
ensures finite_result: \is_finite(\result);
ensures positive_result: \result ≥ -0.;
+ ensures result_value: \result ≡ sqrt(\old(x));
assigns \result;
assigns \result \from x;
*/
@@ -3265,6 +3266,7 @@ extern double sqrt(double x);
requires arg_positive: x ≥ -0.;
ensures finite_result: \is_finite(\result);
ensures positive_result: \result ≥ -0.;
+ ensures result_value: \result ≡ sqrtf(\old(x));
assigns \result;
assigns \result \from x;
*/
--
GitLab