Previous  Up  Next

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 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 : Pmodule.pmodule -> Model_parser.model -> Pinterp_core.oracle

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

val model_of_exec_log : original_model:Model_parser.model ->
       Pinterp_core.Log.exec_log -> Model_parser.model

model_of_exec_log ~original_model log) populates a Model_parser.model from an execution log log

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 : ?check_ce:bool -> Env.env -> classification Pp.pp

Describe a verdict in a short sentence.

val print_classification_log_or_model : ?verb_lvl:int ->
       ?json:[< `All | `Values ] ->
       print_attrs:bool -> (Model_parser.model * classification) Pp.pp

Print classification log or the model, when the model is bad or incomplete (When the prover model is printed and ~json:`Values is given, only the values are printed as JSON.)

val print_model_classification : ?verb_lvl:int ->
       ?json:[< `All | `Values ] ->
       ?check_ce: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.

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.

type strategy_from_rac = (int * Call_provers.prover_answer * Model_parser.model *
        rac_result * rac_result)
       list ->
       (int * Call_provers.prover_answer * Model_parser.model *
        rac_result * rac_result)
       list

Type of strategies to select a model from the RAC execution results.

val best_non_empty_giant_step_rac_result : strategy_from_rac

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_non_empty_model : strategy_from_rac

Select the last non empty model.

val get_rac_results : ?timelimit:float ->
       ?steplimit:int ->
       ?verb_lvl:int ->
       ?compute_term:Pinterp_core.compute_term ->
       ?only_giant_step:bool ->
       Pinterp_core.rac ->
       Env.env ->
       Pmodule.pmodule ->
       (Call_provers.prover_answer * Model_parser.model) list ->
       (int * Call_provers.prover_answer * Model_parser.model *
        rac_result * rac_result)
       list

Given a list of models, return the list of these models together with the results of the execution of normal and giant-step RAC. When called with ~only_giant_step:true, executes only the giant-step RAC.

val select_model_from_verdict : (int * Call_provers.prover_answer * Model_parser.model *
        rac_result * rac_result)
       list -> (Model_parser.model * classification) option

Select a model based on the classification (itself based on the normal and giant-step RAC executions). The first good model is selected.

val select_model_from_giant_step_rac_results : ?strategy:strategy_from_rac ->
       (int * Call_provers.prover_answer * Model_parser.model *
        rac_result * rac_result)
       list -> (Model_parser.model * rac_result) option

Select a model based on the giant-step RAC execution results. By default, the strategy is last_non_empty_model.

val select_model : ?timelimit:float ->
       ?steplimit:int ->
       ?verb_lvl:int ->
       ?compute_term:Pinterp_core.compute_term ->
       check_ce:bool ->
       Pinterp_core.rac ->
       Env.env ->
       Pmodule.pmodule ->
       (Call_provers.prover_answer * Model_parser.model) list ->
       (Model_parser.model * classification) option

Select one of the given models. When counterexample checking is enabled, 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). When counterexample checking is disabled, the last non-empty model is selected. The RAC reduce configuration rac is used only when counterexample checking is enabled.

When counterexample checking is enabled, gives the same result as select_model_from_verdict called with the result of get_rac_results.

val select_model_last_non_empty : (Call_provers.prover_answer * Model_parser.model) list ->
       Model_parser.model option

Select the last, non-empty model in the incremental list of models.

This is a compatiblity function for the behaviour before 2020, and gives the same result as select_model ~check_ce:false.