Commit 159468e4 authored by David Hauzar's avatar David Hauzar

Parser for z3 and cvc4 counter-example models - finished.

parent 5f7d7a5d
......@@ -133,6 +133,8 @@ LIBGENERATED = src/util/config.ml \
src/parser/parser.mli src/parser/parser.ml \
src/driver/driver_parser.mli src/driver/driver_parser.ml \
src/driver/driver_lexer.ml \
src/driver/parse_cvc4_z3_model_parser.mli src/driver/parse_cvc4_z3_model_parser.ml \
src/driver/parse_cvc4_z3_model_lexer.ml \
src/session/compress.ml src/session/xml.ml \
src/session/strategy_parser.ml \
lib/ocaml/why3__BigInt_compat.ml
......@@ -146,7 +148,8 @@ LIB_CORE = ident ty term pattern decl theory \
task pretty dterm env trans printer model_parser
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
whyconf autodetection parse_cvc4_z3_model
whyconf autodetection \
parse_cvc4_z3_model_parser parse_cvc4_z3_model_lexer parse_cvc4_z3_model
LIB_MLW = ity expr dexpr
......
......@@ -10,13 +10,95 @@
(********************************************************************)
open Stdlib
open Format
type model_value =
| Integer of string
| Array of model_array
| Other of string
and arr_index = {
arr_index_key : int;
arr_index_value : model_value;
}
and model_array = {
arr_others : model_value;
arr_indices : arr_index list;
}
let array_create_constant ~value =
{
arr_others = value;
arr_indices = [];
}
let array_add_element ~array ~index ~value =
(*
Adds the element value to the array on specified index.
*)
let int_index = match index with
| Integer s -> int_of_string s
| _ -> raise Not_found in
let arr_index = {
arr_index_key = int_index;
arr_index_value = value
} in
{
arr_others = array.arr_others;
arr_indices = arr_index::array.arr_indices;
}
let rec print_indices fmt indices =
match indices with
| [] -> ()
| index::tail ->
fprintf fmt "; %d -> " index.arr_index_key;
print_model_value fmt index.arr_index_value;
print_indices fmt tail
and
print_array fmt arr =
fprintf fmt "{others -> ";
print_model_value fmt arr.arr_others;
print_indices fmt arr.arr_indices;
fprintf fmt "}"
and
print_model_value fmt value =
(* Prints model value. *)
match value with
| Integer s -> fprintf fmt "%s" s
| Other s -> fprintf fmt "%s" s
| Array a -> print_array fmt a
type model_element = {
me_name : string;
me_value : string;
me_value : model_value;
me_location : Loc.position option;
}
let create_model_element ~name ~value ~location =
{
me_name = name;
me_value = value;
me_location = location;
}
let print_location fmt m_element =
match m_element.me_location with
| None -> fprintf fmt "\"no location\""
| Some loc -> Loc.report_position fmt loc
let rec print_model fmt model =
match model with
| [] -> ()
| m_element::t -> begin
fprintf fmt "%s at %a = %a\n"
m_element.me_name print_location m_element print_model_value m_element.me_value;
print_model fmt t
end
let model_to_string model =
print_model str_formatter model;
flush_str_formatter ()
type model_parser = string -> Printer.printer_mapping -> model_element list
type reg_model_parser = Pp.formatted * model_parser
......
......@@ -9,12 +9,68 @@
(* *)
(********************************************************************)
(** Counter-example model values *)
type model_value =
| Integer of string
| Array of model_array
| Other of string
and arr_index = {
arr_index_key : int;
arr_index_value : model_value;
}
and model_array = {
arr_others : model_value;
arr_indices : arr_index list;
}
val array_create_constant :
value : model_value ->
model_array
(** Creates constant array with all indices equal to the parameter value. *)
val array_add_element :
array : model_array ->
index : model_value ->
value : model_value ->
model_array
(** Adds an element to the array.
@param array : the array to that the element will be added
@param index : the index on which the element will be added.
Note that the index must be of value model_value.Integer
@param value : the value of the element to be added
*)
val print_model_value : Format.formatter -> model_value -> unit
(** Counter-example model elements. Each element represents
a counter-example for a single source-code element.*)
type model_element = {
me_name : string;
me_value : string;
me_location : Loc.position option;
(** The name of the source-code element. *)
me_value : model_value;
(** Counter-example value for the element. *)
me_location : Loc.position option;
(** Source-code location of the element. *)
}
val create_model_element :
name : string ->
value : model_value ->
location : Loc.position option ->
model_element
(** Creates a counter-example model element.
@param name : the name of the source-code element
@param value : counter-example value for the element
@param location : source-code location of the element *)
val print_model : Format.formatter -> model_element list -> unit
val model_to_string : model_element list -> string
type model_parser = string -> Printer.printer_mapping -> model_element list
val register_model_parser : desc:Pp.formatted -> string -> model_parser -> unit
......
......@@ -161,22 +161,9 @@ type pre_prover_call = unit -> prover_call
let save f = f ^ ".save"
let rec debug_print_model_with_loc model =
match model with
| [] -> ()
| m_element::t -> begin
let loc_string = match m_element.me_location with
| None -> "\"no location\""
| Some loc -> begin
Loc.report_position str_formatter loc;
flush_str_formatter ()
end in
Debug.dprintf debug "Call_provers: %s = %s@." m_element.me_name m_element.me_value;
Debug.dprintf debug " Call_provers: At %s" loc_string;
debug_print_model_with_loc t
end
let debug_print_model model =
Debug.dprintf debug "Call_provers: %s@." (Model_parser.model_to_string model)
let parse_prover_run res_parser time out ret on_timelimit timelimit ~printer_mapping =
let ans = match ret with
......@@ -201,7 +188,7 @@ let parse_prover_run res_parser time out ret on_timelimit timelimit ~printer_map
in
let model = res_parser.prp_model_parser out printer_mapping in
Debug.dprintf debug "Call_provers: model:@.";
debug_print_model_with_loc model;
debug_print_model model;
{ pr_answer = ans;
pr_status = ret;
pr_output = out;
......
%{
%}
%start <Data_structures.model_element list> output
%token <string> ATOM
%token STORE
%token CONST
%token AS
%token <string> INT_STR
%token <string> MINUS_INT_STR
%token LPAREN RPAREN
%token EOF
%%
output:
| EOF { [] }
| non_lparen_text LPAREN pairs RPAREN { $3 }
non_lparen_text:
| {}
| ATOM non_lparen_text {}
pairs:
| { [] }
| LPAREN term value RPAREN pairs { (Data_structures.create_model_element $2 $3)::$5 }
term:
| ATOM { $1 }
| LPAREN term_list RPAREN { "(" ^ $2 ^ ")" }
term_list:
| { "" }
| term term_list { $1 ^ $2 }
value:
| integer { $1 }
| array { Data_structures.Array $1 }
| term { Data_structures.Other $1 }
(*| term { Data_structures.Other $1 }*)
integer:
| INT_STR { Data_structures.Integer $1 }
| LPAREN MINUS_INT_STR RPAREN { Data_structures.Integer $2 }
array:
| LPAREN AS CONST array_skipped_part integer RPAREN { Data_structures.array_create_constant $5 }
| LPAREN STORE array integer integer RPAREN { Data_structures.array_add_element $3 $4 $5 }
array_skipped_part:
| term {}
......@@ -15,6 +15,94 @@ open Printer
open Ident
open Term
open Model_parser
open Lexing
let debug = Debug.register_info_flag "parse_cvc4_z3_model"
~desc:"Print@ debugging@ messages@ about@ parsing@ model@ \
returned@ from@ cvc4@ or@ z3."
(*
***************************************************************
** Estabilish mapping to why3 code
****************************************************************
*)
let rec extract_term_string labels raw_string regexp =
match labels with
| [] -> raw_string
| label::labels_tail ->
let l_string = label.lab_string in
begin
try
ignore(Str.search_forward regexp l_string 0);
let end_pos = Str.match_end () in
String.sub l_string end_pos ((String.length l_string) - end_pos)
with Not_found -> extract_term_string labels_tail raw_string regexp
end
let get_term_string term raw_string =
let labels = Slab.elements term.t_label in
let regexp = Str.regexp "model_trace:" in
extract_term_string labels raw_string regexp
let rec get_terms_values_locs_strings raw_strings terms collected_strings =
match raw_strings with
| [] -> collected_strings
| model_element::raw_strings_tail ->
let (term_string, term_location, terms_tail) = match terms with
| [] -> (model_element.me_name, None, [])
| term::t_tail -> ((get_term_string term model_element.me_name), term.t_loc, t_tail) in
let new_model_element = create_model_element
~name:term_string ~value:model_element.me_value ~location:term_location in
let collected_strings = collected_strings @ [new_model_element] in
get_terms_values_locs_strings raw_strings_tail terms_tail collected_strings
(*
***************************************************************
** Parser written using menhir
****************************************************************
*)
let do_parsing model =
let lexbuf = Lexing.from_string model in
try
Parse_cvc4_z3_model_parser.output Parse_cvc4_z3_model_lexer.token lexbuf
with
| Parse_cvc4_z3_model_lexer.Error msg -> Printf.fprintf stderr "%s%!\n" msg;
[]
| Parse_cvc4_z3_model_parser.Error ->
begin
let pos = lexbuf.lex_curr_p in
Printf.fprintf stderr "%d:%d \n"
pos.pos_lnum (pos.pos_cnum - pos.pos_bol + 1);
[]
end
(* Parses the model returned by CVC4 or Z3.
Assumes that the model has the following form "model: (pairs)"
Returns the list of pairs term - value *)
let parse input printer_mapping =
try
let r = Str.regexp "unknown\\|sat" in
let start_m = Str.search_forward r input 0 in
let model_string = String.sub input start_m ((String.length input) - start_m) in
let raw_model = do_parsing model_string in
get_terms_values_locs_strings raw_model printer_mapping.queried_terms []
with Not_found -> []
let () = register_model_parser "cvc4_z3" parse
~desc:"Parser@ for@ the@ model@ of@ cv4@ and@ z3."
(*
***************************************************************
** Obsolete parser
****************************************************************
*)
(*
exception EndOfStringExc;;
......@@ -90,7 +178,8 @@ let _ = parse_pair "((s(s)) 1)" 0
let _ = parse_pair "((sdfd()) (dsf)" 0
let _ = parse_pair "((= (+ (+ (+ (+ (+ (+ (+ x1 x2) x3) x4) x5) x6) x7) x8) 2) false)" 0
(* Parses a sequence of pairs from str. Returns the list of pairs.
(* Parses a sequence of pairs from str. Returns the position in the parsed string
and list of parsed pairs.
Assumes that the parts have a form: "parts: [pair]*\)" *)
let rec parse_pairs str pos list =
try
......@@ -108,44 +197,10 @@ let rec parse_pairs str pos list =
let _ = parse_pairs "((s(s)) 1) (x 1))" 0 []
let _ = parse_pairs "((= (+ (+ (+ (+ (+ (+ (+ x1 x2) x3) x4) x5) x6) x7) x8) 2) false))" 0 []
let rec extract_term_string labels raw_string regexp =
match labels with
| [] -> raw_string
| label::labels_tail ->
let l_string = label.lab_string in
begin
try
ignore(Str.search_forward regexp l_string 0);
let end_pos = Str.match_end () in
String.sub l_string end_pos ((String.length l_string) - end_pos)
with Not_found -> extract_term_string labels_tail raw_string regexp
end
let get_term_string term raw_string =
let labels = Slab.elements term.t_label in
let regexp = Str.regexp "model_trace:" in
extract_term_string labels raw_string regexp
let rec get_terms_values_locs_strings raw_strings terms collected_strings =
match raw_strings with
| [] -> collected_strings
| (raw_term_string, value)::raw_strings_tail ->
let (term_string, term_location, terms_tail) = match terms with
| [] -> (raw_term_string, None, [])
| term::t_tail -> ((get_term_string term raw_term_string), term.t_loc, t_tail) in
let new_model_element = {
me_name = term_string;
me_value = value;
me_location = term_location} in
let collected_strings = collected_strings @ [new_model_element] in
get_terms_values_locs_strings raw_strings_tail terms_tail collected_strings
(* Parses the model returned by CVC4 or Z3.
Assumes that the model has the following form "model: (pairs)"
Returns the list of pairs term - value *)
let parse model printer_mapping =
let parse_obsolete model printer_mapping =
try
let r = Str.regexp "unknown\\|sat" in
let start_m = Str.search_forward r model 0 in
......@@ -156,5 +211,6 @@ let parse model printer_mapping =
let _ = parse "dasfdfd dafsd ( dasfdf ) dfa unknown ((x 1))" Printer.get_default_printer_mapping
let () = register_model_parser "cvc4_z3" parse
let () = register_model_parser "cvc4_z3_obsolete" parse_obsolete
~desc:"Parser@ for@ the@ model@ of@ cv4@ and@ z3."
*)
{
open Parse_cvc4_z3_model_parser
exception Error of string
}
let atom = [^'('')'' ''\t''\n']
let space = [' ''\t''\n']
rule token = parse
| '\n'
{ token lexbuf }
| space+ as space_str
{ SPACE (space_str) }
| "store" { STORE }
| "const" { CONST }
| "as" { AS }
| '('
{ LPAREN }
| ')'
{ RPAREN }
| ['0'-'9']+ as integer
{ INT_STR (integer) }
| '-'space*(['0'-'9']+ as integer) { MINUS_INT_STR ("-"^integer) }
| atom+ as at { ATOM (at) }
| eof
{ EOF }
(* | space { SPACE } *)
| _
{ raise (Error (Printf.sprintf "At offset %d: unexpected character.\n" (Lexing.lexeme_start lexbuf))) }
......@@ -17,7 +17,6 @@ open Whyconf
open Gconfig
open Stdlib
open Debug
open Model_parser
module C = Whyconf
......@@ -558,20 +557,6 @@ let split_transformation = "split_goal_wp"
let inline_transformation = "inline_goal"
let intro_transformation = "introduce_premises"
let rec add_model str model =
match model with
| [] -> str
| m_element::t -> begin
let loc_string = match m_element.me_location with
| None -> "\"no location\""
| Some loc -> begin
Loc.report_position str_formatter loc;
flush_str_formatter ()
end in
let n_str = str ^ m_element.me_name ^ " at " ^ loc_string ^ " = " ^ m_element.me_value ^ "\n" in
add_model n_str t
end
let goal_task_text g =
if (Gconfig.config ()).intro_premises then
let trans =
......@@ -645,7 +630,7 @@ let update_tabs a =
begin
match a.S.proof_state with
| S.Done r ->
add_model "" r.Call_provers.pr_model
Model_parser.model_to_string r.Call_provers.pr_model
| _ -> ""
end
| _ -> ""
......
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