Commit 9a365b17 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,100 +15,18 @@ open Printer
open Ident
open Term
open Model_parser
exception EndOfStringExc;;
let add_chr str chr num_opened =
if num_opened >= 0 then (str ^ Char.escaped chr)
else str
(* Gets the position of the closing bracket of the string
starting in the pos in str assuming that the given number
of brackets are opened in this position.
Assumes that at least one bracket is opened.
Example: get_in_brackets "a)" 0 1
returns 1
*)
let rec get_in_brackets str pos opened =
if pos >= String.length str then raise (EndOfStringExc)
else begin
let chr = str.[pos] in
match chr with
| '(' -> begin
get_in_brackets str (pos+1) (opened+1)
end
| ')' -> begin
if opened-1 = 0 then pos
else
get_in_brackets str (pos+1) (opened-1)
end
| _ -> begin
get_in_brackets str (pos+1) opened
end
end
let _ = get_in_brackets "(2)" 1 1;;
let rec find_first char str pos =
if pos >= String.length str then raise (EndOfStringExc)
else begin
let chr = str.[pos] in
if char == chr then pos
else find_first char str (pos+1);
end
let find_first_open_bracket = find_first '('
let find_first_space = find_first ' '
let find_first_closing_bracket = find_first ')'
let _ = find_first_open_bracket "dasfd dfd (" 0
(* Finds the end of term.
Assumes that the term has a form: "term: (anything) | any_string_delimited_by_space" *)
let term_end ch_delimit str pos =
let chr_first = str.[pos] in
let t_end = match chr_first with
| '(' -> get_in_brackets str (pos+1) 1
| _ -> (find_first ch_delimit str (pos+1))-1 in
t_end
(* Parses one pair of terms. Returns positions of the terms.
Assumes that the part has a form: "pair: [(term1 term2)]*" *)
let parse_pair str pos =
let start_first = pos + 1 in
let end_first = term_end ' ' str start_first in
let start_second = end_first+2 in
let end_second = term_end ')' str start_second in
start_first, end_first, start_second, end_second
let _ = parse_pair "(x 1)" 0
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.
Assumes that the parts have a form: "parts: [pair]*\)" *)
let rec parse_pairs str pos list =
try
let start_pos = find_first '(' str pos in
let (start1, end1, start2, end2) = parse_pair str start_pos in
let part1 = String.sub str start1 (end1-start1+1) in
let part2 = String.sub str start2 (end2-start2+1) in
let newlist = (part1, part2)::list in
parse_pairs str end2 newlist
with EndOfStringExc -> (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 =
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_element_name labels raw_string regexp =
match labels with
| [] -> raw_string
| label::labels_tail ->
......@@ -118,43 +36,64 @@ let rec extract_term_string labels raw_string regexp =
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
with Not_found -> extract_element_name labels_tail raw_string regexp
end
let get_term_string term raw_string =
let get_element_name 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
extract_element_name labels raw_string regexp
(* Uses got from printer mapping to update model names and locations in model.
Assumes that the ordering of elements of terms corresponds the ordering
in raw_model. That is nth element of raw_model corresponds to the nth element
of terms. *)
let rec update_element_names_and_locations raw_model terms updated_model =
match raw_model with
| [] -> updated_model
| model_element::raw_strings_tail ->
let (element_name, element_location, terms_tail) = match terms with
| [] -> (model_element.me_name, None, [])
| term::t_tail -> ((get_element_name term model_element.me_name), term.t_loc, t_tail) in
let new_model_element = create_model_element
~name:element_name ~value:model_element.me_value ~location:element_location in
let updated_model = updated_model @ [new_model_element] in
update_element_names_and_locations raw_strings_tail terms_tail updated_model
(*
***************************************************************
** 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
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 input printer_mapping =
try
let r = Str.regexp "unknown\\|sat" in
let start_m = Str.search_forward r model 0 in
let start = find_first_open_bracket model start_m in
let raw_terms_values_strings = snd(parse_pairs model (start+1) []) in
get_terms_values_locs_strings raw_terms_values_strings printer_mapping.queried_terms []
with Not_found -> []
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 _ = parse "dasfdfd dafsd ( dasfdf ) dfa unknown ((x 1))" Printer.get_default_printer_mapping
let raw_model = do_parsing model_string in
update_element_names_and_locations 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."
{
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