Previous  Up  Next

Module Model_parser

module Model_parser: sig .. end

Model

For a given VC, a model is a set of model elements representing CE values for source code elements.

Model element kind

type model_element_kind =
| Result (*

Result of a function call (if the counter-example is for postcondition)

*)
| Call_result of Loc.position (*

Result of the function call at the given location

*)
| Old (*

Old value of function argument (if the counter-example is for postcondition)

*)
| At of string (*

Value at label

*)
| Loop_before (*

Value from before the loop

*)
| Loop_previous_iteration (*

Value from before current loop iteration

*)
| Loop_current_iteration (*

Value from current loop iteration

*)
| Error_message (*

The model element represents error message, not source-code element. The error message is saved in the name of the model element.

*)
| Other 
val print_model_kind : Stdlib.Format.formatter -> model_element_kind -> unit

Model element concrete value

Concrete syntax for model element values (which are of type Term.term), used for pretty printing and JSON printing.

type concrete_syntax_int = {
   int_value : Number.int_constant; (*

Integer value

*)
   int_verbatim : string; (*

String verbatim, as given by the SMT solver

*)
}

Integers

type concrete_syntax_bv = {
   bv_value : BigInt.t; (*

Bitvector value

*)
   bv_length : int; (*

Length of the bitvector

*)
   bv_verbatim : string; (*

String verbatim, as given by the SMT solver

*)
}

Bitvectors

Real numbers

type concrete_syntax_real = {
   real_value : Number.real_constant; (*

Real value

*)
   real_verbatim : string; (*

String verbatim, as given by the SMT solver

*)
} 
type concrete_syntax_frac = {
   frac_num : concrete_syntax_real; (*

Numerator

*)
   frac_den : concrete_syntax_real; (*

Denominator

*)
   frac_verbatim : string; (*

String verbatim, as given by the SMT solver

*)
}

Fractions

type concrete_syntax_float_value =
| Plus_infinity
| Minus_infinity
| Plus_zero
| Minus_zero
| NaN
| Float_number of {
   float_sign : concrete_syntax_bv; (*

Sign bit

*)
   float_exp : concrete_syntax_bv; (*

Exponent bits

*)
   float_mant : concrete_syntax_bv; (*

Mantissa (or significand) bits

*)
   float_hex : string; (*

Hexadecimal reprensation

*)
}

Floats

type concrete_syntax_float = {
   float_exp_size : int; (*

Size of the exponent

*)
   float_significand_size : int; (*

Size of the significand

*)
   float_val : concrete_syntax_float_value; (*

Value of the constant

*)
} 
type concrete_syntax_constant =
| Boolean of bool
| String of string
| Integer of concrete_syntax_int
| Real of concrete_syntax_real
| Float of concrete_syntax_float
| BitVector of concrete_syntax_bv
| Fraction of concrete_syntax_frac

Constants

type concrete_syntax_quant =
| Forall
| Exists

Quantifiers

type concrete_syntax_binop =
| And
| Or
| Implies
| Iff

Binary operators

type concrete_syntax_funlit_elts = {
   elts_index : concrete_syntax_term;
   elts_value : concrete_syntax_term;
} 
type concrete_syntax_funlit = {
   elts : concrete_syntax_funlit_elts list;
   others : concrete_syntax_term;
}

Function literal value

type concrete_syntax_fun = {
   args : string list;
   body : concrete_syntax_term;
}

Function arguments and body

type concrete_syntax_term =
| Var of string (*

Variable of the given name

*)
| Const of concrete_syntax_constant (*

Constant

*)
| Apply of string * concrete_syntax_term list (*

Application of the given function symbol to the given list of concrete terms

*)
| If of concrete_syntax_term * concrete_syntax_term
* concrete_syntax_term		 (*

If (cb,ct1,ct2) stands for if cb then t1 else ct2

*)
| Epsilon of string * concrete_syntax_term (*

Epsilon (x,ct) stands for eps x. ct

*)
| Quant of concrete_syntax_quant * string list
* concrete_syntax_term		 (*

Quant (q,vars,ct) stands for q vars. ct

*)
| Binop of concrete_syntax_binop * concrete_syntax_term
* concrete_syntax_term		 (*

If (op,ct1,ct2) stands for ct1 op ct2

*)
| Not of concrete_syntax_term (*

Negation of a concrete term

*)
| Function of concrete_syntax_fun (*

Function defined by the given list of arguments and the given body

*)
| FunctionLiteral of concrete_syntax_funlit (*

Special case for function literals, also used for arrays

*)
| Record of (string * concrete_syntax_term) list (*

Record defined by the given list of (field_name,field_value) elements

*)
| Proj of (string * concrete_syntax_term) (*

Projections represent values that are defined by a type coercion: the value eps x. ty'int x = 0 is represented by the concrete syntax term Proj ty'int (Const (Integer 0))

*)

Concrete term

val print_concrete_term : Stdlib.Format.formatter -> concrete_syntax_term -> unit

Helper functions to create concrete terms

val concrete_var_from_vs : Term.vsymbol -> concrete_syntax_term
val concrete_const_bool : bool -> concrete_syntax_term
val concrete_apply_from_ls : Term.lsymbol ->
       concrete_syntax_term list -> concrete_syntax_term
val concrete_apply_equ : concrete_syntax_term ->
       concrete_syntax_term -> concrete_syntax_term
val subst_concrete_term : concrete_syntax_term Wstdlib.Mstr.t ->
       concrete_syntax_term -> concrete_syntax_term
val t_and_l_concrete : concrete_syntax_term list -> concrete_syntax_term

Model elements

type model_element = {
   me_kind : model_element_kind; (*

The kind of model element.

*)
   me_value : Term.term; (*

Counterexample value for the element.

*)
   me_concrete_value : concrete_syntax_term; (*

Concrete syntax of the counterexample value.

*)
   me_location : Loc.position option; (*

Source-code location of the element.

*)
   me_attrs : Ident.Sattr.t; (*

Attributes of the element.

*)
   me_lsymbol : Term.lsymbol; (*

Logical symbol corresponding to the element.

*)
}

Counter-example model elements. Each element represents a counterexample value for a single source code element.

val create_model_element : value:Term.term ->
       concrete_value:concrete_syntax_term ->
       oloc:Loc.position option ->
       attrs:Ident.Sattr.t -> lsymbol:Term.lsymbol -> model_element

Creates a counterexample model element.

value : counterexample value for the element
concrete_value : concrete syntax of the counterexample value
oloc : (optional) location of the element
attrs : attributes of the element
lsymbol : logical symbol corresponding to the element
val get_lsymbol_or_model_trace_name : model_element -> string

Given a model element me, returns the model_trace attribute if it exists in me.me_attrs, otherwise returns the name of the me.me_lsymbol.

Model

type model 
val is_model_empty : model -> bool
val empty_model : model
val set_model_files : model ->
       model_element list Wstdlib.Mint.t Wstdlib.Mstr.t ->
       model

Querying the model

val get_model_elements : model -> model_element list
val get_model_term_loc : model -> Loc.position option
val get_model_term_attrs : model -> Ident.Sattr.t

Searching model elements

val search_model_element_for_id : model ->
       ?loc:Loc.position -> Ident.ident -> model_element option

search_model_element_for_id m ?loc id searches for a model element for identifier id, at the location id.id_loc, or at loc, when given.

val search_model_element_call_result : model ->
       Expr.expr_id option -> model_element option

search_model_element_call_result m oid searches for a model element that holds the return value for a call with id oid.

Printing the model

val json_model : model -> Json_base.json

Counterexample model in JSON format. The format is documented in share/ce-models.json.

val print_model : ?filter_similar:bool ->
       print_attrs:bool -> Stdlib.Format.formatter -> model -> unit

Prints the counterexample model.

print_attrs : when set to true, each element is printed together with the attrs associated to it.
val print_model_human : ?filter_similar:bool ->
       Stdlib.Format.formatter -> model -> print_attrs:bool -> unit

Same as print_model but is intended to be human readable.

Interleaving source code and model

val interleave_with_source : print_attrs:bool ->
       ?start_comment:string ->
       ?end_comment:string ->
       model ->
       rel_filename:string ->
       source_code:string ->
       locations:(Loc.position * 'a) list -> string * (Loc.position * 'a) list

Given a source code and a counterexample model, interleaves the source code with information about the counterexample. That is, for each location in counterexample trace creates a comment in the output source code with information about values of counterexample model elements.

start_comment : the string that starts a comment
end_comment : the string that ends a comment
rel_filename : the file name of the source relative to the session
source_code : the input source code
locations : the source locations that are found in the code

Filtering the model

val model_for_positions_and_decls : model -> positions:Loc.position list -> model

Given a model and a list of source-code positions returns model that contains only elements from the input model that are on these positions plus for every file in the model, elements that are in the positions of function declarations. Elements with other positions are filtered out.

Assumes that for each file the element on the first line of the model has position of function declaration.

Only filename and line number is used to identify positions.

Cleaning the model

class clean : object .. end

Helper class which can be inherited by API users to clean a model, for example by removing elements that do not match a given condition, or removing some "useless" fields in records, etc.

val clean_model : #clean -> model -> model

Registering model parser

type model_parser = Printer.printing_info -> string -> model

Parses the input string (i.e. the output of the SMT solver) into a model (i.e. a mapping of files and source code lines to model elements).

type raw_model_parser = Printer.printing_info -> string -> model_element list 
val register_remove_field : (Ident.Sattr.t * Term.term * concrete_syntax_term ->
        Ident.Sattr.t * Term.term * concrete_syntax_term) ->
       unit
val register_model_parser : desc:Pp.formatted -> string -> raw_model_parser -> unit
val lookup_model_parser : string -> model_parser
val list_model_parsers : unit -> (string * Pp.formatted) list