diff --git a/src/kernel_services/analysis/logic_deps.ml b/src/kernel_services/analysis/logic_deps.ml
new file mode 100644
index 0000000000000000000000000000000000000000..0087286b5bc9bdf5b34ed17042dd17b79666bbed
--- /dev/null
+++ b/src/kernel_services/analysis/logic_deps.ml
@@ -0,0 +1,626 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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
+open Cil_types
+open Cil_datatype
+
+exception NYI of string
+let not_yet_implemented = ref ""
+
+(** [compute_term_deps] is provided by Eva; computes the memory zone on which a
+ term depends. *)
+let compute_term_deps = ref (fun _stmt _expr -> None)
+
+(* Reimport here the type definitions of Db.Properties.Interp. See
+ documentation there. *)
+type ctx = Db.Properties.Interp.To_zone.t_ctx =
+ {state_opt:bool option;
+ ki_opt:(stmt * bool) option;
+ kf:Kernel_function.t}
+
+type pragmas = Db.Properties.Interp.To_zone.t_pragmas =
+ {ctrl: Stmt.Set.t ; stmt: Stmt.Set.t}
+
+type t = Db.Properties.Interp.To_zone.t
+= {before:bool ; ki:stmt ; zone:Locations.Zone.t}
+type zone_info = Db.Properties.Interp.To_zone.t_zone_info
+
+type decl = Db.Properties.Interp.To_zone.t_decl =
+ {var: Varinfo.Set.t ; lbl: Logic_label.Set.t}
+
+let mk_ctx_func_contrat kf ~state_opt =
+ { state_opt = state_opt;
+ ki_opt = None;
+ kf = kf }
+
+let mk_ctx_stmt_contrat kf ki ~state_opt =
+ { state_opt=state_opt;
+ ki_opt= Some(ki, false);
+ kf = kf }
+
+let mk_ctx_stmt_annot kf ki =
+ { state_opt = Some true;
+ ki_opt = Some(ki, true);
+ kf = kf }
+
+type result = {
+ pragmas: pragmas;
+ locals: Varinfo.Set.t;
+ labels: Logic_label.Set.t;
+ zones: (Locations.Zone.t * Locations.Zone.t) Stmt.Map.t option;
+}
+
+let empty_pragmas =
+ { ctrl = Stmt.Set.empty;
+ stmt = Stmt.Set.empty }
+
+let empty_results = {
+ pragmas = empty_pragmas;
+ locals = Varinfo.Set.empty;
+ labels = Logic_label.Set.empty;
+ zones = Some Stmt.Map.empty;
+}
+
+let add_top_zone not_yet_implemented_msg =
+ function
+ | None -> (* top zone *) None
+ | Some _ ->
+ not_yet_implemented := not_yet_implemented_msg;
+ None
+
+let add_zone ~before ki zone =
+ function
+ | None -> (* top zone *) None
+ | Some other_zones ->
+ let zone_true, zone_false =
+ try Stmt.Map.find ki other_zones
+ with Not_found -> Locations.Zone.bottom, Locations.Zone.bottom
+ in
+ let new_zone =
+ if before
+ then Locations.Zone.join zone_true zone, zone_false
+ else zone_true, Locations.Zone.join zone_false zone
+ in
+ Some (Stmt.Map.add ki new_zone other_zones)
+
+let get_result result =
+ let zones =
+ match result.zones with
+ | None -> None
+ | Some other_zones ->
+ let zones =
+ Stmt.Map.to_seq other_zones |>
+ Seq.flat_map (fun (ki, (zone_true, zone_false)) ->
+ List.to_seq [
+ { before=false; ki; zone=zone_false } ;
+ { before=true; ki; zone=zone_true }
+ ]) |>
+ Seq.filter (fun x ->
+ not (Locations.Zone.equal Locations.Zone.bottom x.zone)) |>
+ List.of_seq
+ in
+ Some zones
+ in
+ zones, {var = result.locals; lbl = result.labels}
+
+let get_annot_result result =
+ get_result result, result.pragmas
+
+(** Logic_var utility: *)
+let extract_locals logicvars =
+ Logic_var.Set.fold
+ (fun lv cvars -> match lv.lv_origin with
+ | None -> cvars
+ | Some cvar ->
+ if cvar.Cil_types.vglob then cvars
+ else Varinfo.Set.add cvar cvars)
+ logicvars
+ Varinfo.Set.empty
+
+(** Term utility:
+ Extract C local variables occurring into a [term]. *)
+let extract_locals_from_term term =
+ extract_locals (extract_free_logicvars_from_term term)
+
+(** Predicate utility:
+ Extract C local variables occurring into a [term]. *)
+let extract_locals_from_pred pred =
+ extract_locals (extract_free_logicvars_from_predicate pred)
+
+type abs_label = | AbsLabel_here
+ | AbsLabel_pre
+ | AbsLabel_post
+ | AbsLabel_init
+ | AbsLabel_loop_entry
+ | AbsLabel_loop_current
+ | AbsLabel_stmt of stmt
+
+let is_same_label absl l =
+ match absl, l with
+ | AbsLabel_stmt s1, StmtLabel s2 -> Cil_datatype.Stmt.equal s1 !s2
+ | AbsLabel_here, BuiltinLabel Here -> true
+ | AbsLabel_pre, BuiltinLabel Pre -> true
+ | AbsLabel_post, BuiltinLabel Post -> true
+ | AbsLabel_init, BuiltinLabel Init -> true
+ | AbsLabel_loop_entry, BuiltinLabel LoopEntry -> true
+ | AbsLabel_loop_current, BuiltinLabel LoopCurrent -> true
+ | _, (StmtLabel _ | FormalLabel _ | BuiltinLabel _) -> false
+
+
+let populate_zone ctx visit cil_node current_zones =
+ let { state_opt=before_opt; ki_opt; kf } = ctx in
+ (* interpretation from the
+ - pre-state if [before_opt=Some true]
+ - post-state if [before_opt=Some false]
+ - pre-state with possible reference to the post-state if
+ [before_opt=None] of a property relative to
+ - the contract of function [kf] when [ki_opt=None]
+ otherwise [ki_opt=Some(ki, code_annot)],
+ - the contract of the statement [ki] when [code_annot=false]
+ - the annotation of the statement [ki] when [code_annot=true] *)
+ let vis = object(self)
+ inherit Visitor.frama_c_inplace
+ val mutable current_label = AbsLabel_here
+ val mutable zones = current_zones
+ method get_zones = zones
+
+ method private get_ctrl_point () =
+ let get_fct_entry_point () =
+ (* TODO: to replace by true, None *)
+ true,
+ (try Some (Kernel_function.find_first_stmt kf)
+ with Kernel_function.No_Statement ->
+ (* raised when [kf] has no code. *)
+ None)
+ in
+ let get_ctrl_point dft =
+ let before = Option.value ~default:dft before_opt in
+ match ki_opt with
+ | None -> (* function contract *)
+
+ if before then get_fct_entry_point ()
+ else before, None
+ (* statement contract *)
+ | Some (ki,_) -> (* statement contract and code annotation *)
+ before, Some ki
+ in
+ let result = match current_label with
+ | AbsLabel_stmt stmt -> true, Some stmt
+ | AbsLabel_pre -> get_fct_entry_point ()
+ | AbsLabel_here -> get_ctrl_point true
+ | AbsLabel_post -> get_ctrl_point false
+ | AbsLabel_init -> raise (NYI "[logic_interp] Init label")
+ | AbsLabel_loop_current ->
+ raise (NYI "[logic_interp] LoopCurrent label")
+ | AbsLabel_loop_entry ->
+ raise (NYI "[logic_interp] LoopEntry label")
+ in (* TODO: the method should be able to return result directly *)
+ match result with
+ | current_before, Some current_stmt -> current_before, current_stmt
+ | _ -> raise (NYI
+ "[logic_interp] clause related to a function contract")
+
+ method private change_label: 'a.abs_label -> 'a -> 'a visitAction =
+ fun label x ->
+ let old_label = current_label in
+ current_label <- label;
+ ChangeDoChildrenPost
+ (x,fun x -> current_label <- old_label; x)
+
+ method private change_label_to_here: 'a.'a -> 'a visitAction =
+ fun x ->
+ self#change_label AbsLabel_here x
+
+ method private change_label_to_old: 'a.'a -> 'a visitAction =
+ fun x ->
+ match ki_opt,before_opt with
+ (* function contract *)
+ | None,Some true ->
+ failwith "The use of the label Old is forbidden inside clauses \
+ related to the pre-state of function contracts."
+ | None,None
+ | None,Some false ->
+ (* refers to the pre-state of the contract. *)
+ self#change_label AbsLabel_pre x
+ (* statement contract *)
+ | Some (_ki,false),Some true ->
+ failwith "The use of the label Old is forbidden inside clauses \
+ related to the pre-state of statement contracts."
+ | Some (ki,false),None
+ | Some (ki,false),Some false ->
+ (* refers to the pre-state of the contract. *)
+ self#change_label (AbsLabel_stmt ki) x
+ (* code annotation *)
+ | Some (_ki,true),None
+ | Some (_ki,true),Some _ ->
+ (* refers to the pre-state of the function contract. *)
+ self#change_label AbsLabel_pre x
+
+ method private change_label_to_post: 'a.'a -> 'a visitAction =
+ fun x ->
+ (* allowed when [before_opt=None] for function/statement contracts *)
+ match ki_opt,before_opt with
+ (* function contract *)
+ | None,Some _ ->
+ failwith "Function contract where the use of the label Post is \
+ forbidden."
+ | None,None ->
+ (* refers to the post-state of the contract. *)
+ self#change_label AbsLabel_post x
+ (* statement contract *)
+ | Some (_ki,false),Some _ ->
+ failwith "Statement contract where the use of the label Post is \
+ forbidden."
+ | Some (_ki,false),None ->
+ (* refers to the pre-state of the contract. *)
+ self#change_label AbsLabel_post x
+ (* code annotation *)
+ | Some (_ki,true), _ ->
+ failwith "The use of the label Post is forbidden inside code \
+ annotations."
+
+ method private change_label_to_pre: 'a.'a -> 'a visitAction =
+ fun x ->
+ match ki_opt with
+ (* function contract *)
+ | None ->
+ failwith "The use of the label Pre is forbidden inside function \
+ contracts."
+ (* statement contract *)
+ (* code annotation *)
+ | Some _ ->
+ (* refers to the pre-state of the function contract. *)
+ self#change_label AbsLabel_pre x
+
+ method private change_label_aux: 'a. _ -> 'a -> 'a visitAction =
+ fun lbl x -> self#change_label lbl x
+
+ method private change_label_to_stmt: 'a.stmt -> 'a -> 'a visitAction =
+ fun stmt x ->
+ match ki_opt with
+ (* function contract *)
+ | None ->
+ failwith "the use of C labels is forbidden inside clauses related \
+ to function contracts."
+ (* statement contract *)
+ (* code annotation *)
+ | Some _ ->
+ (* refers to the state at the C label of the statement [stmt]. *)
+ self#change_label (AbsLabel_stmt stmt) x
+
+
+ method! vpredicate_node p =
+ let fail () =
+ raise (NYI (Format.asprintf
+ "[logic_interp] %a" Printer.pp_predicate_node p))
+ in
+ match p with
+ | Pat (_, BuiltinLabel Old) -> self#change_label_to_old p
+ | Pat (_, BuiltinLabel Here) -> self#change_label_to_here p
+ | Pat (_, BuiltinLabel Pre) -> self#change_label_to_pre p
+ | Pat (_, BuiltinLabel Post) -> self#change_label_to_post p
+ | Pat (_, BuiltinLabel Init) ->
+ self#change_label_aux AbsLabel_init p
+ | Pat (_, BuiltinLabel LoopCurrent) ->
+ self#change_label_aux AbsLabel_loop_current p
+ | Pat (_, BuiltinLabel LoopEntry) ->
+ self#change_label_aux AbsLabel_loop_entry p
+ | Pat (_, FormalLabel s) ->
+ failwith ("unknown logic label" ^ s)
+ | Pat (_, StmtLabel st) -> self#change_label_to_stmt !st p
+ | Pfalse | Ptrue | Prel _ | Pand _ | Por _ | Pxor _ | Pimplies _
+ | Piff _ | Pnot _ | Pif _ | Plet _ | Pforall _ | Pexists _
+ | Papp (_, [], _) (* No label, thus cannot access memory *)
+ | Pseparated _ (* need only to preserve the values of each pointer *)
+ -> DoChildren
+
+ | Pinitialized (lbl, t) | Pdangling (lbl, t) ->
+ (* Dependencies of [\initialized(p)] or [\dangling(p)] are the
+ dependencies of [*p]. *)
+ if is_same_label current_label lbl then (
+ let typ = Logic_typing.type_of_pointed t.term_type in
+ let tlv = Cil.mkTermMem ~addr:t ~off:TNoOffset in
+ let tlv' = Logic_const.term (TLval tlv) typ in
+ self#do_term_lval tlv';
+ DoChildren
+ )
+ else fail ()
+
+ | Pvalid_read (_lbl, _) | Pvalid (_lbl, _) ->
+ (* Does not take dynamic allocation into account, but then
+ Value does not either. [lbl] can be ignored because they are
+ taken into account by the functions [from_...] below *)
+ DoChildren
+
+ | Pobject_pointer _ | Pvalid_function _ ->
+ DoChildren
+
+ | Papp _ | Pallocable _ | Pfreeable _ | Pfresh _
+ -> fail ()
+
+ method private do_term_lval t =
+ let current_before, current_stmt = self#get_ctrl_point () in
+ match !compute_term_deps current_stmt t with
+ | Some zone ->
+ let filter = function Base.CLogic_Var _ -> false | _ -> true in
+ let zone = Locations.Zone.filter_base filter zone in
+ zones <- add_zone ~before:current_before current_stmt zone zones
+ | None ->
+ raise (NYI "[logic_interp] dependencies of a term lval")
+
+ method! vterm t =
+ match t.term_node with
+ | TAddrOf _ | TLval (TMem _,_)
+ | TLval(TVar {lv_origin = Some _},_) | TStartOf _ ->
+ self#do_term_lval t;
+ SkipChildren
+ | Tat (_, BuiltinLabel Old) -> self#change_label_to_old t
+ | Tat (_, BuiltinLabel Here) -> self#change_label_to_here t
+ | Tat (_, BuiltinLabel Pre) -> self#change_label_to_pre t
+ | Tat (_, BuiltinLabel Post) -> self#change_label_to_post t
+ | Tat (_, BuiltinLabel Init) ->
+ self#change_label_aux AbsLabel_init t
+ | Tat (_, BuiltinLabel LoopCurrent) ->
+ self#change_label_aux AbsLabel_loop_current t
+ | Tat (_, BuiltinLabel LoopEntry) ->
+ self#change_label_aux AbsLabel_loop_entry t
+ | Tat (_, StmtLabel st) -> self#change_label_to_stmt !st t
+ | Tat (_, FormalLabel s) ->
+ failwith ("unknown logic label" ^ s)
+ | TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _ | TAlignOfE _ ->
+ (* These are static constructors, there are no dependencies here *)
+ SkipChildren
+ | _ -> DoChildren
+ end
+ in
+ try
+ ignore (visit (vis :> Visitor.frama_c_inplace) cil_node);
+ vis#get_zones
+ with NYI msg ->
+ add_top_zone msg (vis#get_zones)
+
+let update_pragmas f results =
+ { results with pragmas = f results.pragmas }
+
+let add_ctrl_pragma stmt =
+ update_pragmas (fun x -> { x with ctrl = Stmt.Set.add stmt x.ctrl })
+
+let add_stmt_pragma stmt =
+ update_pragmas (fun x -> { x with stmt = Stmt.Set.add stmt x.stmt })
+
+let add_results_from_term ctx results t =
+ let zones = populate_zone ctx Visitor.visitFramacTerm t results.zones in
+ {
+ results with
+ zones;
+ locals = Varinfo.Set.union (extract_locals_from_term t) results.locals;
+ labels = Logic_label.Set.union (extract_labels_from_term t) results.labels
+ }
+
+let add_results_from_pred ctx results p =
+ let zones = populate_zone ctx Visitor.visitFramacPredicate p results.zones in
+ {
+ results with
+ zones;
+ locals = Varinfo.Set.union (extract_locals_from_pred p) results.locals;
+ labels = Logic_label.Set.union (extract_labels_from_pred p) results.labels
+ }
+
+(** Entry point to get the list of [ki] * [Locations.Zone.t]
+ needed to evaluate the list of [terms]
+ relative to the [ctx] of interpretation. *)
+let from_terms terms ctx =
+ List.fold_left (add_results_from_term ctx) empty_results terms |>
+ get_result
+
+(** Entry point to get the list of [ki] * [Locations.Zone.t]
+ needed to evaluate the [term]
+ relative to the [ctx] of interpretation. *)
+let from_term term ctx =
+ add_results_from_term ctx empty_results term |>
+ get_result
+
+(** Entry point to get the list of [ki] * [Locations.Zone.t]
+ needed to evaluate the list of [preds]
+ relative to the [ctx] of interpretation. *)
+let from_preds preds ctx =
+ List.fold_left (add_results_from_pred ctx) empty_results preds |>
+ get_result
+
+(** Entry point to get the list of [ki] * [Locations.Zone.t]
+ needed to evaluate the [pred]
+ relative to the [ctx] of interpretation. *)
+let from_pred pred ctx =
+ add_results_from_pred ctx empty_results pred |>
+ get_result
+
+(** Used by annotations entry points. *)
+let get_zone_from_annot a (ki,kf) loop_body_opt results =
+ let get_zone_from_term k term results =
+ let ctx = { state_opt = Some true; ki_opt = Some (k, true); kf } in
+ add_results_from_term ctx results term
+ and get_zone_from_pred k pred results =
+ let ctx = { state_opt = Some true; ki_opt = Some (k, true); kf } in
+ add_results_from_pred ctx results pred
+ in
+ match a.annot_content with
+ | APragma (Slice_pragma (SPexpr term) | Impact_pragma (IPexpr term)) ->
+ results |>
+ (* to preserve the interpretation of the pragma *)
+ get_zone_from_term ki term |>
+ (* to select the reachability of the pragma *)
+ add_ctrl_pragma ki
+ | APragma (Slice_pragma SPctrl) ->
+ (* to select the reachability of the pragma *)
+ add_ctrl_pragma ki results
+ | APragma (Slice_pragma SPstmt | Impact_pragma IPstmt) ->
+ (* to preserve the effect of the statement *)
+ add_stmt_pragma ki results
+ | AAssert (_behav,pred) ->
+ (* to preserve the interpretation of the assertion *)
+ get_zone_from_pred ki pred.tp_statement results
+ | AInvariant (_behav,true,pred) -> (* loop invariant *)
+ (* WARNING this is obsolete *)
+ (* [JS 2010/09/02] TODO: so what is the right way to do? *)
+ (* to preserve the interpretation of the loop invariant *)
+ get_zone_from_pred (Option.get loop_body_opt) pred.tp_statement results
+ | AInvariant (_behav,false,pred) -> (* code invariant *)
+ (* to preserve the interpretation of the code invariant *)
+ get_zone_from_pred ki pred.tp_statement results
+ | AVariant (term,_) ->
+ (* to preserve the interpretation of the variant *)
+ get_zone_from_term (Option.get loop_body_opt) term results
+ | APragma (Loop_pragma (Unroll_specs terms))
+ | APragma (Loop_pragma (Widen_hints terms))
+ | APragma (Loop_pragma (Widen_variables terms)) ->
+ (* to select the declaration of the variables *)
+ List.fold_left
+ (fun results term -> {
+ results with
+ locals = Varinfo.Set.union (extract_locals_from_term term) results.locals;
+ labels = Logic_label.Set.union (extract_labels_from_term term) results.labels
+ })
+ results terms
+ | AAllocation (_,FreeAllocAny) -> results
+ | AAllocation (_,FreeAlloc(f,a)) ->
+ let get_zone results x =
+ get_zone_from_term (Option.get loop_body_opt) x.it_content results
+ in
+ let results = List.fold_left get_zone results f in
+ let results = List.fold_left get_zone results a in
+ results
+ | AAssigns (_, WritesAny) -> results
+ | AAssigns (_, Writes l) -> (* loop assigns *)
+ let get_zone results x =
+ get_zone_from_term (Option.get loop_body_opt) x.it_content results
+ in
+ List.fold_left
+ (fun results (zone,deps) ->
+ let results = get_zone results zone in
+ match deps with
+ FromAny -> results
+ | From l -> List.fold_left get_zone results l)
+ results l
+ | AStmtSpec _ -> (* TODO *)
+ raise (NYI "[logic_interp] statement contract")
+ | AExtended _ -> raise (NYI "[logic_interp] extension")
+
+(* Used by annotations entry points. *)
+let get_from_stmt_annots code_annot_filter ((ki, _kf) as stmt) results =
+ Option.fold
+ ~none:results
+ ~some:(fun caf ->
+ let loop_body_opt = match ki.skind with
+ | Loop(_, { bstmts = body :: _ }, _, _, _) -> Some body
+ | _ -> None
+ in
+ Annotations.fold_code_annot
+ (fun _ a results ->
+ if caf a
+ then get_zone_from_annot a stmt loop_body_opt results
+ else results)
+ ki results)
+ code_annot_filter
+
+(** Used by annotations entry points. *)
+let from_ki_annot annot ((ki, _kf) as stmt) =
+ let real_ki = match ki.skind with
+ Loop(_,{bstmts = loop_entry::_},_,_,_) -> Some loop_entry
+ | _ -> None
+ in
+ get_zone_from_annot annot stmt real_ki
+
+(** Entry point to get the list of [ki] * [Locations.Zone.t]
+ needed to evaluate the code annotations related to this [stmt]. *)
+let from_stmt_annot annot stmt =
+ from_ki_annot annot stmt empty_results |>
+ get_annot_result
+
+(** Entry point to get the list of [ki] * [Locations.Zone.t]
+ needed to evaluate the code annotations related to this [stmt]. *)
+let from_stmt_annots code_annot_filter stmt =
+ get_from_stmt_annots code_annot_filter stmt empty_results |>
+ get_annot_result
+
+(** Entry point to get the list of [ki] * [Locations.Zone.t]
+ needed to evaluate the code annotations related to this [kf]. *)
+let from_func_annots iter_on_kf_stmt code_annot_filter kf =
+ let results = ref empty_results in
+ let from_stmt_annots ki =
+ results := get_from_stmt_annots code_annot_filter (ki, kf) !results
+ in
+ iter_on_kf_stmt from_stmt_annots kf;
+ get_annot_result !results
+
+(** To quickly build a annotation filter *)
+let code_annot_filter annot ~threat ~user_assert ~slicing_pragma ~loop_inv ~loop_var ~others =
+ match annot.annot_content with
+ | APragma (Slice_pragma _) -> slicing_pragma
+ | AAssert _ ->
+ (match Alarms.find annot with
+ | None -> user_assert
+ | Some _a -> threat)
+ | AVariant _ -> loop_var
+ | AInvariant(_behav,true,_pred) -> loop_inv
+ | AInvariant(_,false,_) -> others
+ | AAllocation _ -> others
+ | AAssigns _ -> others
+ | APragma (Loop_pragma _)| APragma (Impact_pragma _) -> others
+ | AStmtSpec _ | AExtended _ (* TODO *) -> false
+
+
+exception Prune
+
+let to_result_from_pred p =
+ let visitor = object (_self)
+ inherit Visitor.frama_c_inplace
+
+ method! vterm_lhost t =
+ match t with
+ | TResult _ -> raise Prune
+ | _ -> DoChildren
+
+ end
+ in
+ (try
+ ignore(Visitor.visitFramacPredicate visitor p);
+ false
+ with Prune ->
+ true)
+
+
+let () =
+ Db.Properties.Interp.To_zone.code_annot_filter := code_annot_filter;
+ Db.Properties.Interp.To_zone.mk_ctx_func_contrat := mk_ctx_func_contrat;
+ Db.Properties.Interp.To_zone.mk_ctx_stmt_contrat := mk_ctx_stmt_contrat;
+ Db.Properties.Interp.To_zone.mk_ctx_stmt_annot := mk_ctx_stmt_annot;
+
+ Db.Properties.Interp.To_zone.from_term := from_term;
+ Db.Properties.Interp.To_zone.from_terms := from_terms;
+ Db.Properties.Interp.To_zone.from_pred := from_pred;
+ Db.Properties.Interp.To_zone.from_preds := from_preds;
+ Db.Properties.Interp.To_zone.from_stmt_annot := from_stmt_annot;
+ Db.Properties.Interp.To_zone.from_stmt_annots := from_stmt_annots;
+ Db.Properties.Interp.To_zone.from_func_annots := from_func_annots;
+
+ Db.Properties.Interp.to_result_from_pred := to_result_from_pred;
diff --git a/src/kernel_services/analysis/logic_deps.mli b/src/kernel_services/analysis/logic_deps.mli
new file mode 100644
index 0000000000000000000000000000000000000000..fa485d47605aa6940c809fe51c0e5fbbd4820d4e
--- /dev/null
+++ b/src/kernel_services/analysis/logic_deps.mli
@@ -0,0 +1,96 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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
+
+val compute_term_deps: (stmt -> term -> Locations.Zone.t option) ref
+
+type ctx = Db.Properties.Interp.To_zone.t_ctx
+
+val mk_ctx_func_contrat: kernel_function -> state_opt:bool option -> ctx
+(** To build an interpretation context relative to function
+ contracts. *)
+
+val mk_ctx_stmt_contrat: kernel_function -> stmt -> state_opt:bool option -> ctx
+(** To build an interpretation context relative to statement
+ contracts. *)
+
+val mk_ctx_stmt_annot: kernel_function -> stmt -> ctx
+(** To build an interpretation context relative to statement
+ annotations. *)
+
+type t = Db.Properties.Interp.To_zone.t
+type zone_info = Db.Properties.Interp.To_zone.t_zone_info
+(** list of zones at some program points.
+ * None means that the computation has failed. *)
+
+type decl = Db.Properties.Interp.To_zone.t_decl
+type pragmas = Db.Properties.Interp.To_zone.t_pragmas
+
+val from_term: term -> ctx -> zone_info * decl
+(** Entry point to get zones needed to evaluate the [term] relative to
+ the [ctx] of interpretation. *)
+
+val from_terms: term list -> ctx -> zone_info * decl
+(** Entry point to get zones needed to evaluate the list of [terms]
+ relative to the [ctx] of interpretation. *)
+
+val from_pred: predicate -> ctx -> zone_info * decl
+(** Entry point to get zones needed to evaluate the [predicate]
+ relative to the [ctx] of interpretation. *)
+
+val from_preds: predicate list -> ctx -> zone_info * decl
+(** Entry point to get zones needed to evaluate the list of
+ [predicates] relative to the [ctx] of interpretation. *)
+
+val from_stmt_annot:
+ code_annotation -> stmt * kernel_function ->
+ (zone_info * decl) * pragmas
+(** Entry point to get zones needed to evaluate an annotation on the
+ given stmt. *)
+
+val from_stmt_annots:
+ (code_annotation -> bool) option ->
+ stmt * kernel_function -> (zone_info * decl) * pragmas
+(** Entry point to get zones needed to evaluate annotations of this
+ [stmt]. *)
+
+val from_func_annots:
+ ((stmt -> unit) -> kernel_function -> unit) ->
+ (code_annotation -> bool) option ->
+ kernel_function -> (zone_info * decl) * pragmas
+(** Entry point to get zones
+ needed to evaluate annotations of this [kf]. *)
+
+val code_annot_filter:
+ code_annotation ->
+ threat:bool -> user_assert:bool -> slicing_pragma:bool ->
+ loop_inv:bool -> loop_var:bool -> others:bool -> bool
+(** To quickly build an annotation filter *)
+
+(** Does the interpretation of the predicate rely on the interpretation
+ of the term result? *)
+val to_result_from_pred: predicate -> bool
+
+(** The follow declarations are kept for compatibility and should not be used *)
+exception NYI of string
+val not_yet_implemented: string ref
diff --git a/src/kernel_services/analysis/logic_interp.ml b/src/kernel_services/analysis/logic_interp.ml
index c2545b30ac9ab205c9cacb82fe05ad423b6a2927..6c96f61d9b9a3b34dd459b0776c136894184fb06 100644
--- a/src/kernel_services/analysis/logic_interp.ml
+++ b/src/kernel_services/analysis/logic_interp.ml
@@ -20,699 +20,10 @@
(* *)
(**************************************************************************)
-open Cil
-open Cil_types
-open Cil_datatype
-
exception Error = Logic_parse_string.Error
-
-(** Utilities to identify [Locations.Zone.t] involved into
- [code_annotation]. *)
-module To_zone : sig
-
- type ctx = Db.Properties.Interp.To_zone.t_ctx =
- {state_opt:bool option;
- ki_opt:(stmt * bool) option;
- kf:Kernel_function.t}
-
- val mk_ctx_func_contrat: kernel_function -> state_opt:bool option -> ctx
- (** [mk_ctx_func_contrat] to define an interpretation context related to
- [kernel_function] contracts.
- The control point of the interpretation is defined as follows:
- - pre-state if [state_opt=Some true]
- - post-state if [state_opt=Some false]
- - pre-state with possible reference to the post-state if
- [state_opt=None]. *)
-
- val mk_ctx_stmt_contrat:
- kernel_function -> stmt -> state_opt:bool option -> ctx
- (** [mk_ctx_stmt_contrat] to define an interpretation context related to
- [stmt] contracts.
- The control point of the interpretation is defined as follows:
- - pre-state if [state_opt=Some true]
- - post-state if [state_opt=Some false]
- - pre-state with possible reference to the post-state if
- [state_opt=None]. *)
-
- val mk_ctx_stmt_annot: kernel_function -> stmt -> ctx
- (** [mk_ctx_stmt_annot] to define an interpretation context related to an
- annotation attached before the [stmt]. *)
-
- type zone_info = Db.Properties.Interp.To_zone.t_zone_info
- type decl = Db.Properties.Interp.To_zone.t_decl
- type pragmas = Db.Properties.Interp.To_zone.t_pragmas
- val not_yet_implemented : string ref
- exception NYI of string
-
- val compute_term_deps: (stmt -> term -> Locations.Zone.t option) ref
- (** Provided by Eva, compute the memory zone on which a term depends. *)
-
- val from_term: term -> ctx -> (zone_info * decl)
- (** Entry point to get zones
- needed to evaluate the [term] relative to the [ctx] of
- interpretation. *)
-
- val from_terms: term list -> ctx -> (zone_info * decl)
- (** Entry point to get zones
- needed to evaluate the list of [terms] relative to the [ctx] of
- interpretation. *)
-
- val from_pred: predicate -> ctx -> (zone_info * decl)
- (** Entry point to get zones
- needed to evaluate the [predicate] relative to the [ctx] of
- interpretation. *)
-
- val from_preds: predicate list -> ctx -> (zone_info * decl)
- (** Entry point to get zones
- needed to evaluate the list of [predicates] relative to the [ctx] of
- interpretation. *)
-
- val from_stmt_annot:
- code_annotation -> (stmt * kernel_function) ->
- (zone_info * decl) * pragmas
- (** Entry point to get zones needed to evaluate code annotations of this
- [stmt]. *)
-
- val from_stmt_annots:
- (code_annotation -> bool) option ->
- (stmt * kernel_function) -> (zone_info * decl) * pragmas
- (** Entry point to get zones needed to evaluate code annotations of this
- [stmt]. *)
-
- val from_func_annots:
- ((stmt -> unit) -> kernel_function -> unit) ->
- (code_annotation -> bool) option ->
- kernel_function -> (zone_info * decl) * pragmas
- (** Entry point to get zones needed to evaluate code annotations of this
- [kf]. *)
-
- val code_annot_filter:
- code_annotation ->
- threat:bool -> user_assert:bool -> slicing_pragma:bool ->
- loop_inv:bool -> loop_var:bool -> others:bool -> bool
- (** To quickly build a annotation filter *)
-end
-=
+module To_zone =
struct
-
- exception NYI of string
- (* Reimport here the type definitions of Db.Properties.Interp. See
- documentation there. *)
- type ctx = Db.Properties.Interp.To_zone.t_ctx =
- {state_opt:bool option;
- ki_opt:(stmt * bool) option;
- kf:Kernel_function.t}
-
- type pragmas = Db.Properties.Interp.To_zone.t_pragmas =
- {ctrl: Stmt.Set.t ; stmt: Stmt.Set.t}
-
- type t = Db.Properties.Interp.To_zone.t
- = {before:bool ; ki:stmt ; zone:Locations.Zone.t}
- type zone_info = Db.Properties.Interp.To_zone.t_zone_info
-
- type decl = Db.Properties.Interp.To_zone.t_decl =
- {var: Varinfo.Set.t ; lbl: Logic_label.Set.t}
-
- let mk_ctx_func_contrat kf ~state_opt =
- { state_opt = state_opt;
- ki_opt = None;
- kf = kf }
-
- let mk_ctx_stmt_contrat kf ki ~state_opt =
- { state_opt=state_opt;
- ki_opt= Some(ki, false);
- kf = kf }
-
- let mk_ctx_stmt_annot kf ki =
- { state_opt = Some true;
- ki_opt = Some(ki, true);
- kf = kf }
-
- type result = {
- pragmas: pragmas;
- locals: Varinfo.Set.t;
- labels: Logic_label.Set.t;
- zones: (Locations.Zone.t * Locations.Zone.t) Stmt.Map.t option;
- }
-
- let empty_pragmas =
- { ctrl = Stmt.Set.empty;
- stmt = Stmt.Set.empty }
-
- let empty_results = {
- pragmas = empty_pragmas;
- locals = Varinfo.Set.empty;
- labels = Logic_label.Set.empty;
- zones = Some Stmt.Map.empty;
- }
-
- let not_yet_implemented = ref ""
-
- let compute_term_deps = ref (fun _stmt _expr -> None)
-
- let add_top_zone not_yet_implemented_msg =
- function
- | None -> (* top zone *) None
- | Some _ ->
- not_yet_implemented := not_yet_implemented_msg;
- None
-
- let add_zone ~before ki zone =
- function
- | None -> (* top zone *) None
- | Some other_zones ->
- let zone_true, zone_false =
- try Stmt.Map.find ki other_zones
- with Not_found -> Locations.Zone.bottom, Locations.Zone.bottom
- in
- let new_zone =
- if before
- then Locations.Zone.join zone_true zone, zone_false
- else zone_true, Locations.Zone.join zone_false zone
- in
- Some (Stmt.Map.add ki new_zone other_zones)
-
- let get_result result =
- let zones =
- match result.zones with
- | None -> None
- | Some other_zones ->
- let zones =
- Stmt.Map.to_seq other_zones |>
- Seq.flat_map (fun (ki, (zone_true, zone_false)) ->
- List.to_seq [
- { before=false; ki; zone=zone_false } ;
- { before=true; ki; zone=zone_true }
- ]) |>
- Seq.filter (fun x ->
- not (Locations.Zone.equal Locations.Zone.bottom x.zone)) |>
- List.of_seq
- in
- Some zones
- in
- zones, {var = result.locals; lbl = result.labels}
-
- let get_annot_result result =
- get_result result, result.pragmas
-
- (** Logic_var utility: *)
- let extract_locals logicvars =
- Logic_var.Set.fold
- (fun lv cvars -> match lv.lv_origin with
- | None -> cvars
- | Some cvar ->
- if cvar.Cil_types.vglob then cvars
- else Varinfo.Set.add cvar cvars)
- logicvars
- Varinfo.Set.empty
-
- (** Term utility:
- Extract C local variables occurring into a [term]. *)
- let extract_locals_from_term term =
- extract_locals (extract_free_logicvars_from_term term)
-
- (** Predicate utility:
- Extract C local variables occurring into a [term]. *)
- let extract_locals_from_pred pred =
- extract_locals (extract_free_logicvars_from_predicate pred)
-
- type abs_label = | AbsLabel_here
- | AbsLabel_pre
- | AbsLabel_post
- | AbsLabel_init
- | AbsLabel_loop_entry
- | AbsLabel_loop_current
- | AbsLabel_stmt of stmt
-
- let is_same_label absl l =
- match absl, l with
- | AbsLabel_stmt s1, StmtLabel s2 -> Cil_datatype.Stmt.equal s1 !s2
- | AbsLabel_here, BuiltinLabel Here -> true
- | AbsLabel_pre, BuiltinLabel Pre -> true
- | AbsLabel_post, BuiltinLabel Post -> true
- | AbsLabel_init, BuiltinLabel Init -> true
- | AbsLabel_loop_entry, BuiltinLabel LoopEntry -> true
- | AbsLabel_loop_current, BuiltinLabel LoopCurrent -> true
- | _, (StmtLabel _ | FormalLabel _ | BuiltinLabel _) -> false
-
-
- let populate_zone ctx visit cil_node current_zones =
- let { state_opt=before_opt; ki_opt; kf } = ctx in
- (* interpretation from the
- - pre-state if [before_opt=Some true]
- - post-state if [before_opt=Some false]
- - pre-state with possible reference to the post-state if
- [before_opt=None] of a property relative to
- - the contract of function [kf] when [ki_opt=None]
- otherwise [ki_opt=Some(ki, code_annot)],
- - the contract of the statement [ki] when [code_annot=false]
- - the annotation of the statement [ki] when [code_annot=true] *)
- let vis = object(self)
- inherit Visitor.frama_c_inplace
- val mutable current_label = AbsLabel_here
- val mutable zones = current_zones
- method get_zones = zones
-
- method private get_ctrl_point () =
- let get_fct_entry_point () =
- (* TODO: to replace by true, None *)
- true,
- (try Some (Kernel_function.find_first_stmt kf)
- with Kernel_function.No_Statement ->
- (* raised when [kf] has no code. *)
- None)
- in
- let get_ctrl_point dft =
- let before = Option.value ~default:dft before_opt in
- match ki_opt with
- | None -> (* function contract *)
-
- if before then get_fct_entry_point ()
- else before, None
- (* statement contract *)
- | Some (ki,_) -> (* statement contract and code annotation *)
- before, Some ki
- in
- let result = match current_label with
- | AbsLabel_stmt stmt -> true, Some stmt
- | AbsLabel_pre -> get_fct_entry_point ()
- | AbsLabel_here -> get_ctrl_point true
- | AbsLabel_post -> get_ctrl_point false
- | AbsLabel_init -> raise (NYI "[logic_interp] Init label")
- | AbsLabel_loop_current ->
- raise (NYI "[logic_interp] LoopCurrent label")
- | AbsLabel_loop_entry ->
- raise (NYI "[logic_interp] LoopEntry label")
- in (* TODO: the method should be able to return result directly *)
- match result with
- | current_before, Some current_stmt -> current_before, current_stmt
- | _ -> raise (NYI
- "[logic_interp] clause related to a function contract")
-
- method private change_label: 'a.abs_label -> 'a -> 'a visitAction =
- fun label x ->
- let old_label = current_label in
- current_label <- label;
- ChangeDoChildrenPost
- (x,fun x -> current_label <- old_label; x)
-
- method private change_label_to_here: 'a.'a -> 'a visitAction =
- fun x ->
- self#change_label AbsLabel_here x
-
- method private change_label_to_old: 'a.'a -> 'a visitAction =
- fun x ->
- match ki_opt,before_opt with
- (* function contract *)
- | None,Some true ->
- failwith "The use of the label Old is forbidden inside clauses \
- related to the pre-state of function contracts."
- | None,None
- | None,Some false ->
- (* refers to the pre-state of the contract. *)
- self#change_label AbsLabel_pre x
- (* statement contract *)
- | Some (_ki,false),Some true ->
- failwith "The use of the label Old is forbidden inside clauses \
- related to the pre-state of statement contracts."
- | Some (ki,false),None
- | Some (ki,false),Some false ->
- (* refers to the pre-state of the contract. *)
- self#change_label (AbsLabel_stmt ki) x
- (* code annotation *)
- | Some (_ki,true),None
- | Some (_ki,true),Some _ ->
- (* refers to the pre-state of the function contract. *)
- self#change_label AbsLabel_pre x
-
- method private change_label_to_post: 'a.'a -> 'a visitAction =
- fun x ->
- (* allowed when [before_opt=None] for function/statement contracts *)
- match ki_opt,before_opt with
- (* function contract *)
- | None,Some _ ->
- failwith "Function contract where the use of the label Post is \
- forbidden."
- | None,None ->
- (* refers to the post-state of the contract. *)
- self#change_label AbsLabel_post x
- (* statement contract *)
- | Some (_ki,false),Some _ ->
- failwith "Statement contract where the use of the label Post is \
- forbidden."
- | Some (_ki,false),None ->
- (* refers to the pre-state of the contract. *)
- self#change_label AbsLabel_post x
- (* code annotation *)
- | Some (_ki,true), _ ->
- failwith "The use of the label Post is forbidden inside code \
- annotations."
-
- method private change_label_to_pre: 'a.'a -> 'a visitAction =
- fun x ->
- match ki_opt with
- (* function contract *)
- | None ->
- failwith "The use of the label Pre is forbidden inside function \
- contracts."
- (* statement contract *)
- (* code annotation *)
- | Some _ ->
- (* refers to the pre-state of the function contract. *)
- self#change_label AbsLabel_pre x
-
- method private change_label_aux: 'a. _ -> 'a -> 'a visitAction =
- fun lbl x -> self#change_label lbl x
-
- method private change_label_to_stmt: 'a.stmt -> 'a -> 'a visitAction =
- fun stmt x ->
- match ki_opt with
- (* function contract *)
- | None ->
- failwith "the use of C labels is forbidden inside clauses related \
- to function contracts."
- (* statement contract *)
- (* code annotation *)
- | Some _ ->
- (* refers to the state at the C label of the statement [stmt]. *)
- self#change_label (AbsLabel_stmt stmt) x
-
-
- method! vpredicate_node p =
- let fail () =
- raise (NYI (Format.asprintf
- "[logic_interp] %a" Printer.pp_predicate_node p))
- in
- match p with
- | Pat (_, BuiltinLabel Old) -> self#change_label_to_old p
- | Pat (_, BuiltinLabel Here) -> self#change_label_to_here p
- | Pat (_, BuiltinLabel Pre) -> self#change_label_to_pre p
- | Pat (_, BuiltinLabel Post) -> self#change_label_to_post p
- | Pat (_, BuiltinLabel Init) ->
- self#change_label_aux AbsLabel_init p
- | Pat (_, BuiltinLabel LoopCurrent) ->
- self#change_label_aux AbsLabel_loop_current p
- | Pat (_, BuiltinLabel LoopEntry) ->
- self#change_label_aux AbsLabel_loop_entry p
- | Pat (_, FormalLabel s) ->
- failwith ("unknown logic label" ^ s)
- | Pat (_, StmtLabel st) -> self#change_label_to_stmt !st p
- | Pfalse | Ptrue | Prel _ | Pand _ | Por _ | Pxor _ | Pimplies _
- | Piff _ | Pnot _ | Pif _ | Plet _ | Pforall _ | Pexists _
- | Papp (_, [], _) (* No label, thus cannot access memory *)
- | Pseparated _ (* need only to preserve the values of each pointer *)
- -> DoChildren
-
- | Pinitialized (lbl, t) | Pdangling (lbl, t) ->
- (* Dependencies of [\initialized(p)] or [\dangling(p)] are the
- dependencies of [*p]. *)
- if is_same_label current_label lbl then (
- let typ = Logic_typing.type_of_pointed t.term_type in
- let tlv = Cil.mkTermMem ~addr:t ~off:TNoOffset in
- let tlv' = Logic_const.term (TLval tlv) typ in
- self#do_term_lval tlv';
- DoChildren
- )
- else fail ()
-
- | Pvalid_read (_lbl, _) | Pvalid (_lbl, _) ->
- (* Does not take dynamic allocation into account, but then
- Value does not either. [lbl] can be ignored because they are
- taken into account by the functions [from_...] below *)
- DoChildren
-
- | Pobject_pointer _ | Pvalid_function _ ->
- DoChildren
-
- | Papp _ | Pallocable _ | Pfreeable _ | Pfresh _
- -> fail ()
-
- method private do_term_lval t =
- let current_before, current_stmt = self#get_ctrl_point () in
- match !compute_term_deps current_stmt t with
- | Some zone ->
- let filter = function Base.CLogic_Var _ -> false | _ -> true in
- let zone = Locations.Zone.filter_base filter zone in
- zones <- add_zone ~before:current_before current_stmt zone zones
- | None ->
- raise (NYI "[logic_interp] dependencies of a term lval")
-
- method! vterm t =
- match t.term_node with
- | TAddrOf _ | TLval (TMem _,_)
- | TLval(TVar {lv_origin = Some _},_) | TStartOf _ ->
- self#do_term_lval t;
- SkipChildren
- | Tat (_, BuiltinLabel Old) -> self#change_label_to_old t
- | Tat (_, BuiltinLabel Here) -> self#change_label_to_here t
- | Tat (_, BuiltinLabel Pre) -> self#change_label_to_pre t
- | Tat (_, BuiltinLabel Post) -> self#change_label_to_post t
- | Tat (_, BuiltinLabel Init) ->
- self#change_label_aux AbsLabel_init t
- | Tat (_, BuiltinLabel LoopCurrent) ->
- self#change_label_aux AbsLabel_loop_current t
- | Tat (_, BuiltinLabel LoopEntry) ->
- self#change_label_aux AbsLabel_loop_entry t
- | Tat (_, StmtLabel st) -> self#change_label_to_stmt !st t
- | Tat (_, FormalLabel s) ->
- failwith ("unknown logic label" ^ s)
- | TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _ | TAlignOfE _ ->
- (* These are static constructors, there are no dependencies here *)
- SkipChildren
- | _ -> DoChildren
- end
- in
- try
- ignore (visit (vis :> Visitor.frama_c_inplace) cil_node);
- vis#get_zones
- with NYI msg ->
- add_top_zone msg (vis#get_zones)
-
- let update_pragmas f results =
- { results with pragmas = f results.pragmas }
-
- let add_ctrl_pragma stmt =
- update_pragmas (fun x -> { x with ctrl = Stmt.Set.add stmt x.ctrl })
-
- let add_stmt_pragma stmt =
- update_pragmas (fun x -> { x with stmt = Stmt.Set.add stmt x.stmt })
-
- let add_results_from_term ctx results t =
- let zones = populate_zone ctx Visitor.visitFramacTerm t results.zones in
- {
- results with
- zones;
- locals = Varinfo.Set.union (extract_locals_from_term t) results.locals;
- labels = Logic_label.Set.union (extract_labels_from_term t) results.labels
- }
-
- let add_results_from_pred ctx results p =
- let zones = populate_zone ctx Visitor.visitFramacPredicate p results.zones in
- {
- results with
- zones;
- locals = Varinfo.Set.union (extract_locals_from_pred p) results.locals;
- labels = Logic_label.Set.union (extract_labels_from_pred p) results.labels
- }
-
- (** Entry point to get the list of [ki] * [Locations.Zone.t]
- needed to evaluate the list of [terms]
- relative to the [ctx] of interpretation. *)
- let from_terms terms ctx =
- List.fold_left (add_results_from_term ctx) empty_results terms |>
- get_result
-
- (** Entry point to get the list of [ki] * [Locations.Zone.t]
- needed to evaluate the [term]
- relative to the [ctx] of interpretation. *)
- let from_term term ctx =
- add_results_from_term ctx empty_results term |>
- get_result
-
- (** Entry point to get the list of [ki] * [Locations.Zone.t]
- needed to evaluate the list of [preds]
- relative to the [ctx] of interpretation. *)
- let from_preds preds ctx =
- List.fold_left (add_results_from_pred ctx) empty_results preds |>
- get_result
-
- (** Entry point to get the list of [ki] * [Locations.Zone.t]
- needed to evaluate the [pred]
- relative to the [ctx] of interpretation. *)
- let from_pred pred ctx =
- add_results_from_pred ctx empty_results pred |>
- get_result
-
- (** Used by annotations entry points. *)
- let get_zone_from_annot a (ki,kf) loop_body_opt results =
- let get_zone_from_term k term results =
- let ctx = { state_opt = Some true; ki_opt = Some (k, true); kf } in
- add_results_from_term ctx results term
- and get_zone_from_pred k pred results =
- let ctx = { state_opt = Some true; ki_opt = Some (k, true); kf } in
- add_results_from_pred ctx results pred
- in
- match a.annot_content with
- | APragma (Slice_pragma (SPexpr term) | Impact_pragma (IPexpr term)) ->
- results |>
- (* to preserve the interpretation of the pragma *)
- get_zone_from_term ki term |>
- (* to select the reachability of the pragma *)
- add_ctrl_pragma ki
- | APragma (Slice_pragma SPctrl) ->
- (* to select the reachability of the pragma *)
- add_ctrl_pragma ki results
- | APragma (Slice_pragma SPstmt | Impact_pragma IPstmt) ->
- (* to preserve the effect of the statement *)
- add_stmt_pragma ki results
- | AAssert (_behav,pred) ->
- (* to preserve the interpretation of the assertion *)
- get_zone_from_pred ki pred.tp_statement results
- | AInvariant (_behav,true,pred) -> (* loop invariant *)
- (* WARNING this is obsolete *)
- (* [JS 2010/09/02] TODO: so what is the right way to do? *)
- (* to preserve the interpretation of the loop invariant *)
- get_zone_from_pred (Option.get loop_body_opt) pred.tp_statement results
- | AInvariant (_behav,false,pred) -> (* code invariant *)
- (* to preserve the interpretation of the code invariant *)
- get_zone_from_pred ki pred.tp_statement results
- | AVariant (term,_) ->
- (* to preserve the interpretation of the variant *)
- get_zone_from_term (Option.get loop_body_opt) term results
- | APragma (Loop_pragma (Unroll_specs terms))
- | APragma (Loop_pragma (Widen_hints terms))
- | APragma (Loop_pragma (Widen_variables terms)) ->
- (* to select the declaration of the variables *)
- List.fold_left
- (fun results term -> {
- results with
- locals = Varinfo.Set.union (extract_locals_from_term term) results.locals;
- labels = Logic_label.Set.union (extract_labels_from_term term) results.labels
- })
- results terms
- | AAllocation (_,FreeAllocAny) -> results
- | AAllocation (_,FreeAlloc(f,a)) ->
- let get_zone results x =
- get_zone_from_term (Option.get loop_body_opt) x.it_content results
- in
- let results = List.fold_left get_zone results f in
- let results = List.fold_left get_zone results a in
- results
- | AAssigns (_, WritesAny) -> results
- | AAssigns (_, Writes l) -> (* loop assigns *)
- let get_zone results x =
- get_zone_from_term (Option.get loop_body_opt) x.it_content results
- in
- List.fold_left
- (fun results (zone,deps) ->
- let results = get_zone results zone in
- match deps with
- FromAny -> results
- | From l -> List.fold_left get_zone results l)
- results l
- | AStmtSpec _ -> (* TODO *)
- raise (NYI "[logic_interp] statement contract")
- | AExtended _ -> raise (NYI "[logic_interp] extension")
-
- (* Used by annotations entry points. *)
- let get_from_stmt_annots code_annot_filter ((ki, _kf) as stmt) results =
- Option.fold
- ~none:results
- ~some:(fun caf ->
- let loop_body_opt = match ki.skind with
- | Loop(_, { bstmts = body :: _ }, _, _, _) -> Some body
- | _ -> None
- in
- Annotations.fold_code_annot
- (fun _ a results ->
- if caf a
- then get_zone_from_annot a stmt loop_body_opt results
- else results)
- ki results)
- code_annot_filter
-
- (** Used by annotations entry points. *)
- let from_ki_annot annot ((ki, _kf) as stmt) =
- let real_ki = match ki.skind with
- Loop(_,{bstmts = loop_entry::_},_,_,_) -> Some loop_entry
- | _ -> None
- in
- get_zone_from_annot annot stmt real_ki
-
- (** Entry point to get the list of [ki] * [Locations.Zone.t]
- needed to evaluate the code annotations related to this [stmt]. *)
- let from_stmt_annot annot stmt =
- from_ki_annot annot stmt empty_results |>
- get_annot_result
-
- (** Entry point to get the list of [ki] * [Locations.Zone.t]
- needed to evaluate the code annotations related to this [stmt]. *)
- let from_stmt_annots code_annot_filter stmt =
- get_from_stmt_annots code_annot_filter stmt empty_results |>
- get_annot_result
-
- (** Entry point to get the list of [ki] * [Locations.Zone.t]
- needed to evaluate the code annotations related to this [kf]. *)
- let from_func_annots iter_on_kf_stmt code_annot_filter kf =
- let results = ref empty_results in
- let from_stmt_annots ki =
- results := get_from_stmt_annots code_annot_filter (ki, kf) !results
- in
- iter_on_kf_stmt from_stmt_annots kf;
- get_annot_result !results
-
- (** To quickly build a annotation filter *)
- let code_annot_filter annot ~threat ~user_assert ~slicing_pragma ~loop_inv ~loop_var ~others =
- match annot.annot_content with
- | APragma (Slice_pragma _) -> slicing_pragma
- | AAssert _ ->
- (match Alarms.find annot with
- | None -> user_assert
- | Some _a -> threat)
- | AVariant _ -> loop_var
- | AInvariant(_behav,true,_pred) -> loop_inv
- | AInvariant(_,false,_) -> others
- | AAllocation _ -> others
- | AAssigns _ -> others
- | APragma (Loop_pragma _)| APragma (Impact_pragma _) -> others
- | AStmtSpec _ | AExtended _ (* TODO *) -> false
+ exception NYI = Logic_deps.NYI
+ let not_yet_implemented = Logic_deps.not_yet_implemented
end
-
-exception Prune
-
-let to_result_from_pred p =
- let visitor = object (_self)
- inherit Visitor.frama_c_inplace
-
- method! vterm_lhost t =
- match t with
- | TResult _ -> raise Prune
- | _ -> DoChildren
-
- end
- in
- (try
- ignore(Visitor.visitFramacPredicate visitor p);
- false
- with Prune ->
- true)
-
-
-let () =
- Db.Properties.Interp.To_zone.code_annot_filter := To_zone.code_annot_filter;
- Db.Properties.Interp.To_zone.mk_ctx_func_contrat :=
- To_zone.mk_ctx_func_contrat;
- Db.Properties.Interp.To_zone.mk_ctx_stmt_contrat :=
- To_zone.mk_ctx_stmt_contrat;
- Db.Properties.Interp.To_zone.mk_ctx_stmt_annot := To_zone.mk_ctx_stmt_annot;
-
- Db.Properties.Interp.To_zone.from_term := To_zone.from_term;
- Db.Properties.Interp.To_zone.from_terms := To_zone.from_terms;
- Db.Properties.Interp.To_zone.from_pred := To_zone.from_pred;
- Db.Properties.Interp.To_zone.from_preds := To_zone.from_preds;
- Db.Properties.Interp.To_zone.from_stmt_annot := To_zone.from_stmt_annot;
- Db.Properties.Interp.To_zone.from_stmt_annots := To_zone.from_stmt_annots;
- Db.Properties.Interp.To_zone.from_func_annots := To_zone.from_func_annots;
-
- Db.Properties.Interp.to_result_from_pred := to_result_from_pred;
diff --git a/src/kernel_services/analysis/logic_interp.mli b/src/kernel_services/analysis/logic_interp.mli
index 739821d75e5c0bfaaeec7ed8ec41f1f396323ec8..4e8a7e6d648fc250f0e197a1388088b9045c17fa 100644
--- a/src/kernel_services/analysis/logic_interp.mli
+++ b/src/kernel_services/analysis/logic_interp.mli
@@ -20,12 +20,14 @@
(* *)
(**************************************************************************)
+(* This module exists for compatibility only and will be removed in future
+ versions *)
+
open Cil_types
module To_zone : sig
exception NYI of string
val not_yet_implemented : string ref
- val compute_term_deps: (stmt -> term -> Locations.Zone.t option) ref
end
exception [@alert deprecated "Use directly Logic_parse_string.Error istead."]
diff --git a/src/plugins/eva/legacy/logic_inout.ml b/src/plugins/eva/legacy/logic_inout.ml
index 7ae89d1e63344cad129208aff8220dfd5ef1e1da..34ed60bad552a00cac80bb75364e007797e383dc 100644
--- a/src/plugins/eva/legacy/logic_inout.ml
+++ b/src/plugins/eva/legacy/logic_inout.ml
@@ -43,7 +43,7 @@ let compute_term_deps stmt t =
let state = Results.(before stmt |> get_cvalue_model) in
term_deps state t
-let () = Logic_interp.To_zone.compute_term_deps := compute_term_deps
+let () = Logic_deps.compute_term_deps := compute_term_deps
let valid_behaviors kf state =
let funspec = Annotations.funspec kf in