Commit da3f5499 authored by Sylvain Dailler's avatar Sylvain Dailler

In ce collection pass, constants can now have several projections.

These projections are necessary because records have changed from
old system to new system. Previously, a record was never abstract.
Subsequently, we could always give value to its fields independently.
Now, when a record (or algebraic type, not handled by this commit) is
abstract, we use the function defined for its fields as projections.
So, we need to have several projections per constant in order to represent
those as values.

This patch is also a first step to the necessary cleaning of ce treatment
code.
parent 9c49c6da
......@@ -100,6 +100,7 @@ type model_value =
| Boolean of bool
| Array of model_array
| Record of model_record
| Proj of model_proj
| Bitvector of string
| Apply of string * model_value list
| Unparsed of string
......@@ -111,7 +112,10 @@ and model_array = {
arr_others : model_value;
arr_indices : arr_index list;
}
and model_record = (field_name * model_value) list
and model_proj = (proj_name * model_value)
and proj_name = string
and field_name = string
let array_create_constant ~value =
......@@ -209,6 +213,8 @@ let rec convert_model_value value : Json_base.json =
Json_base.Record m
| Record r ->
convert_record r
| Proj p ->
convert_proj p
and convert_array a =
let m_others =
......@@ -230,6 +236,13 @@ and convert_record r =
let m = Mstr.add "val" (Json_base.Record m_field) m in
Json_base.Record m
and convert_proj p =
let proj_name, value = p in
let m = Mstr.add "type" (Json_base.String "Proj") Mstr.empty in
let m = Mstr.add "proj_name" (Json_base.String proj_name) m in
let m = Mstr.add "value" (convert_model_value value) m in
Json_base.Proj m
and convert_fields fields =
Json_base.List
(List.map
......@@ -277,6 +290,11 @@ and print_record_human fmt r =
(Pp.print_list_delim ~start:Pp.lbrace ~stop:Pp.rbrace ~sep:Pp.semi
(fun fmt (f, v) -> fprintf fmt "%s = %a" f print_model_value_human v)) r
and print_proj_human fmt p =
let s, v = p in
fprintf fmt "%s %a"
s print_model_value_human v
and print_model_value_human fmt (v: model_value) =
match v with
| Integer s -> fprintf fmt "%s" s
......@@ -288,6 +306,7 @@ and print_model_value_human fmt (v: model_value) =
fprintf fmt "(%s %a)" s (Pp.print_list Pp.space print_model_value_human) lt
| Array arr -> print_array_human fmt arr
| Record r -> print_record_human fmt r
| Proj p -> print_proj_human fmt p
| Bitvector s -> fprintf fmt "%s" s
| Unparsed s -> fprintf fmt "%s" s
......@@ -437,16 +456,15 @@ let print_model
~print_model_value
fmt
model =
(* Simple and easy way to print file sorted alphabetically
FIXME: but StringMap.iter is supposed to iter in alphabetic order, so waste of time and memory here !
*)
let l = StringMap.bindings model.model_files in
List.iter (fun (k, e) -> print_model_file ~print_attrs ~print_model_value fmt me_name_trans k e) l
StringMap.iter (fun k e ->
print_model_file ~print_attrs ~print_model_value fmt me_name_trans k e)
model.model_files
let print_model_human
?(me_name_trans = why_name_trans)
fmt
model = print_model ~me_name_trans ~print_model_value:print_model_value_human fmt model
model =
print_model ~me_name_trans ~print_model_value:print_model_value_human fmt model
let print_model ?(me_name_trans = why_name_trans)
~print_attrs
......@@ -671,7 +689,6 @@ let print_model_json
fmt
model_files_bindings
let model_to_string_json
?(me_name_trans = why_name_trans)
?(vc_line_trans = (fun i -> string_of_int i))
......@@ -696,20 +713,66 @@ let add_to_model model model_element =
let model_file = IntMap.add line_number elements model_file in
StringMap.add filename model_file model
let recover_name term_map raw_name =
let t = Mstr.find raw_name term_map in
construct_name (get_model_trace_string ~attrs:t.t_attrs) t.t_attrs
let rec replace_projection (const_function: string -> string) model_value =
match model_value with
| Integer _ | Decimal _ | Fraction _ | Float _ | Boolean _ | Bitvector _
| Unparsed _ -> model_value
| Array a ->
Array (replace_projection_array const_function a)
| Record r ->
let r =
List.map (fun (field_name, value) ->
let field_name = try const_function field_name with
Not_found -> field_name
in
(field_name, replace_projection const_function value)
)
r
in
Record r
| Proj p ->
let proj_name, value = p in
let proj_name =
try const_function proj_name
with Not_found -> proj_name
in
Proj (proj_name, replace_projection const_function value)
| Apply (s, l) ->
let s = try const_function s
with Not_found -> s
in
Apply (s, (List.map (fun v -> replace_projection const_function v) l))
and replace_projection_array const_function a =
let {arr_others = others; arr_indices = arr_index_list} = a in
let others = replace_projection const_function others in
let arr_index_list =
List.map
(fun ind ->
let {arr_index_key = key; arr_index_value = value} = ind in
let value = replace_projection const_function value in
{arr_index_key = key; arr_index_value = value}
)
arr_index_list
in
{arr_others = others; arr_indices = arr_index_list}
let build_model_rec (raw_model: model_element list) (term_map: Term.term Mstr.t) (model: model_files) =
List.fold_left (fun model raw_element ->
let raw_element_name = raw_element.me_name.men_name in
let raw_element_value = replace_projection (fun x -> (recover_name term_map x).men_name) raw_element.me_value in
try
(
let t = Mstr.find raw_element_name term_map in
let real_model_trace =
construct_name (get_model_trace_string ~attrs:t.t_attrs) t.t_attrs
in
let model_element = {
me_name = real_model_trace;
me_value = raw_element.me_value;
me_location = t.t_loc;
me_term = Some t;
me_name = construct_name (get_model_trace_string ~attrs:t.t_attrs) t.t_attrs;
me_value = raw_element_value;
me_location = t.t_loc;
me_term = Some t;
} in
add_to_model model model_element
)
......
......@@ -34,6 +34,7 @@ type model_value =
| Boolean of bool
| Array of model_array
| Record of model_record
| Proj of model_proj
| Bitvector of string
| Apply of string * model_value list
| Unparsed of string
......@@ -45,6 +46,8 @@ and model_array = {
arr_others : model_value;
arr_indices : arr_index list;
}
and model_proj = (proj_name * model_value)
and proj_name = string
and model_record = (field_name * model_value) list
and field_name = string
......@@ -98,19 +101,19 @@ type model_element_name = {
(** Counter-example model elements. Each element represents
a counter-example for a single source-code element.*)
type model_element = {
me_name : model_element_name;
me_name : model_element_name;
(** Information about the name of the model element *)
me_value : model_value;
me_value : model_value;
(** Counter-example value for the element. *)
me_location : Loc.position option;
me_location : Loc.position option;
(** Source-code location of the element. *)
me_term : Term.term option;
me_term : Term.term option;
(** Why term corresponding to the element. *)
}
val create_model_element :
name : string ->
value : model_value ->
name : string ->
value : model_value ->
?location : Loc.position ->
?term : Term.term ->
unit ->
......
......@@ -188,21 +188,6 @@ let rec grep out l = match l with
| HighFailure -> assert false
with Not_found -> grep out l end
(*
let rec grep out l = match l with
| [] ->
HighFailure
| (re,pa) :: l ->
begin try
ignore (Str.search_forward re out 0);
match pa with
| Valid | Invalid | Timeout | OutOfMemory | StepLimitExceeded -> pa
| Unknown (s, ru) -> Unknown ((Str.replace_matched s out), ru)
| Failure s -> Failure (Str.replace_matched s out)
| HighFailure -> assert false
with Not_found -> grep out l end
*)
(* Create a regexp matching the same as the union of all regexp of the list. *)
let craft_efficient_re l =
let s = Format.asprintf "%a"
......@@ -214,12 +199,6 @@ let craft_efficient_re l =
in
Str.regexp s
(*
let print_delim fmt d =
match d with
| Str.Delim s -> Format.fprintf fmt "Delim %s" s
| Str.Text s -> Format.fprintf fmt "Text %s" s
*)
let debug_print_model ~print_attrs model =
let model_str = Model_parser.model_to_string ~print_attrs model in
Debug.dprintf debug "Call_provers: %s@." model_str
......@@ -238,9 +217,6 @@ let analyse_result res_parser printer_mapping out =
| Str.Text t -> Model t)
result_list
in
(* Format.eprintf "[incremental model parsing] results list is @[[%a]@]@."
(Pp.print_list Pp.semi print_delim) result_list;
*)
let rec analyse saved_model saved_res l =
match l with
| [] ->
......
This diff is collapsed.
......@@ -11,10 +11,6 @@
open Wstdlib
(* Debugging function *)
val print_table:
Smt2_model_defs.correspondence_table -> unit
(* This allows registering a transformation of counterexamples terms. It allows
to convert Apply(s, t) into appropriate counterexample datatypes. For
example, an unconstrained array that was translated from an high-level
......@@ -28,5 +24,5 @@ val register_apply_to_records:
(* From the table generated by the parser, build a list of model_element *)
val create_list:
Sstr.t -> ((string * string) list) Mstr.t -> Smt2_model_defs.correspondence_table ->
Sstr.t -> ((string * string) list) Mstr.t -> Smt2_model_defs.definition Mstr.t ->
Model_parser.model_element list
......@@ -10,9 +10,10 @@
(********************************************************************)
%{
open Smt2_model_defs
%}
%start <Smt2_model_defs.correspondence_table> output
%start <Smt2_model_defs.definition Wstdlib.Mstr.t> output
%token <string> ATOM
%token MODEL
%token STORE
......@@ -55,8 +56,8 @@ output:
| LPAREN MODEL list_decls RPAREN { $3 }
list_decls:
| LPAREN decl RPAREN { Smt2_model_defs.add_element $2 Wstdlib.Mstr.empty false}
| LPAREN decl RPAREN list_decls { Smt2_model_defs.add_element $2 $4 false }
| LPAREN decl RPAREN { add_element $2 Wstdlib.Mstr.empty}
| LPAREN decl RPAREN list_decls { add_element $2 $4 }
| COMMENT list_decls { $2 } (* Lines beginning with ';' are ignored *)
(* Examples:
......@@ -68,8 +69,8 @@ list_decls:
decl:
| DEFINE_FUN name LPAREN args_lists RPAREN
ireturn_type smt_term
{ let t = Smt2_model_defs.make_local $4 $7 in
Some ($2, (Smt2_model_defs.Function ($4, t))) }
{ let t = make_local $4 $7 in
Some ($2, (Function ($4, t))) }
| DECLARE_SORT isort_def { None }
| DECLARE_DATATYPES idata_def { None }
(* z3 declare function *)
......@@ -77,32 +78,32 @@ decl:
| FORALL LPAREN args_lists RPAREN smt_term { None } (* z3 cardinality *)
smt_term:
| name { Smt2_model_defs.Variable $1 }
| integer { Smt2_model_defs.Integer $1 }
| decimal { Smt2_model_defs.Decimal $1 }
| fraction { Smt2_model_defs.Fraction $1 }
| array { Smt2_model_defs.Array $1 }
| bitvector { Smt2_model_defs.Bitvector $1 }
| boolean { Smt2_model_defs.Boolean $1 }
| name { Variable $1 }
| integer { Sval (Integer $1) }
| decimal { Sval (Decimal $1) }
| fraction { Sval (Fraction $1) }
| array { Array $1 }
| bitvector { Sval (Bitvector $1) }
| boolean { Sval (Boolean $1) }
(* z3 sometimes answer with boolean expressions for some reason ? *)
| boolean_expression { Smt2_model_defs.Other "" }
| FLOAT_VALUE { Smt2_model_defs.Float $1 }
| boolean_expression { Sval (Other "") }
| FLOAT_VALUE { Sval (Float $1) }
(* ite (= ?a ?b) ?c ?d *)
| LPAREN ITE pair_equal smt_term smt_term RPAREN
{ match $3 with
| None -> Smt2_model_defs.Other ""
| Some (t1, t2) -> Smt2_model_defs.Ite (t1, t2, $4, $5) }
| None -> Sval (Other "")
| Some (t1, t2) -> Ite (t1, t2, $4, $5) }
(* No parsable value are applications. *)
| application { $1 }
(* Particular case for functions that are defined as an equality:
define-fun f ((a int) (b int)) (= a b) *)
| LPAREN EQUAL list_smt_term RPAREN { Smt2_model_defs.Other "" }
| LPAREN EQUAL list_smt_term RPAREN { Sval (Other "") }
| LPAREN LET LPAREN list_let RPAREN smt_term RPAREN
{ Smt2_model_defs.substitute $4 $6 }
{ substitute $4 $6 }
(* z3 specific constructor *)
| LPAREN UNDERSCORE AS_ARRAY name RPAREN
{ Smt2_model_defs.To_array (Smt2_model_defs.Variable $4) }
{ To_array (Variable $4) }
(* value of let are not used *)
......@@ -129,11 +130,11 @@ list_smt_term:
| list_smt_term smt_term { $2 :: $1}
application:
| LPAREN name list_smt_term RPAREN { Smt2_model_defs.Apply($2, List.rev $3) }
| LPAREN binop smt_term smt_term RPAREN { Smt2_model_defs.Apply($2, [$3;$4]) }
| LPAREN name list_smt_term RPAREN { Apply ($2, List.rev $3) }
| LPAREN binop smt_term smt_term RPAREN { Apply ($2, [$3;$4]) }
(* This should not happen in relevant part of the model *)
| LPAREN INT_TO_BV smt_term RPAREN {
Smt2_model_defs.Apply($2, [$3]) }
Apply ($2, [$3]) }
binop:
......@@ -145,20 +146,20 @@ array:
| LPAREN
LPAREN AS CONST ireturn_type
RPAREN smt_term
RPAREN{ Smt2_model_defs.Const $7 }
RPAREN{ Const $7 }
| LPAREN
STORE array smt_term smt_term
RPAREN { Smt2_model_defs.Store ($3, $4, $5) }
RPAREN { Store ($3, $4, $5) }
| LPAREN
STORE name smt_term smt_term
RPAREN { Smt2_model_defs.Store (Smt2_model_defs.Array_var $3, $4, $5) }
RPAREN { Store (Array_var $3, $4, $5) }
(* When array is of type int -> bool, Cvc4 returns something that looks like:
(ARRAY_LAMBDA (LAMBDA ((BOUND_VARIABLE_1162 Int)) false)) *)
| LPAREN
ARRAY_LAMBDA
LPAREN LAMBDA LPAREN args_lists RPAREN smt_term
RPAREN RPAREN
{ Smt2_model_defs.Const $8 }
{ Const $8 }
args_lists:
| { [] }
......
......@@ -9,97 +9,49 @@
(* *)
(********************************************************************)
open Wstdlib
type variable = string
(* Simple counterexample that already represent a complete value *)
type simple_value =
| Integer of string
| Decimal of (string * string)
| Fraction of (string * string)
| Float of Model_parser.float_type
| Other of string
| Bitvector of string
| Boolean of bool
type array =
| Array_var of variable
| Const of term
| Store of array * term * term
and term =
| Integer of string
| Decimal of (string * string)
| Fraction of (string * string)
| Float of Model_parser.float_type
| Sval of simple_value
| Apply of (string * term list)
| Other of string
| Array of array
| Bitvector of string
| Boolean of bool
| Cvc4_Variable of variable
| Function_Local_Variable of variable
| Variable of variable
| Ite of term * term * term * term
| Record of string * ((string * term) list)
| To_array of term
(* TODO remove tree *)
| Trees of (string * term) list
type definition =
| Function of (variable * string option) list * term
| Term of term
| Noelement
(* Type returned by parsing of model.
An hashtable that makes a correspondence between names (string) and
associated definition (complex stuff) *)
type correspondence_table = (bool * definition) Mstr.t
let print_float fmt f =
match f with
| Model_parser.Plus_infinity -> Format.fprintf fmt "Plus_infinity"
| Model_parser.Minus_infinity -> Format.fprintf fmt "Minus_infinity"
| Model_parser.Plus_zero -> Format.fprintf fmt "Plus_zero"
| Model_parser.Minus_zero -> Format.fprintf fmt "Minus_zero"
| Model_parser.Not_a_number -> Format.fprintf fmt "NaN"
| Model_parser.Float_value (b, eb, sb) -> Format.fprintf fmt "(%s, %s, %s)" b eb sb
| Model_parser.Float_hexa(s,f) -> Format.fprintf fmt "%s (%g)" s f
let rec print_array fmt a =
match a with
| Array_var v -> Format.fprintf fmt "ARRAY_VAR : %s" v
| Const t -> Format.fprintf fmt "CONST : %a" print_term t
| Store (a, t1, t2) ->
Format.fprintf fmt "STORE : %a %a %a"
print_array a print_term t1 print_term t2
(* Printing function for terms *)
and print_term fmt t =
match t with
| Integer s -> Format.fprintf fmt "Integer: %s" s
| Decimal (s1, s2) -> Format.fprintf fmt "Decimal: %s . %s" s1 s2
| Fraction (s1, s2) -> Format.fprintf fmt "Fraction: %s / %s" s1 s2
| Float f -> Format.fprintf fmt "Float: %a" print_float f
| Apply (s, lt) ->
Format.fprintf fmt "Apply: (%s, %a)" s
(Pp.print_list_delim ~start:Pp.lsquare ~stop:Pp.rsquare ~sep:Pp.comma print_term)
lt
| Other s -> Format.fprintf fmt "Other: %s" s
| Array a -> Format.fprintf fmt "Array: %a" print_array a
| Bitvector bv -> Format.fprintf fmt "Bv: %s" bv
| Boolean _b -> Format.fprintf fmt "Boolean"
| Cvc4_Variable cvc -> Format.fprintf fmt "CVC4VAR: %s" cvc
| Function_Local_Variable v -> Format.fprintf fmt "LOCAL: %s" v
| Variable v -> Format.fprintf fmt "VAR: %s" v
| Ite _ -> Format.fprintf fmt "ITE"
| Record (n, l) ->
Format.fprintf fmt "record_type: %s; list_fields: %a" n
(Pp.print_list Pp.semi
(fun fmt (x, a) -> Format.fprintf fmt "(%s, %a)" x print_term a))
l
| To_array t -> Format.fprintf fmt "TO_array: %a@." print_term t
let print_def fmt d =
match d with
| Function (_vars, t) -> Format.fprintf fmt "FUNCTION : %a" print_term t
| Term t -> Format.fprintf fmt "TERM : %a" print_term t
| Noelement -> Format.fprintf fmt "NOELEMENT"
let add_element x (t: correspondence_table) b =
let add_element x (t: definition Mstr.t) =
match x with
| None -> t
| Some (key, value) ->
Mstr.add key (b, value) t
Mstr.add key value t
exception Bad_local_variable
......@@ -150,19 +102,17 @@ and make_local vars_lists t =
| Apply (s, lt) ->
let lt = List.map (make_local vars_lists) lt in
Apply (s, lt)
| Integer _ | Decimal _ | Fraction _ | Float _ | Other _ -> t
| Bitvector _ -> t
| Sval v -> Sval v
| Cvc4_Variable _ -> raise Bad_local_variable
| Boolean _ -> t
| Function_Local_Variable _ -> raise Bad_local_variable
| Record (n, l) -> Record (n, List.map (fun (f, x) -> f, make_local vars_lists x) l)
| To_array t -> To_array (make_local vars_lists t)
(* TODO tree does not exist yet *)
| Trees t -> Trees t
let rec subst var value t =
match t with
| Integer _ | Decimal _ | Fraction _ | Float _
| Other _ | Bitvector _ | Boolean _ ->
t
| Sval v -> Sval v
| Array a -> Array (subst_array var value a)
| Cvc4_Variable _ -> raise Bad_local_variable
| Function_Local_Variable _ -> t
......@@ -178,7 +128,8 @@ let rec subst var value t =
| To_array t -> To_array (subst var value t)
| Apply (s, lt) ->
Apply (s, List.map (subst var value) lt)
(* Tree does not exists yet *)
| Trees t -> Trees t
and subst_array var value a =
match a with
......
......@@ -13,6 +13,16 @@ open Wstdlib
type variable = string
(* Simple counterexample that already represent a complete value *)
type simple_value =
| Integer of string
| Decimal of (string * string)
| Fraction of (string * string)
| Float of Model_parser.float_type
| Other of string
| Bitvector of string
| Boolean of bool
type array =
(* Array_var is used by let-bindings only *)
| Array_var of variable
......@@ -20,41 +30,27 @@ type array =
| Store of array * term * term
and term =
| Integer of string
| Decimal of (string * string)
| Fraction of (string * string)
| Float of Model_parser.float_type
| Sval of simple_value
| Apply of (string * term list)
| Other of string
| Array of array
| Bitvector of string
| Boolean of bool
| Cvc4_Variable of variable
| Function_Local_Variable of variable
| Variable of variable
| Ite of term * term * term * term
| Record of string * ((string * term) list)
| To_array of term
(* TODO remove tree *)
| Trees of (string * term) list
type definition =
| Function of (variable * string option) list * term
| Term of term (* corresponding value of a term *)
| Noelement
(* Type returned by parsing of model.
An hashtable that makes a correspondence between names (string) and
associated definition (complex stuff) *)
(* The boolean is true when the term has no external variable *)
type correspondence_table = (bool * definition) Mstr.t
val add_element: (string * definition) option ->
correspondence_table -> bool -> correspondence_table
definition Mstr.t -> definition Mstr.t
val make_local: (variable * string option) list -> term -> term
val print_term: Format.formatter -> term -> unit
val print_def: Format.formatter -> definition -> unit
(* Used for let bindings of z3 *)
val substitute: (string * term) list -> term -> term
......@@ -62,6 +62,7 @@ let convert_record l =
type json =
| Record of json Mstr.t
| Proj of json Mstr.t
| List of json list
| String of string
| Int of int
......@@ -72,6 +73,7 @@ type json =
let rec print_json fmt v =
match v with
| Record r -> map_bindings (fun x -> x) print_json fmt (Mstr.bindings r)
| Proj p -> map_bindings (fun x -> x) print_json fmt (Mstr.bindings p)
| List l -> list print_json fmt l
| String s -> string fmt s
| Int i -> int fmt i
......
......@@ -56,6 +56,7 @@ val convert_record : (string * 'a) list -> 'a Wstdlib.Mstr.t
function to print it *)
type json =
| Record of json Wstdlib.Mstr.t
| Proj of json Wstdlib.Mstr.t
| List of json list
| String of string
| Int of int
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment