diff --git a/.Makefile.lint b/.Makefile.lint
index 66084f3fb8c3d315c6cea8f263594c13633ad5d9..5028a0c6648db3b43fe38ed4c82e3c7244270ebe 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -134,7 +134,6 @@ ML_LINT_KO+=src/kernel_services/ast_transformations/clone.ml
ML_LINT_KO+=src/kernel_services/ast_transformations/clone.mli
ML_LINT_KO+=src/kernel_services/ast_transformations/filter.ml
ML_LINT_KO+=src/kernel_services/ast_transformations/filter.mli
-ML_LINT_KO+=src/kernel_services/ast_transformations/inline.ml
ML_LINT_KO+=src/kernel_services/cmdline_parameters/cmdline.ml
ML_LINT_KO+=src/kernel_services/cmdline_parameters/cmdline.mli
ML_LINT_KO+=src/kernel_services/cmdline_parameters/parameter_builder.ml
diff --git a/src/kernel_services/ast_transformations/inline.ml b/src/kernel_services/ast_transformations/inline.ml
index 70979b5c048ee8277af349d95333e9319cbb7372..1b9e32b076f7eb78f846eb68d87c0b9ae307f281 100644
--- a/src/kernel_services/ast_transformations/inline.ml
+++ b/src/kernel_services/ast_transformations/inline.ml
@@ -170,16 +170,16 @@ let inliner functions_to_inline = object (self)
let callee =
try Globals.Functions.get f
with Not_found ->
- Kernel.fatal
- ~current:true "Expecting a function, got %a" Printer.pp_varinfo f
+ Kernel.fatal
+ ~current:true "Expecting a function, got %a" Printer.pp_varinfo f
in
if Kernel_function.Set.mem callee functions_to_inline &&
not (self#recursive_call_limit callee)
then begin
if is_variadic_function f then begin
Kernel.warning ~wkey ~current:true ~once:true
- "Ignoring inlining option for variadic function %a"
- Printer.pp_varinfo f;
+ "Ignoring inlining option for variadic function %a"
+ Printer.pp_varinfo f;
Cil.DoChildren
end else
begin
@@ -256,7 +256,7 @@ let inliner functions_to_inline = object (self)
the current kf. Otherwise, each subsequent call to a recursive
inlined function would be inlined once again. *)
if Cil_datatype.Kf.Set.mem callee already_visited then
- Cil.ChangeToPost (stmt, do_after)
+ Cil.ChangeToPost (stmt, do_after)
else
Cil.DoChildrenPost do_after
end
@@ -322,3 +322,196 @@ let () =
Kernel_file.add_code_transformation_after_cleanup
~deps:[(module InlineCalls.As_string:Parameter_sig.S)]
inline_transform inline_calls
+
+(* -------------------------------------------------------------------------- *)
+(* Inlining of predicates and logic functions *)
+(* -------------------------------------------------------------------------- *)
+
+open Cil_datatype
+
+exception CannotInline
+
+type inline_env = {
+ (** Returns true for predicate and logic functions to be inlined. Other
+ predicates and functions are left unchanged. *)
+ inline: logic_info -> bool;
+
+ (** logic argument of the predicate -> term that replaces it, plus the label
+ at which it must be evaluated. *)
+ map_param: (term * logic_label) Logic_var.Map.t;
+
+ (** logic label of the predicate -> label at call site *)
+ map_label: logic_label Logic_label.Map.t;
+
+ (** predicates and functions already inlined once, to prevent loops on
+ recursive definitions *)
+ already_seen: Logic_info.Set.t;
+
+ (** current default label, Here at the beginning *)
+ curr_label: logic_label;
+}
+
+(* Specification of the following inliner: the resulting term/predicate
+ contains only Papp or Tapp nodes for which [env.inline] does not hold.
+ Hence, an evaluation engine that understands these functions and predicates
+ can fully evaluate the inlined predicate/term.
+
+ To implement this specification, we fail eagerly when encountering a
+ recursive definition, or a fully unknown predicate/function without a body.*)
+
+(** Visitors for inlining defined predicates and logical function *)
+class logic_inliner env = object (self)
+ inherit Visitor.frama_c_copy(Project.current())
+
+ method! vlogic_label label =
+ match Logic_label.Map.find label env.map_label with
+ | exception Not_found -> Cil.JustCopy
+ | x -> Cil.ChangeTo x
+
+ method private inline_label l =
+ try Logic_label.Map.find l env.map_label with Not_found -> l
+
+ method private inline_labels labels =
+ List.map self#inline_label labels
+
+ method private inline_args args =
+ let one t = Visitor.visitFramacTerm (self :> Visitor.frama_c_copy) t in
+ List.map one args
+
+ (* Builds the environnement to enter into the body of [li] with actual
+ labels and arguments [labels] and [args] respectively. Assumes that
+ both have already been inlined. *)
+ method private new_env li args labels =
+ let map_param =
+ List.fold_left2
+ (fun m v t -> Logic_var.Map.add v (t, env.curr_label) m)
+ Logic_var.Map.empty li.l_profile args
+ in
+ let map_label =
+ List.fold_left2
+ (fun m l1 l2 -> Logic_label.Map.add l1 l2 m)
+ Logic_label.Map.empty li.l_labels labels
+ in {
+ env with (* only inline and curr_label is kept *)
+ map_param;
+ map_label;
+ already_seen = Logic_info.Set.add li env.already_seen;
+ }
+
+ (* 'Freeze' [off] so that its evaluation occurs at the given label.
+ Does something only for [TIndex]. *)
+ method private freeze_off off lbl =
+ match off with
+ | TNoOffset -> TNoOffset
+ | TField (fi, o) -> TField (fi, self#freeze_off o lbl)
+ | TModel (mi, o) -> TModel (mi, self#freeze_off o lbl)
+ | TIndex (i, o) ->
+ let i' = Logic_const.tat ~loc:i.term_loc (i, lbl) in
+ TIndex (i', self#freeze_off o lbl)
+
+ method private add_at t lbl =
+ if Logic_label.equal lbl env.curr_label
+ then t
+ else Logic_const.tat ~loc:t.term_loc (t, lbl)
+
+ method! vterm t =
+ match t.term_node with
+ | Tat (t', l) ->
+ let l = self#inline_label l in
+ let vis = new logic_inliner { env with curr_label = l } in
+ let t' = Visitor.visitFramacTerm vis t' in
+ Cil.ChangeTo (self#add_at t' l)
+ | TLval (TVar v, TNoOffset) -> begin
+ match Logic_var.Map.find v env.map_param with
+ | exception Not_found -> Cil.JustCopy
+ | (x, lbl) ->
+ (* Replace [v] by [x], making sure it is evaluated at [lbl] *)
+ Cil.ChangeTo (self#add_at x lbl)
+ end
+ | TLval (TVar v, off) -> begin
+ match Logic_var.Map.find v env.map_param with
+ | exception Not_found -> Cil.DoChildren
+ | (x, lbl) ->
+ match x.term_node with
+ | TLval (h, offx) ->
+ (* First, inline inside [off] *)
+ let off =
+ Visitor.visitFramacTermOffset (self :> Visitor.frama_c_copy) off
+ in
+ (* We need to compute [h ++ offx ++ off] with the proper labels.
+ [h ++ offx] must be evaluated at [lbl], [off] at the current
+ label. Thus, we build [\at (h ++ offx ++ \at(off, cur), lbl)]. *)
+ let off' =
+ if Logic_label.equal env.curr_label lbl then off
+ else self#freeze_off off env.curr_label
+ in
+ let offx' = Logic_const.addTermOffset off' offx in
+ let x' = {t with term_node = TLval(h, offx')} in
+ Cil.ChangeTo (self#add_at x' lbl)
+ | _ -> (* we cannot handle casts on aggregates, functions
+ returning aggregates, etc, because we cannot buid
+ the corresponding term without a TLet *)
+ raise CannotInline
+ end
+ | Tapp({ l_body = LBterm body } as li, labels, args) -> begin
+ if Logic_info.Set.mem li env.already_seen then raise CannotInline;
+ let args = self#inline_args args in
+ let labels = self#inline_labels labels in
+ if env.inline li
+ then
+ let env = self#new_env li args labels in
+ let vis = new logic_inliner env in
+ Cil.ChangeTo (Visitor.visitFramacTerm vis body)
+ else Cil.ChangeTo {t with term_node = Tapp(li, labels, args) }
+ end
+ | Tapp (li, _, _) when env.inline li ->
+ raise CannotInline
+ | _ -> Cil.DoChildren
+
+ method! vpredicate p =
+ match p.pred_content with
+ | Pat (p', l) ->
+ let l = self#inline_label l in
+ let vis = new logic_inliner { env with curr_label = l } in
+ let p' = Visitor.visitFramacPredicate vis p' in
+ Cil.ChangeTo (Logic_const.pat ~loc:p.pred_loc (p', l))
+ | Papp ({ l_body = LBpred body } as li, labels, args) -> begin
+ if Logic_info.Set.mem li env.already_seen then raise CannotInline;
+ let args = self#inline_args args in
+ let labels = self#inline_labels labels in
+ if env.inline li
+ then
+ let env = self#new_env li args labels in
+ let vis = new logic_inliner env in
+ Cil.ChangeTo (Visitor.visitFramacPredicate vis body)
+ else Cil.ChangeTo {p with pred_content = Papp(li, labels, args) }
+ end
+ | Papp (li, _, _) when env.inline li ->
+ raise CannotInline
+ | _ -> Cil.DoChildren
+
+end
+
+let inliner curr_label inline =
+ new logic_inliner {
+ inline;
+ map_param = Logic_var.Map.empty;
+ map_label = Logic_label.Map.empty;
+ already_seen = Logic_info.Set.empty;
+ curr_label = curr_label;
+ }
+
+let inline_term ~inline ?(current = BuiltinLabel Here) term =
+ let current_loc = Cil_const.CurrentLoc.get () in
+ try Some (Visitor.visitFramacTerm (inliner current inline) term)
+ with CannotInline ->
+ (* The visitor changes and resets the reference to the current location.
+ If an exception is raised during the visit, the current location must be
+ reset by the caller. *)
+ Cil_const.CurrentLoc.set current_loc;
+ None
+
+let inline_predicate ~inline ?(current = BuiltinLabel Here) pred =
+ let current_loc = Cil_const.CurrentLoc.get () in
+ try Some (Visitor.visitFramacPredicate (inliner current inline) pred)
+ with CannotInline -> Cil_const.CurrentLoc.set current_loc; None
diff --git a/src/kernel_services/ast_transformations/inline.mli b/src/kernel_services/ast_transformations/inline.mli
index e36a1038264255393e92d404e42634833cff9389..5571b25c71a8e08c1799e7e7905d395b8cea9d64 100644
--- a/src/kernel_services/ast_transformations/inline.mli
+++ b/src/kernel_services/ast_transformations/inline.mli
@@ -20,4 +20,20 @@
(* *)
(**************************************************************************)
-val inline_calls : Cil_types.file -> unit
+open Cil_types
+
+val inline_calls : file -> unit
+
+(** [inline_term ~inline term] inlines in [term] the application of predicates
+ and logic functions for which [inline] is true. If provided, [current] is
+ the current label of the term; it is [Here] by default. Returns [None]
+ if the inlining of a predicate or a logic function fails, in particular
+ when they are recursive or have no direct definitiion. *)
+val inline_term:
+ inline:(logic_info -> bool) -> ?current:logic_label -> term -> term option
+
+(** Inlines predicates and logic functions in a predicate. See [inline_term]
+ for details. *)
+val inline_predicate:
+ inline:(logic_info -> bool) -> ?current:logic_label ->
+ predicate -> predicate option
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 81df02d653aab56af8818bd290ec73627e32b0b9..c29e3bdde8129514d0e129ef27199a4400eec849 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -651,188 +651,9 @@ let is_known_logic_fun_pred known lvi =
let is_known_logic_fun = is_known_logic_fun_pred known_logic_funs
let is_known_predicate = is_known_logic_fun_pred known_predicates
-exception CannotInline
-
-type inline_env = {
- (** logic argument of the predicate -> term that replaces it, plus the label
- at which it must be evaluated. *)
- ie_map_param: (term * logic_label) Logic_var.Map.t;
-
- (** logic label of the predicate -> label at call site *)
- ie_map_label: logic_label Logic_label.Map.t;
-
- (** predicates and functions already inlined once, to prevent loops on
- recursive definitions *)
- ie_already_seen: Logic_info.Set.t;
-
- (** current default label, Here at the beginning *)
- ie_curr_label: logic_label;
-}
-
-(* Specification of the following inliner: the resulting term/predicate
- contains only Papp or Tapp nodes for which [is_known_logic_fun] and
- [is_known_pred] hold. Hence, an evaluation engine that understands the
- predicates/functions that verify [is_known_...] can fully evaluate the
- inlined predicate/term.
-
- To implement this specification, we fail eargerly when encountering a
- recursive definition, or a fully unknown predicate/function without a body.*)
-
-(** Visitors for inlining defined predicates and logical function *)
-class inliner env = object (self)
- inherit Visitor.frama_c_copy(Project.current())
-
- method! vlogic_label label =
- match Logic_label.Map.find label env.ie_map_label with
- | exception Not_found -> Cil.JustCopy
- | x -> Cil.ChangeTo x
-
- method private inline_label l =
- try Logic_label.Map.find l env.ie_map_label with Not_found -> l
-
- method private inline_labels labels =
- List.map self#inline_label labels
-
- method private inline_args args =
- let one t = Visitor.visitFramacTerm (self :> Visitor.frama_c_copy) t in
- List.map one args
-
- (* Builds the environnement to enter into the body of [li] with actual
- labels and arguments [labels] and [args] respectively. Assumes that
- both have already been inlined. *)
- method private new_env li args labels =
- let ie_map_param =
- List.fold_left2
- (fun m v t -> Logic_var.Map.add v (t, env.ie_curr_label) m)
- Logic_var.Map.empty li.l_profile args
- in
- let ie_map_label =
- List.fold_left2
- (fun m l1 l2 -> Logic_label.Map.add l1 l2 m)
- Logic_label.Map.empty li.l_labels labels
- in {
- env with (* only curr_label is kept *)
- ie_map_param;
- ie_map_label;
- ie_already_seen = Logic_info.Set.add li env.ie_already_seen;
- }
-
- (* 'Freeze' [off] so that its evaluation occurs at the given label.
- Does something only for [TIndex]. *)
- method private freeze_off off lbl =
- match off with
- | TNoOffset -> TNoOffset
- | TField (fi, o) -> TField (fi, self#freeze_off o lbl)
- | TModel (mi, o) -> TModel (mi, self#freeze_off o lbl)
- | TIndex (i, o) ->
- let i' = Logic_const.tat ~loc:i.term_loc (i, lbl) in
- TIndex (i', self#freeze_off o lbl)
-
- method private add_at t lbl =
- if Logic_label.equal lbl env.ie_curr_label
- then t
- else Logic_const.tat ~loc:t.term_loc (t, lbl)
-
- method! vterm t =
- match t.term_node with
- | Tat (t', l) ->
- let l = self#inline_label l in
- let vis = new inliner { env with ie_curr_label = l } in
- let t' = Visitor.visitFramacTerm vis t' in
- Cil.ChangeTo (self#add_at t' l)
- | TLval (TVar v, TNoOffset) -> begin
- match Logic_var.Map.find v env.ie_map_param with
- | exception Not_found -> Cil.JustCopy
- | (x, lbl) ->
- (* Replace [v] by [x], making sure it is evaluated at [lbl] *)
- Cil.ChangeTo (self#add_at x lbl)
- end
- | TLval (TVar v, off) -> begin
- match Logic_var.Map.find v env.ie_map_param with
- | exception Not_found -> Cil.DoChildren
- | (x, lbl) ->
- match x.term_node with
- | TLval (h, offx) ->
- (* First, inline inside [off] *)
- let off =
- Visitor.visitFramacTermOffset (self :> Visitor.frama_c_copy) off
- in
- (* We need to compute [h ++ offx ++ off] with the proper labels.
- [h ++ offx] must be evaluated at [lbl], [off] at the current
- label. Thus, we build [\at (h ++ offx ++ \at(off, cur), lbl)]. *)
- let off' =
- if Logic_label.equal env.ie_curr_label lbl then off
- else self#freeze_off off env.ie_curr_label
- in
- let offx' = Logic_const.addTermOffset off' offx in
- let x' = {t with term_node = TLval(h, offx')} in
- Cil.ChangeTo (self#add_at x' lbl)
- | _ -> (* we cannot handle casts on aggregates, functions
- returning aggregates, etc, because we cannot buid
- the corresponding term without a TLet *)
- raise CannotInline
- end
- | Tapp({ l_body = LBterm body } as li, labels, args) -> begin
- if Logic_info.Set.mem li env.ie_already_seen then raise CannotInline;
- let args = self#inline_args args in
- let labels = self#inline_labels labels in
- if is_known_logic_fun li.l_var_info then
- Cil.ChangeTo {t with term_node = Tapp(li, labels, args) }
- else
- let env = self#new_env li args labels in
- let vis = new inliner env in
- Cil.ChangeTo (Visitor.visitFramacTerm vis body)
- end
- | Tapp (li, _, _) when not (is_known_logic_fun li.l_var_info) ->
- raise CannotInline
- | _ -> Cil.DoChildren
-
- method! vpredicate p =
- match p.pred_content with
- | Pat (p', l) ->
- let l = self#inline_label l in
- let vis = new inliner { env with ie_curr_label = l } in
- let p' = Visitor.visitFramacPredicate vis p' in
- Cil.ChangeTo (Logic_const.pat ~loc:p.pred_loc (p', l))
- | Papp ({ l_body = LBpred body } as li, labels, args) -> begin
- if Logic_info.Set.mem li env.ie_already_seen then raise CannotInline;
- let args = self#inline_args args in
- let labels = self#inline_labels labels in
- if is_known_predicate li.l_var_info then
- Cil.ChangeTo {p with pred_content = Papp(li, labels, args) }
- else
- let env = self#new_env li args labels in
- let vis = new inliner env in
- Cil.ChangeTo (Visitor.visitFramacPredicate vis body)
- end
- | Papp (li, _, _) when not (is_known_predicate li.l_var_info) ->
- raise CannotInline
- | _ -> Cil.DoChildren
-
-end
-
-let inliner curr_label =
- new inliner {
- ie_map_param = Logic_var.Map.empty;
- ie_map_label = Logic_label.Map.empty;
- ie_already_seen = Logic_info.Set.empty;
- ie_curr_label = curr_label;
- }
-
-let inline_term t cl =
- let current_loc = Cil_const.CurrentLoc.get () in
- try Some (Visitor.visitFramacTerm (inliner cl) t)
- with CannotInline ->
- (* The visitor changes and resets the reference to the current location.
- If an exception is raised during the visit, the current location must be
- reset by the caller. *)
- Cil_const.CurrentLoc.set current_loc;
- None
-
-let inline_predicate p cl =
- let current_loc = Cil_const.CurrentLoc.get () in
- try Some (Visitor.visitFramacPredicate (inliner cl) p)
- with CannotInline -> Cil_const.CurrentLoc.set current_loc; None
+let inline logic_info =
+ let logic_var = logic_info.l_var_info in
+ not (is_known_logic_fun logic_var || is_known_predicate logic_var)
(* We evaluate the ACSL sign type as integers 1 or -1. Sign values can only be
constructed through the \sign function (handled in eval_known_logic_function)
@@ -1132,7 +953,7 @@ let rec eval_term ~alarm_mode env t =
if is_known_logic_fun li.l_var_info then
eval_known_logic_function ~alarm_mode env li labels args
else
- match inline_term t env.e_cur with
+ match Inline.inline_term ~inline ~current:env.e_cur t with
| Some t' -> eval_term ~alarm_mode env t'
| None ->
let s =
@@ -2068,7 +1889,7 @@ let rec reduce_by_predicate ~alarm_mode env positive p =
if is_known_predicate li.l_var_info then
reduce_by_known_papp env positive li labels args
else
- match inline_predicate p env.e_cur with
+ match Inline.inline_predicate ~inline ~current:env.e_cur p with
| None -> env
| Some p' ->
reduce_by_predicate_content env positive p'.pred_content
@@ -2325,7 +2146,7 @@ and eval_predicate env pred =
if is_known_predicate li.l_var_info then
eval_known_papp env li labels args
else
- match inline_predicate p env.e_cur with
+ match Inline.inline_predicate ~inline ~current:env.e_cur p with
| None -> Unknown
| Some p' -> do_eval env p'
end
@@ -2494,7 +2315,7 @@ let predicate_deps env pred =
assert false (* TODO! Must evaluate the arguments, plus the
dependencies of the predicate itself. *)
else
- match inline_predicate p env.e_cur with
+ match Inline.inline_predicate ~inline ~current:env.e_cur p with
| None -> assert false
| Some p' -> do_eval env p'
end