From b7fe57005bee6ed79ede4b2ac0080c7644dfd8bb Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 25 Feb 2019 15:10:51 +0100
Subject: [PATCH] [ACSL] Make `Logic_interp` aware of local variables scopes
Note: at some point, it might be useful to make `term` and `pred` take a
`kinstr` as argument to have a better scope for typechecking.
---
src/kernel_services/analysis/logic_interp.ml | 52 +++++++++++++++----
.../ast_data/kernel_function.ml | 6 +++
.../ast_data/kernel_function.mli | 8 +++
3 files changed, 56 insertions(+), 10 deletions(-)
diff --git a/src/kernel_services/analysis/logic_interp.ml b/src/kernel_services/analysis/logic_interp.ml
index 8a82bb7009c..e8af8bc2a58 100644
--- a/src/kernel_services/analysis/logic_interp.ml
+++ b/src/kernel_services/analysis/logic_interp.ml
@@ -27,14 +27,43 @@ open Cil_datatype
exception Error of Cil_types.location * string
exception Unbound of string
-let find_var kf x =
+let find_var kf kinstr ?label ~var =
let vi =
- try Globals.Vars.find_from_astinfo x (VLocal kf)
+ try
+ let vi = Globals.Vars.find_from_astinfo var (VLocal kf) in
+ (match kinstr with
+ | Kglobal -> vi (* don't refine search: the Kglobal here
+ does not indicate the function contract, but merely
+ the fact that we do not have any information about
+ the targeted program point. Hence, no scope check
+ can be performed or we might reject many legitimate
+ terms and predicates.
+ *)
+ | Kstmt stmt ->
+ let scope =
+ match label with
+ | None | Some "Here" | Some "Post" | Some "Old" -> stmt
+ | Some "Pre" -> raise Not_found (* no local variable in scope. *)
+ | Some "Init" -> raise Not_found (* no local variable in scope. *)
+ | Some "LoopEntry" | Some "LoopCurrent" ->
+ if not (Kernel_function.stmt_in_loop kf stmt) then
+ Kernel.fatal
+ "Use of LoopEntry or LoopCurrent outside of a loop";
+ Kernel_function.find_enclosing_loop kf stmt
+ | Some l ->
+ (try let s = Kernel_function.find_label kf l in !s
+ with Not_found ->
+ Kernel.fatal
+ "Use of label %s that does not exist in function %a"
+ l Kernel_function.pretty kf)
+ in
+ if Kernel_function.var_is_in_scope scope vi then vi
+ else raise Not_found)
with Not_found ->
try
- Globals.Vars.find_from_astinfo x (VFormal kf)
+ Globals.Vars.find_from_astinfo var (VFormal kf)
with Not_found ->
- Globals.Vars.find_from_astinfo x VGlobal
+ Globals.Vars.find_from_astinfo var VGlobal
in
cvar_to_lvar vi
@@ -46,18 +75,21 @@ let find_var kf x =
module DefaultLT (X:
sig
val kf: Kernel_function.t
- val in_loop: bool (* Only useful for code annotations *)
+ val kinstr: Cil_types.kinstr
end) =
Logic_typing.Make
(struct
let anonCompFieldName = Cabs2cil.anonCompFieldName
let conditionalConversion = Cabs2cil.logicConditionalConversion
- let is_loop () = X.in_loop
+ let is_loop () =
+ match X.kinstr with
+ | Kglobal -> false
+ | Kstmt s -> Kernel_function.stmt_in_loop X.kf s
let find_macro _ = raise Not_found
- let find_var x = find_var X.kf x
+ let find_var ?label ~var = find_var X.kf X.kinstr ?label ~var
let find_enum_tag x =
try
@@ -118,7 +150,7 @@ let code_annot kf stmt s =
sync_typedefs ();
let module LT = DefaultLT(struct
let kf = kf
- let in_loop = Kernel_function.stmt_in_loop kf stmt
+ let kinstr = Kstmt stmt
end) in
let loc = Stmt.loc stmt in
let pa =
@@ -141,7 +173,7 @@ let term kf ?(loc=Location.unknown) ?(env=default_term_env ()) s =
sync_typedefs ();
let module LT = DefaultLT(struct
let kf = kf
- let in_loop = false (* unused *)
+ let kinstr = Kglobal
end) in
let pa_expr = Extlib.opt_map snd (Logic_lexer.lexpr (fst loc, s)) in
let parse pa_expr = LT.term env pa_expr in
@@ -156,7 +188,7 @@ let predicate kf ?(loc=Location.unknown) ?(env=default_term_env ()) s =
sync_typedefs ();
let module LT = DefaultLT(struct
let kf = kf
- let in_loop = false (* unused *)
+ let kinstr = Kglobal
end) in
let pa_expr = Extlib.opt_map snd (Logic_lexer.lexpr (fst loc, s)) in
let parse pa_expr = LT.predicate env pa_expr in
diff --git a/src/kernel_services/ast_data/kernel_function.ml b/src/kernel_services/ast_data/kernel_function.ml
index 1d7d7d982b0..8e876e4d23b 100644
--- a/src/kernel_services/ast_data/kernel_function.ml
+++ b/src/kernel_services/ast_data/kernel_function.ml
@@ -425,6 +425,12 @@ let find_syntactic_callsites kf =
try CallSites.find table kf
with Not_found -> []
+let var_is_in_scope stmt vi =
+ let blocks = find_all_enclosing_blocks stmt in
+ List.exists
+ (fun b -> List.exists (Cil_datatype.Varinfo.equal vi) b.blocals)
+ blocks
+
(* ************************************************************************* *)
(** {2 Checkers} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/ast_data/kernel_function.mli b/src/kernel_services/ast_data/kernel_function.mli
index d6700783c49..18c1dac1287 100644
--- a/src/kernel_services/ast_data/kernel_function.mli
+++ b/src/kernel_services/ast_data/kernel_function.mli
@@ -127,6 +127,14 @@ val find_syntactic_callsites : t -> (t * stmt) list
[stmt].
@since Carbon-20110201 *)
+val var_is_in_scope: stmt -> varinfo -> bool
+ (** [var_is_in_scope kf stmt vi] returns [true] iff the local variable [vi]
+ is syntactically visible from statement [stmt] in function [kf]. Note
+ that on the contrary to {!Globals.Syntactic_search.find_in_scope}, the
+ variable is searched according to its [vid], not its [vorig_name].
+
+ @since Frama-C+dev *)
+
(* ************************************************************************* *)
(** {2 Checkers} *)
(* ************************************************************************* *)
--
GitLab