Module RecUnrolling

Unrolling of recursive functions driven by counterexamples

Outside of compositional analyses, a recursive function is unrolled a number of times in the transition system, and the recursive calls past those unrollings are left unconstrained (see LustreTransSys). A counterexample that reaches such a call may be spurious. When one does, the function is unrolled once more and the engines run again on the system built anew, with what they had established carried over (see Kind2Flow); this is not an analysis of its own. Once a function is at the limit set with --rec_unrollings, a property whose counterexample reaches its cutoff is left unknown.

This module keeps, for the analysis under way, the functions to unroll further and the properties given up on.

val depth : Analysis.param -> Scope.t -> int

The number of unrollings of a recursive function in the analysis

val reset : unit -> unit

Forget the requests and the properties given up on: a new system is analyzed

val start_round : TransSys.t -> unit

Forget the requests, and count the instances of the recursive functions of the system the engines are about to run on, to tell how fast the unrollings multiply them

val request : Analysis.param -> string -> Scope.t list -> [ `Requested | `At_limit of Scope.t list * Scope.t list ]

A counterexample to the property reached the cutoffs of the functions. Those below the limits are requested to be unrolled further; if there is none, the property is given up on, and the functions at a limit that were not reported yet are returned, to be reported once: first those whose next unrolling is expected to exceed the instances allowed with --rec_instances, then those at the limit set with --rec_unrollings.

val requested : unit -> Scope.t list

The functions requested to be unrolled further

val suspect : TransSys.t -> string -> (StateVar.t * Model.value list) list -> Scope.t list

The recursive functions the counterexample to the property may be spurious for: a cutoff of theirs is reached by the counterexample, and the counterexample is not known to be genuine. It is genuine if the functions as they are violate the property with the inputs of the counterexample. The supervisor asks a solver for a violation with those inputs, evaluates the calls past the unrollings the model executes at their concrete arguments, with the definitions of the functions in a solver of their own, gives their values back to the query as facts, and asks again, until the model only executes calls it knows the values of (genuine) or there is no violation left (spurious). A function without a definition, a call that cannot be evaluated or a query that cannot be decided in time, or a round whose checks have taken their budget, leave the counterexample suspect. The supervisor is meant to call this.

val check_abstractions : sliced:(unit -> TransSys.t option) -> TransSys.t -> string -> (StateVar.t * Model.value list) list -> unit

The counterexample to the property, which is reported, executes instances of recursive functions that their contracts abstract, in a compositional and modular analysis. If the functions as they are, rather than their contracts, violate the property with the inputs of the counterexample, the property is recorded as falsified by the functions (see genuine_properties): refining the functions, which only replaces their contracts by their bodies, cannot prove it. The check is the one of suspect, with the abstracted instances as well as the calls past the unrollings, and takes from the same budget; an undecided counterexample is not recorded. It is made on the system sliced () gives, the system of the analysis sliced to the property, if any, and on the system of the analysis otherwise. The supervisor is meant to call this.

val genuine_properties : unit -> string list

The properties recorded by check_abstractions since reset

val learned_facts : unit -> (UfSymbol.t * Term.t list * Term.t) list

The values of the calls to recursive functions that check_abstractions evaluated since reset, while showing a counterexample spurious: each a functional symbol of an output of the function, with the concrete arguments of the call and its value. These are values the functions do have, which the contracts that abstract them allowed to differ (see Analysis.info.learned).

val is_exhausted : string -> bool

Whether the property was given up on

val all_settled : TransSys.t -> bool

Whether every property of the system is proved, disproved or given up on