From 76ca0d357b1973d2c26a884006ac9facbed29afe Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Tue, 20 Aug 2019 14:55:37 +0200
Subject: [PATCH] [Eva] evaluate logic function memchr_off
---
share/libc/__fc_string_axiomatic.h | 4 +-
.../value/domains/cvalue/builtins_string.ml | 8 +++
.../value/domains/cvalue/builtins_string.mli | 2 +
src/plugins/value/legacy/eval_terms.ml | 60 +++++++++++++++++++
4 files changed, 72 insertions(+), 2 deletions(-)
diff --git a/share/libc/__fc_string_axiomatic.h b/share/libc/__fc_string_axiomatic.h
index efd4b09bc69..249460be20a 100644
--- a/share/libc/__fc_string_axiomatic.h
+++ b/share/libc/__fc_string_axiomatic.h
@@ -44,7 +44,6 @@ __BEGIN_DECLS
@ }
@*/
-
/*@ axiomatic MemChr {
@ logic 𔹠memchr{L}(char *s, ℤ c, ℤ n)
@ reads s[0..n - 1];
@@ -52,7 +51,8 @@ __BEGIN_DECLS
@
@ logic ℤ memchr_off{L}(char *s, ℤ c, ℤ n)
@ reads s[0..n - 1];
- @ // Returns the offset at which [c] appears in [s]. // TODO: is n useful?
+ @ // Returns the offset at which [c] appears in [s], or [n-1] otherwise.
+ @ // It represents the largest searched index when looking for [c] in [s].
@
@ axiom memchr_def{L}:
@ \forall char *s; \forall ℤ c; \forall ℤ n;
diff --git a/src/plugins/value/domains/cvalue/builtins_string.ml b/src/plugins/value/domains/cvalue/builtins_string.ml
index 2c39d88a1ba..fe5d9582572 100644
--- a/src/plugins/value/domains/cvalue/builtins_string.ml
+++ b/src/plugins/value/domains/cvalue/builtins_string.ml
@@ -435,6 +435,10 @@ let _frama_c_strnlen_wrapper =
register_builtin "strnlen"
~search:Ival.zero ~stop_at_0:false ~typ:Char ~length:true ~limit:1
+let frama_c_memchr_off_wrapper =
+ register_builtin "__fc_memchr_off"
+ ~search:Ival.bottom ~stop_at_0:false ~typ:Char ~length:true ~limit:2
+
let _frama_c_memchr_wrapper =
register_builtin "memchr"
~search:Ival.bottom ~stop_at_0:false ~typ:Char ~length:false ~limit:2
@@ -451,6 +455,10 @@ let frama_c_wcslen_wrapper =
register_builtin "wcslen"
~search:Ival.zero ~stop_at_0:false ~typ:Wide ~length:true ?limit:None
+let frama_c_wmemchr_off_wrapper =
+ register_builtin "__fc_wmemchr_off"
+ ~search:Ival.bottom ~stop_at_0:false ~typ:Wide ~length:true ~limit:2
+
let frama_c_wcschr_wrapper =
register_builtin "wcschr"
~search:Ival.bottom ~stop_at_0:true ~typ:Wide ~length:false ?limit:None
diff --git a/src/plugins/value/domains/cvalue/builtins_string.mli b/src/plugins/value/domains/cvalue/builtins_string.mli
index a19e4d7b091..b5e79dfd512 100644
--- a/src/plugins/value/domains/cvalue/builtins_string.mli
+++ b/src/plugins/value/domains/cvalue/builtins_string.mli
@@ -30,3 +30,5 @@ val frama_c_strlen_wrapper: str_builtin_sig
val frama_c_wcslen_wrapper: str_builtin_sig
val frama_c_strchr_wrapper: str_builtin_sig
val frama_c_wcschr_wrapper: str_builtin_sig
+val frama_c_memchr_off_wrapper: str_builtin_sig
+val frama_c_wmemchr_off_wrapper: str_builtin_sig
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 13ffb2300d3..27318b86c56 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -613,6 +613,53 @@ let eval_logic_charchr builtin env s c ldeps_s ldeps_c =
let ldeps = join_logic_deps ldeps_s ldeps_c in
{ etype; ldeps; eover; empty = false; eunder }
+(* Evaluates the logical functions memchr_off/wmemchr_off. *)
+let eval_logic_memchr_off builtin env s c n ldeps_s ldeps_c ldeps_n =
+ let max_bounds =
+ try
+ Ival.max_int (Cvalue.V.project_ival n)
+ with Cvalue.V.Not_based_on_null | Error_Bottom -> None
+ in
+ let v_bounds =
+ Cvalue.V.inject_ival (Ival.inject_range (Some Int.zero) (Extlib.opt_map Int.pred max_bounds))
+ in
+ let eover =
+ match builtin (env_current_state env) [s; c; n] with
+ | None, _ -> v_bounds
+ | Some offsm, alarms ->
+ if alarms
+ then v_bounds
+ else
+ begin
+ let normalized_v =
+ let v = Extlib.the (Cvalue.V_Offsetmap.single_interval_value offsm) in
+ let r = Cvalue.V_Or_Uninitialized.get_v v in
+ try
+ let ir = Cvalue.V.project_ival r in
+ match Ival.max_int ir with
+ | None -> v_bounds
+ | Some m ->
+ let normalized_i =
+ match max_bounds with
+ | Some n ->
+ if Int.(equal m n) then
+ Ival.join (Ival.inject_singleton (Int.pred m)) ir
+ else ir
+ | None -> ir
+ in
+ Cvalue.V.inject_ival normalized_i
+ with
+ | Cvalue.V.Not_based_on_null -> v_bounds
+ in
+ Cvalue.V.meet normalized_v v_bounds
+ end
+ in
+ let eunder = under_from_over eover in
+ let etype = Cil.intType in
+ let ldeps = join_logic_deps ldeps_s (join_logic_deps ldeps_c ldeps_n) in
+ { etype; ldeps; eover; eunder }
+
+
(* Evaluates the logical predicate is_allocable, according to the following
logic:
- if the size to allocate is always too large (> SIZE_MAX), allocation fails;
@@ -682,6 +729,8 @@ let known_logic_funs = [
"wcslen", Libc;
"strchr", Libc;
"wcschr", Libc;
+ "memchr_off", Libc;
+ "wmemchr_off", Libc;
"atan2", ACSL;
"atan2f", ACSL;
"pow", ACSL;
@@ -1304,6 +1353,17 @@ and eval_known_logic_function ~alarm_mode env li labels args =
in
eval_logic_charlen builtin { env with e_cur = lbl } r.eover r.ldeps
+ | ("memchr_off" | "wmemchr_off") as b, _, [lbl], [arg_s; arg_c; arg_n] ->
+ let s = eval_term ~alarm_mode env arg_s in
+ let c = eval_term ~alarm_mode env arg_c in
+ let n = eval_term ~alarm_mode env arg_n in
+ let builtin =
+ if b = "memchr_off" then Builtins_string.frama_c_memchr_off_wrapper
+ else Builtins_string.frama_c_wmemchr_off_wrapper
+ in
+ eval_logic_memchr_off builtin
+ { env with e_cur = lbl } s.eover c.eover n.eover s.ldeps c.ldeps n.ldeps
+
| ("strchr" | "wcschr") as b, _, [lbl], [arg_s; arg_c] ->
let s = eval_term ~alarm_mode env arg_s in
let c = eval_term ~alarm_mode env arg_c in
--
GitLab