Module WpStrategy

module WpStrategy: sig .. end

This file provide all the functions to build a strategy that can then be used by the main generic calculus.

Annotations

type t_annots

a set of annotations to be added to a program point.

val empty_acc : t_annots

How to use an annotation

type annot_kind =

`\|`	`Ahyp`	`(*`	annotation is an hypothesis, but not a goal (see Aboth) : A => ...	`*)`
`\|`	`Agoal`	`(*`	annotation is a goal, but not an hypothesis (see Aboth): A /\ ...	`*)`
`\|`	`Aboth of bool`	`(*`	annotation can be used as both hypothesis and goal : with true : considered as both : A /\ A=>.. with false : we just want to use it as hyp right now.	`*)`
`\|`	`AcutB of bool`	`(*`	annotation is use as a cut : with true (A is also a goal) -> A (+ proof obligation A => ...) with false (A is an hyp only) -> True (+ proof obligation A => ...)	`*)`
`\|`	`AcallHyp of Cil_types.kernel_function`	`(*`	annotation is a called function property to consider as an Hyp. The pre are not here but in AcallPre since they can also be considered as goals.	`*)`
`\|`	`AcallPre of bool * Cil_types.kernel_function`	`(*`	annotation is a called function precondition : to be considered as hyp, and goal if bool=true	`*)`
`\|`	`AcallCheck of Cil_types.kernel_function`	`(*`	annotation is check-only called function precondition. handled internally by `WpStrategy.add_prop_call_pre` below.	`*)`
`\|`	`AcallPost of Cil_types.kernel_function`	`(*`	annotation is a called function post check : to be considered as goal only (no hyp)	`*)`

An annotation can be used for different purpose.

Adding properties (predicates)

val normalize : WpPropId.prop_id ->
       ?assumes:Cil_types.predicate ->
       NormAtLabels.label_mapping ->
       Cil_types.predicate -> Cil_types.predicate option

val add_prop : t_annots ->
       annot_kind ->
       WpPropId.prop_id -> Cil_types.predicate option -> t_annots

generic function to add a predicate property after normalisation. All the add_prop_xxx functions below use this one.

val add_prop_fct_pre_bhv : t_annots ->
       annot_kind ->
       Cil_types.kernel_function -> Cil_types.funbehavior -> t_annots

val add_prop_fct_pre : t_annots ->
       annot_kind ->
       Cil_types.kernel_function ->
       Cil_types.funbehavior ->
       assumes:Cil_types.predicate option ->
       Cil_types.identified_predicate -> t_annots

Add the predicate as a function precondition. Add assumes => pre if assumes is given.

val add_prop_fct_bhv_pre : t_annots ->
       annot_kind ->
       Cil_types.kernel_function -> Cil_types.funbehavior -> t_annots

Add the preconditions of the behavior

val add_prop_fct_smoke : t_annots ->
       Cil_types.kernel_function -> Cil_types.funbehavior -> t_annots

Add Smoke Test behavior

val add_prop_dead_loop : t_annots ->
       Cil_types.kernel_function -> Cil_types.stmt -> t_annots

Add Smoke Test for loop

val add_prop_dead_code : t_annots ->
       Cil_types.kernel_function -> Cil_types.stmt -> t_annots

Add Smoke Test for possibly dead code

val add_prop_dead_call : Cil_types.kernel_function ->
       Cil_types.stmt ->
       t_annots ->
       t_annots -> t_annots * t_annots

Add Smoke Test for possibly dead call : (posts,exits)

val add_prop_fct_post : t_annots ->
       annot_kind ->
       Cil_types.kernel_function ->
       Cil_types.funbehavior ->
       Cil_types.termination_kind ->
       Cil_types.identified_predicate -> t_annots

val add_prop_stmt_pre : t_annots ->
       annot_kind ->
       Cil_types.kernel_function ->
       Cil_types.stmt ->
       Cil_types.funbehavior ->
       assumes:Cil_types.predicate option ->
       Cil_types.identified_predicate -> t_annots

Add the predicate as a stmt precondition. Add assumes => pre if assumes is given.

val add_prop_stmt_post : t_annots ->
       annot_kind ->
       Cil_types.kernel_function ->
       Cil_types.stmt ->
       Cil_types.funbehavior ->
       Cil_types.termination_kind ->
       Clabels.c_label option ->
       assumes:Cil_types.predicate option ->
       Cil_types.identified_predicate -> t_annots

Add the predicate as a stmt precondition. Add \old (assumes) => post if assumes is given.

val add_prop_stmt_bhv_requires : t_annots ->
       annot_kind ->
       Cil_types.kernel_function ->
       Cil_types.stmt ->
       Cil_types.funbehavior -> with_assumes:bool -> t_annots

Add all the b_requires. Add b_assumes => b_requires if with_assumes

val add_prop_stmt_spec_pre : t_annots ->
       annot_kind ->
       Cil_types.kernel_function ->
       Cil_types.stmt -> Cil_types.funspec -> t_annots

Process the stmt spec precondition as an hypothesis for external properties. Add assumes => requires for all the behaviors.

val add_prop_call_pre : t_annots ->
       annot_kind ->
       WpPropId.prop_id ->
       assumes:Cil_types.predicate ->
       Cil_types.identified_predicate -> t_annots

val add_prop_call_post : t_annots ->
       annot_kind ->
       Cil_types.kernel_function ->
       Cil_types.funbehavior ->
       Cil_types.termination_kind ->
       assumes:Cil_types.predicate ->
       Cil_types.identified_predicate -> t_annots

Add a postcondition of a called function. Beware that kf and bhv are the called one.

val add_prop_assert : t_annots ->
       annot_kind ->
       Cil_types.kernel_function ->
       Cil_types.stmt ->
       Cil_types.code_annotation -> Cil_types.predicate -> t_annots

val add_prop_loop_inv : t_annots ->
       annot_kind ->
       Cil_types.stmt ->
       WpPropId.prop_id -> Cil_types.predicate -> t_annots

Adding assigns properties

val add_assigns : t_annots ->
       annot_kind ->
       WpPropId.prop_id -> WpPropId.assigns_desc -> t_annots

generic function to add an assigns property.

val add_assigns_any : t_annots ->
       annot_kind -> WpPropId.assigns_full_info -> t_annots

generic function to add a WriteAny assigns property.

val add_stmt_spec_assigns_hyp : t_annots ->
       Cil_types.kernel_function ->
       Cil_types.stmt ->
       Clabels.c_label option -> Cil_types.funspec -> t_annots

shortcut to add a stmt spec assigns property as an hypothesis.

val add_call_assigns_any : t_annots -> Cil_types.stmt -> t_annots

short cut to add a dynamic call

val add_call_assigns_hyp : t_annots ->
       Cil_types.kernel_function ->
       Cil_types.stmt ->
       called_kf:Cil_types.kernel_function ->
       Clabels.c_label option -> Cil_types.funspec option -> t_annots

shortcut to add a call assigns property as an hypothesis.

val add_loop_assigns_hyp : t_annots ->
       Cil_types.kernel_function ->
       Cil_types.stmt ->
       (Cil_types.code_annotation * Cil_types.from list) option ->
       t_annots

shortcut to add a loop assigns property as an hypothesis.

val add_fct_bhv_assigns_hyp : t_annots ->
       Cil_types.kernel_function ->
       Cil_types.termination_kind -> Cil_types.funbehavior -> t_annots

val assigns_upper_bound : Cil_types.funspec -> (Cil_types.funbehavior * Cil_types.from list) option

Getting information from annotations

val get_hyp_only : t_annots -> WpPropId.pred_info list

val get_goal_only : t_annots -> WpPropId.pred_info list

val get_both_hyp_goals : t_annots -> WpPropId.pred_info list * WpPropId.pred_info list

val get_cut : t_annots -> (bool * WpPropId.pred_info) list

the bool in get_cut results says if the property has to be considered as a both goal and hyp (goal=true, or hyp only (goal=false)

val get_call_hyp : t_annots -> Cil_types.kernel_function -> WpPropId.pred_info list

To be used as hypotheses around a call, (the pre are in get_call_pre_goal)

val get_call_pre : t_annots ->
       Cil_types.kernel_function ->
       WpPropId.pred_info list * WpPropId.pred_info list

Preconditions of a called function to be considered as hyp and goal (similar to get_both_hyp_goals).

val get_call_post : t_annots -> Cil_types.kernel_function -> WpPropId.pred_info list

Post-checks of a called function to be considered as goal only

val get_call_asgn : t_annots ->
       Cil_types.kernel_function option -> WpPropId.assigns_full_info

val get_asgn_hyp : t_annots -> WpPropId.assigns_full_info

val get_asgn_goal : t_annots -> WpPropId.assigns_full_info

Printing

val pp_annots : Stdlib.Format.formatter -> t_annots -> unit

Annotation table

type annots_tbl

val create_tbl : unit -> annots_tbl

val add_on_edges : annots_tbl -> t_annots -> Cil2cfg.edge list -> unit

val add_node_annots : annots_tbl ->
       Cil2cfg.t ->
       Cil2cfg.node ->
       t_annots * (t_annots * t_annots) -> unit

add_node_annots cfg annots v (before, (after, exits)) add the annotations for the node :

(before,(post,exits)) :

exits : \exits properties

before : preconditions

val add_loop_annots : annots_tbl ->
       Cil2cfg.t ->
       Cil2cfg.node ->
       entry:t_annots ->
       back:t_annots -> core:t_annots -> unit

val add_axiom : annots_tbl -> LogicUsage.logic_lemma -> unit

val add_all_axioms : annots_tbl -> unit

Strategy

type strategy

type strategy_for_froms = {

	`get_pre : unit -> t_annots;`
	`more_vars : Cil_types.logic_var list;`

}

type strategy_kind =

`\|`	`SKannots`	`(*`	normal mode for annotations	`*)`
`\|`	`SKfroms of strategy_for_froms`

val mk_strategy : string ->
       Cil2cfg.t ->
       string option ->
       strategy_kind -> annots_tbl -> strategy

val get_annots : strategy -> Cil2cfg.edge -> t_annots

val strategy_has_asgn_goal : strategy -> bool

val strategy_has_prop_goal : strategy -> bool

val strategy_kind : strategy -> strategy_kind

val global_axioms : strategy -> WpPropId.axiom_info list

val behavior_name_of_strategy : strategy -> string option

val is_default_behavior : strategy -> bool

val cfg_of_strategy : strategy -> Cil2cfg.t

val get_kf : strategy -> Cil_types.kernel_function

val get_bhv : strategy -> string option

val pp_info_of_strategy : Stdlib.Format.formatter -> strategy -> unit

Other useful things

val is_main_init : Cil_types.kernel_function -> bool

The function is the main entry point AND it is not a lib entry

val isInitConst : unit -> bool

True if both options -const-readonly and -wp-init are positioned, and the variable is global, not extern, with a "const" type (see hasConstAttribute).

Since Sodium-20150201

val isGlobalInitConst : Cil_types.varinfo -> bool

True if the variable is global, not extern, with a "const" qualifier type. Should only apply when isInitConst is true.

Since Sodium-20150201

val fold_bhv_post_cond : warn:bool ->
       ('n_acc -> Cil_types.identified_predicate -> 'n_acc) ->
       ('e_acc -> Cil_types.identified_predicate -> 'e_acc) ->
       'n_acc * 'e_acc -> Cil_types.funbehavior -> 'n_acc * 'e_acc

apply f_normal on the Normal postconditions, f_exits on the Exits postconditions, and warn on the others.

val mk_variant_properties : Cil_types.kernel_function ->
       Cil_types.stmt ->
       Cil_types.code_annotation ->
       Cil_types.term ->
       (WpPropId.prop_id * Cil_types.predicate) *
       (WpPropId.prop_id * Cil_types.predicate)