From d5f3afc80e2a0b130e5ecd0ef8bc9244ff8aa2be Mon Sep 17 00:00:00 2001
From: Fonenantsoa Maurica <maurica.fonenantsoa@gmail.com>
Date: Thu, 15 Nov 2018 13:17:07 +0100
Subject: [PATCH] Fixes Issue 69: unsound translation when bounds for
quantified variables are bigger than their types
---
src/plugins/e-acsl/VERSION | 2 +-
src/plugins/e-acsl/doc/Changelog | 1 +
src/plugins/e-acsl/interval.ml | 1 +
src/plugins/e-acsl/interval.mli | 1 +
src/plugins/e-acsl/loops.ml | 88 +++++++++++++++++--
src/plugins/e-acsl/loops.mli | 3 +
src/plugins/e-acsl/misc.ml | 4 +
src/plugins/e-acsl/misc.mli | 3 +
src/plugins/e-acsl/tests/bts/issue69.c | 12 +++
.../e-acsl/tests/bts/oracle/gen_issue69.c | 69 +++++++++++++++
.../tests/bts/oracle/issue69.res.oracle | 3 +
src/plugins/e-acsl/translate.ml | 1 +
12 files changed, 181 insertions(+), 7 deletions(-)
create mode 100644 src/plugins/e-acsl/tests/bts/issue69.c
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/issue69.res.oracle
diff --git a/src/plugins/e-acsl/VERSION b/src/plugins/e-acsl/VERSION
index 93cc5dffbe7..06088970bd5 100644
--- a/src/plugins/e-acsl/VERSION
+++ b/src/plugins/e-acsl/VERSION
@@ -1 +1 @@
-18.0+dev
+18.0-beta
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 83371e18524..9897d0a71f4 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -23,6 +23,7 @@
Plugin E-ACSL 18.0 (Argon)
##########################
+-* E-ACSL [2018/11/13] Fix typing bug for quantified variables.
-* runtime [2018/11/13] Fix bug #!2405 about memory initialization
in presence of GCC constructors.
-* E-ACSL [2018/10/23] Fix bug #2406 about monitoring of variables
diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index 0f68e4bc8d0..005ea7a7c26 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -61,6 +61,7 @@ module Env = struct
let clear () = Logic_var.Hashtbl.clear tbl
let add = Logic_var.Hashtbl.add tbl
let remove = Logic_var.Hashtbl.remove tbl
+ let replace = Logic_var.Hashtbl.replace tbl
let find = Logic_var.Hashtbl.find tbl
end
diff --git a/src/plugins/e-acsl/interval.mli b/src/plugins/e-acsl/interval.mli
index 3d5fd8b3be2..958f24409dd 100644
--- a/src/plugins/e-acsl/interval.mli
+++ b/src/plugins/e-acsl/interval.mli
@@ -66,6 +66,7 @@ module Env: sig
val clear: unit -> unit
val add: Cil_types.logic_var -> Ival.t -> unit
val remove: Cil_types.logic_var -> unit
+ val replace: Cil_types.logic_var -> Ival.t -> unit
end
(* ************************************************************************** *)
diff --git a/src/plugins/e-acsl/loops.ml b/src/plugins/e-acsl/loops.ml
index 2d0551e2996..ea01ce00c63 100644
--- a/src/plugins/e-acsl/loops.ml
+++ b/src/plugins/e-acsl/loops.ml
@@ -31,6 +31,10 @@ let translate_named_predicate_ref
: (kernel_function -> Env.t -> predicate -> Env.t) ref
= Extlib.mk_fun "translate_named_predicate_ref"
+let named_predicate_ref
+ : (kernel_function -> Env.t -> predicate -> exp * Env.t) ref
+ = Extlib.mk_fun "named_predicate_ref"
+
let term_to_exp_ref
: (kernel_function -> Env.t -> term -> exp * Env.t) ref
= Extlib.mk_fun "term_to_exp_ref"
@@ -98,12 +102,74 @@ let preserve_invariant prj env kf stmt = match stmt.skind with
(**************************** Nested loops ********************************)
(**************************************************************************)
+(* It could happen that the bounds provided for a quantifier [lv] are bigger
+ than its type. [bounds_for_small_type] handles such cases
+ and provides smaller bounds whenever possible.
+ Let B be the inferred interval and R the range of [lv.typ]
+ - Case 1: B \subseteq R
+ Example: [\forall unsigned char c; 4 <= c <= 100 ==> 0 <= c <= 255]
+ Return: B
+ - Case 2: B \not\subseteq R and the bounds of B are inferred exactly
+ Example: [\forall unsigned char c; 4 <= c <= 300 ==> 0 <= c <= 255]
+ Return: B \intersect R
+ - Case 3: B \not\subseteq R and the bounds of B are NOT inferred exactly
+ Example: [\let m = n > 0 ? 4 : 341; \forall char u; 1 < u < m ==> u > 0]
+ Return: R with a guard guaranteeing that [lv] does not overflow *)
+let bounds_for_small_type ~loc (t1, lv, t2) =
+ match lv.lv_type with
+ | Linteger ->
+ t1, t2, None
+ | Ctype ty ->
+ let i1 = Interval.infer t1 in
+ let i2 = Interval.infer t2 in
+ let i =
+ (* Ival.join would NOT be correct here:
+ Eg: (Ival.join [-3..-3] [300..300]) gives {-3, 300}
+ but NOT [-3..300] *)
+ Ival.inject_range (Ival.min_int i1) (Ival.max_int i2)
+ in
+ let ity = Interval.interv_of_typ ty in
+ if Ival.is_included i ity then
+ (* case 1 *)
+ t1, t2, None
+ else if Ival.is_singleton_int i1 && Ival.is_singleton_int i2 then begin
+ (* case 2 *)
+ let i = Ival.meet i ity in
+ (* now we potentially have a better interval for [lv]
+ ==> update the binding *)
+ Interval.Env.replace lv i;
+ (* the smaller bounds *)
+ let min, max = Misc.finite_min_and_max i in
+ let t1 = Logic_const.tint ~loc min in
+ let t2 = Logic_const.tint ~loc max in
+ let ctx = Typing.integer_ty_of_typ ty in
+ (* we are assured that we will not have a GMP,
+ once again because we intersected with [ity] *)
+ Typing.type_term ~use_gmp_opt:false ~ctx t1;
+ Typing.type_term ~use_gmp_opt:false ~ctx t2;
+ t1, t2, None
+ end else
+ (* case 3 *)
+ let min, max = Misc.finite_min_and_max ity in
+ let guard_lower = Logic_const.tint ~loc min in
+ let guard_upper = Logic_const.tint ~loc max in
+ let lv_term = Logic_const.tvar ~loc lv in
+ let guard_lower = Logic_const.prel ~loc (Rle, guard_lower, lv_term) in
+ let guard_upper = Logic_const.prel ~loc (Rle, lv_term, guard_upper) in
+ let guard = Logic_const.pand ~loc (guard_lower, guard_upper) in
+ t1, t2, Some guard
+ | Ltype _ | Lvar _ | Lreal | Larrow _ ->
+ Options.abort "quantification over non-integer type is not part of E-ACSL"
+
let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
let term_to_exp = !term_to_exp_ref in
match lscope_vars with
| [] ->
mk_innermost_block env
| Lscope.Lvs_quantif(t1, rel1, logic_x, rel2, t2) :: lscope_vars' ->
+ let t1, t2, guard_for_small_type_opt =
+ bounds_for_small_type ~loc (t1, logic_x, t2)
+ in
let ctx =
let ty1 = Typing.get_integer_ty t1 in
let ty2 = Typing.get_integer_ty t2 in
@@ -198,8 +264,6 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
let guard = block_to_stmt guard_blk in
(* increment the loop counter [x++];
previous typing ensures that [x++] fits type [ty] *)
- (* TODO: should check that it does not overflow in the case of the type
- of the loop variable is __declared__ too small. *)
let tlv_one = t_plus_one ~ty:ctx_one tlv in
let incr, env = term_to_exp kf (Env.push env) tlv_one in
let next_blk, env = Env.pop_and_get
@@ -208,20 +272,32 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
~global_clear:false
Env.Middle
in
- (* remove logic binding now that the block is constructed *)
- let env = Env.Logic_binding.remove env logic_x in
(* generate the whole loop *)
- let start = block_to_stmt init_blk in
let next = block_to_stmt next_blk in
+ let stmts, env = match guard_for_small_type_opt with
+ | None ->
+ guard :: body @ [ next ], env
+ | Some p ->
+ let e, env = !named_predicate_ref kf (Env.push env) p in
+ let stmt, env =
+ Misc.mk_e_acsl_guard ~reverse:true Misc.RTE kf e p, env
+ in
+ let b, env = Env.pop_and_get env stmt ~global_clear:false Env.After in
+ let guard_for_small_type = Cil.mkStmt ~valid_sid:true (Block b) in
+ guard_for_small_type :: guard :: body @ [ next ], env
+ in
+ let start = block_to_stmt init_blk in
let stmt = mkStmt
~valid_sid:true
(Loop(
[],
- mkBlock (guard :: body @ [ next ]),
+ mkBlock stmts,
loc,
None,
Some break_stmt))
in
+ (* remove logic binding before returning *)
+ let env = Env.Logic_binding.remove env logic_x in
[ start ; stmt ], env
| Lscope.Lvs_let(lv, t) :: lscope_vars' ->
let ty = Typing.get_typ t in
diff --git a/src/plugins/e-acsl/loops.mli b/src/plugins/e-acsl/loops.mli
index 3a5dfa38146..27a0596d6be 100644
--- a/src/plugins/e-acsl/loops.mli
+++ b/src/plugins/e-acsl/loops.mli
@@ -62,6 +62,9 @@ val mk_nested_loops:
val translate_named_predicate_ref:
(kernel_function -> Env.t -> predicate -> Env.t) ref
+val named_predicate_ref:
+ (kernel_function -> Env.t -> predicate -> exp * Env.t) ref
+
val term_to_exp_ref:
(kernel_function -> Env.t -> term -> exp * Env.t) ref
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index 55ef595b98f..ee27e0f4521 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -311,6 +311,10 @@ let mk_ptr_sizeof typ loc =
| TPtr (t', _) -> Cil.new_exp ~loc (SizeOf t')
| _ -> assert false
+let finite_min_and_max i = match Ival.min_and_max i with
+ | Some min, Some max -> min, max
+ | None, _ | _, None -> assert false
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/misc.mli b/src/plugins/e-acsl/misc.mli
index c78ce824241..8f12597aa04 100644
--- a/src/plugins/e-acsl/misc.mli
+++ b/src/plugins/e-acsl/misc.mli
@@ -124,6 +124,9 @@ val mk_ptr_sizeof: typ -> location -> exp
(* [mk_ptr_sizeof ptr_typ loc] takes the pointer typ [ptr_typ] that points
to a [typ] typ and returns [sizeof(typ)]. *)
+val finite_min_and_max: Ival.t -> Integer.t * Integer.t
+(* [finite_min_and_max i] takes the finite ival [i] and returns its bounds *)
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/tests/bts/issue69.c b/src/plugins/e-acsl/tests/bts/issue69.c
new file mode 100644
index 00000000000..c571c92c749
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/issue69.c
@@ -0,0 +1,12 @@
+/* run.config
+ COMMENT: typing bug of Issue 69
+*/
+
+int main(void) {
+ /*@ assert \forall unsigned char c; 4 <= c <= 300 ==> 0 <= c <= 255; */ ;
+
+ int n = 5;
+ /*@ assert
+ \let m = n > 0 ? 4 : 341;
+ \forall char u; 1 < u < m ==> u > 0; */ ;
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c
new file mode 100644
index 00000000000..a25febaa04e
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c
@@ -0,0 +1,69 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ /*@ assert ∀ unsigned char c; 4 ≤ c ≤ 300 ⇒ 0 ≤ c ≤ 255; */
+ {
+ int __gen_e_acsl_forall;
+ int __gen_e_acsl_c;
+ __gen_e_acsl_forall = 1;
+ __gen_e_acsl_c = (unsigned char)4;
+ while (1) {
+ if (__gen_e_acsl_c <= 255) ; else break;
+ {
+ int __gen_e_acsl_and;
+ if (0 <= __gen_e_acsl_c) __gen_e_acsl_and = __gen_e_acsl_c <= 255;
+ else __gen_e_acsl_and = 0;
+ if (__gen_e_acsl_and) ;
+ else {
+ __gen_e_acsl_forall = 0;
+ goto e_acsl_end_loop1;
+ }
+ }
+ __gen_e_acsl_c ++;
+ }
+ e_acsl_end_loop1: ;
+ __e_acsl_assert(__gen_e_acsl_forall,(char *)"Assertion",(char *)"main",
+ (char *)"\\forall unsigned char c; 4 <= c <= 300 ==> 0 <= c <= 255",
+ 6);
+ }
+ int n = 5;
+ /*@ assert \let m = n > 0? 4: 341; ∀ char u; 1 < u < m ⇒ u > 0; */
+ {
+ int __gen_e_acsl_m;
+ int __gen_e_acsl_if;
+ int __gen_e_acsl_forall_2;
+ int __gen_e_acsl_u;
+ if (n > 0) __gen_e_acsl_if = 4; else __gen_e_acsl_if = 341;
+ __gen_e_acsl_m = __gen_e_acsl_if;
+ __gen_e_acsl_forall_2 = 1;
+ __gen_e_acsl_u = (char)1 + 1;
+ while (1) {
+ {
+ int __gen_e_acsl_and_2;
+ if (-128 <= __gen_e_acsl_u) __gen_e_acsl_and_2 = __gen_e_acsl_u <= 127;
+ else __gen_e_acsl_and_2 = 0;
+ __e_acsl_assert(__gen_e_acsl_and_2,(char *)"RTE",(char *)"main",
+ (char *)"-128 <= u <= 127",11);
+ }
+ if (__gen_e_acsl_u < __gen_e_acsl_m) ; else break;
+ if (__gen_e_acsl_u > 0) ;
+ else {
+ __gen_e_acsl_forall_2 = 0;
+ goto e_acsl_end_loop2;
+ }
+ __gen_e_acsl_u ++;
+ }
+ e_acsl_end_loop2: ;
+ __e_acsl_assert(__gen_e_acsl_forall_2,(char *)"Assertion",(char *)"main",
+ (char *)"\\let m = n > 0? 4: 341;\n\\forall char u; 1 < u < m ==> u > 0",
+ 10);
+ }
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue69.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue69.res.oracle
new file mode 100644
index 00000000000..a3f1846d9e3
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue69.res.oracle
@@ -0,0 +1,3 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/bts/issue69.c:10: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 5d44cafba2c..089c2b98ab3 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -840,6 +840,7 @@ let named_predicate_to_exp ?name kf env p =
let () =
Loops.term_to_exp_ref := term_to_exp;
Loops.translate_named_predicate_ref := translate_named_predicate;
+ Loops.named_predicate_ref := named_predicate_to_exp;
Quantif.predicate_to_exp_ref := named_predicate_to_exp;
At_with_lscope.term_to_exp_ref := term_to_exp;
At_with_lscope.predicate_to_exp_ref := named_predicate_to_exp;
--
GitLab