Module Check_ce

module Check_ce: sig .. end

Validation of candidate counterexamples and classification of proof failures using runtime-assertion checking

This module provides an interface for validating counterexamples and classifying proof failures using normal and giant-step runtime assertion checking, as described in the following article:

Benedikt Becker, Cláudio Belo Lourenço, Claude Marché (2021): Explaining Proof Failures with Giant-Step Runtime Assertion Checking.

The objective is to validate the candidate counterexample derived from the prover model in Model_parser, and to classify proof failures for valid counterexamples (see type Check_ce.verdict).

RAC execution

An interface to the Why3 interpreter in Pinterp with normal and giant-step runtime-assertion checking (RAC) for counterexample checking.

type rac_result_state =

`\|`	`Res_normal`	`(*`	The execution terminated normally	`*)`
`\|`	`Res_fail of Pinterp_core.cntr_ctx * Term.term`	`(*`	The execution terminated due to a failed assertion	`*)`
`\|`	`Res_stuck of string`	`(*`	The execution terminated due to a failed assumption	`*)`
`\|`	`Res_incomplete of string`	`(*`	The execution could not be terminated due to incompleteness in the execution or oracle	`*)`

The result state of a RAC execution

val print_rac_result_state : rac_result_state Pp.pp

Print a RAC result state

type rac_result =

`\|`	`RAC_not_done of string`	`(*`	RAC has not be done for the reason given as argument. Possible reasons include: the VC has no identified source location, the identified source location cannot be associated to a program routine, a small-step RAC has not been executed because only the giant-step one was requested.	`*)`
`\|`	`RAC_done of rac_result_state * Pinterp_core.Log.exec_log`	`(*`	The result of a RAC execution includes the final state and the execution log.	`*)`

val string_of_rac_result_state : rac_result_state -> string

String of the RAC result state variant

val print_rac_result : ?verb_lvl:int -> rac_result Pp.pp

Print the result state of a RAC execution with the execution log

val print_dbg_rac_result_model : print_normal:bool ->
       print_giant:bool ->
       int option ->
       (int * 'a * 'b * rac_result * rac_result) Pp.pp

val rac_execute : Pinterp.ctx ->
       Expr.rsymbol -> rac_result_state * Pinterp_core.Log.exec_log

Execute a call to the program function given by the rsymbol using normal or giant-step RAC, using the given model as an oracle for program parameters (and during giant-steps).

Conversions with models

val oracle_of_model : Pdecl.known_map -> Model_parser.model -> Pinterp_core.oracle

Create an oracle from a (prover model-derived) candidate counterexample.

val model_of_exec_log : env:Env.env ->
       known_map:Decl.known_map ->
       prover_model:Model_parser.model ->
       Pinterp_core.Log.exec_log -> Model_parser.model

model_of_exec_log ~env ~known_map ~prover_model log populates a Model_parser.model from an execution log log, using information about record declaration from known_map

Counterexample validation and proof failure classification

type verdict =

`\|`	`NC`	`(*`	Non-conformity between program and annotations: the counterexample shows that the program doesn't comply to the verification goal.	`*)`
`\|`	`SW`	`(*`	Sub-contract weakness: the counterexample shows that the contracts of some function or loop are too weak.	`*)`
`\|`	`NC_SW`	`(*`	A non-conformity or a sub-contract weakness.	`*)`
`\|`	`BAD_CE of string`	`(*`	Bad counterexample, the string gives a reason.	`*)`
`\|`	`INCOMPLETE of string`	`(*`	Incompleteness, the string gives a reason.	`*)`

Verdict of the classification. The verdicts NC, SW, and NC_SW are said to be valid.

val string_of_verdict : verdict -> string

The variant name of the verdict as a string.

type classification = verdict * Pinterp_core.Log.exec_log

The result of a classification based on normal and giant-step RAC execution is comprised of a verdict itself and the log of the relevant execution.

val report_verdict : Env.env -> classification Pp.pp

Describe a verdict in a short sentence.

val print_classification_log_or_model : ?verb_lvl:int ->
       json:bool ->
       print_attrs:bool -> (Model_parser.model * classification) Pp.pp

Print classification log or the model when the model is bad or the verdict is INCOMPLETE

val print_model_classification : ?verb_lvl:int ->
       json:bool -> Env.env -> (Model_parser.model * classification) Pp.pp

Print the classification with the classification log or model.

val classify : vc_term_loc:Loc.position option ->
       vc_term_attrs:Ident.Sattr.t ->
       normal_result:rac_result_state * Pinterp_core.Log.exec_log ->
       giant_step_result:rac_result_state * Pinterp_core.Log.exec_log ->
       classification

Classify a counterexample based on the results of the normal and giant-step RAC executions. Returns the log of the RAC execution corresponding to the classification (that is, giant in the case of a subcontract weakness, small-step in the case of a non conformity)

Model selection based on counterexample checking

Why3 requests three models from the prover, resulting in three candidate counterexamples (Call_provers.prover_result.pr_models). The following functions help selecting one counterexample.

val models_from_rac : limits:Call_provers.resource_limits ->
       ?verb_lvl:int ->
       ?compute_term:Pinterp_core.compute_term ->
       Pinterp_core.rac ->
       Env.env ->
       Pmodule.pmodule ->
       (Call_provers.prover_answer * Model_parser.model) list ->
       (Model_parser.model * rac_result * rac_result *
        classification)
       list

Execute small and giant-step RAC on the models, and compute the classification. The computed classification is based on the results of the normal and giant step RAC executions, and contains the relevant execution logs. This log can be used to explain the classification. The returned model list contains the prover supplide models, where we update the values to those that have been computed by the small-step RAC. The model is provided as an easier to manipulate object than the log, but it might contain several inconsistencies; in particular, only the me_concrete_value fields of the model are guaranteed to be updated.

val models_from_giant_step : limits:Call_provers.resource_limits ->
       ?verb_lvl:int ->
       ?compute_term:Pinterp_core.compute_term ->
       Pinterp_core.rac ->
       Env.env ->
       Pmodule.pmodule ->
       (Call_provers.prover_answer * Model_parser.model) list ->
       (Model_parser.model * rac_result) list

Execute only the giant-step RAC. The returned rac_result contains a trace of the execution of the RAC, and can be used for displaying to the user or to further elaborate the counterexample. As a helper mechanism, we also return a new model. See the discussion on models_from_rac for a more in-depth explanation.

val best_rac_result : (Model_parser.model * rac_result * rac_result *
        classification)
       list -> (Model_parser.model * classification) option

Select a model based on the classification (itself based on the normal and giant-step RAC executions). The rac_result are just discarded, as the classification is calculated at the previous stage.

The first good model is selected (i.e. with verdict Check_ce.verdict.NC, Check_ce.verdict.SW, or Check_ce.verdict.NC_SW, if any).

val best_giant_step_result : (Model_parser.model * rac_result) list ->
       (Model_parser.model * rac_result) option

Select the best non empty model based on the result of the giant-step RAC execution, with the following classification: RAC_done (Res_fail _ , _) > RAC_done (Res_normal, _) > RAC_done (Res_stuck _ , _) > RAC_done (Res_incomplete _ , _) > RAC_not_done _

val last_nonempty_model : env:Env.env ->
       known_map:Decl.known_map ->
       (Call_provers.prover_answer * Model_parser.model) list ->
       Model_parser.model option

Select the last non-empty model from the list of models, and builds concrete terms based on the terms it contains. Helper function for the cases where counterexample checking has not been requested.

val debug_check_ce_rac_results : Debug.flag

Print information about the models returned by the solver and the results of checking them by interpreting the program concretly and abstractly using the values in the solver's model.

val debug_check_ce_categorization : Debug.flag

Print the result of the categorization computed from the results of the concrete and abstract RAC executions.

val warn_concrete_term : Loc.warning_id

Warn about failures when creating a concrete counterexample