Module Counterexample

module Counterexample: sig .. end

Use solver models and Pinterp to create counterexamples


Solver's model analysis and counterexample construction

val debug_check_ce : Debug.flag

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

type verdict = private 
| Good_model (*

the model leads to a counterexample

*)
| Bad_model (*

the model doesn't lead to a counterexample

*)
| Dont_know (*

cannot decide if the model leads to a counterexample

*)
type full_verdict = private {
   verdict : verdict;
   reason : string;
   exec_log : Pinterp.Log.exec_log;
}
type check_model_result = private 
| Cannot_check_model of {
   reason : string;
}
| Check_model_result of {
   abstract : full_verdict;
   concrete : full_verdict;
}
val print_check_model_result : ?verb_lvl:int -> check_model_result Pp.pp
val check_model : Pinterp.rac_reduce_config ->
Env.env ->
Pmodule.pmodule -> Model_parser.model -> check_model_result

Summary of checking models

type ce_summary = 
| NCCE of Pinterp.Log.exec_log (*

Non-conformity between program and annotations: the CE shows that the program doesn't comply to the verification goal.

*)
| SWCE of Pinterp.Log.exec_log (*

Sub-contract weakness: The contracts of some function or loop are underspecified.

*)
| NCCE_SWCE of Pinterp.Log.exec_log (*

Non-conformity or sub-contract weakness.

*)
| BAD_CE (*

Bad counterexample.

*)
| UNKNOWN of string (*

The counterexample has not been verified.

*)
val ce_summary : check_model_result -> ce_summary
val print_ce_summary_title : ?check_ce:bool -> ce_summary Pp.pp
val print_ce_summary_kind : ce_summary Pp.pp
val print_counterexample : ?verb_lvl:int ->
?check_ce:bool ->
?json:[< `All | `Values ] ->
(Model_parser.model * ce_summary) Pp.pp

Print a counterexample. (When the prover model is printed and ~json:`Values is given, only the values are printedas JSON.)

Model selection

type sort_models 

Sort prover models in select_model.

val select_model : ?verb_lvl:int ->
?check:bool ->
?reduce_config:Pinterp.rac_reduce_config ->
?sort_models:sort_models ->
Env.env ->
Pmodule.pmodule ->
(Call_provers.prover_answer * Model_parser.model) list ->
(Model_parser.model * ce_summary) option

select ~check ~conservative ~reduce_config env pm ml chooses a model from ml. check is set to false by default and indicates if interpretation should be used to select the model. reduce_config is set to rac_reduce_config () by default and is only used if check=true. Different priorizations of prover models can be selected by sort_models, which is by default prioritize_first_good_model if check and prioritize_last_non_empty_model otherwise.

val prioritize_first_good_model : sort_models

If there is any model that can be verified by counterexample checking, prioritize NCCE over SWCE over NCCE_SWCE, and prioritize simpler models from the incremental list produced by the prover.

Otherwise prioritize the last, non-empty model in the incremental list, but penalize bad models.

val prioritize_last_non_empty_model : sort_models

Do not consider the result of checking the counterexample model, but just priotize the last, non-empty model in the incremental list of models.

Compatibility

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

Select the last, non-empty model in the incremental list of models as done before 2020. The summary is included for compatibility with select_model and is always UNKNOWN.

Same behaviour as select_model ~check:false ~sort_models:prioritize_last_non_empty_model.

Conversion to Model_parser.model

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

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