Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
119
Issues
119
List
Boards
Labels
Service Desk
Milestones
Merge Requests
16
Merge Requests
16
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
e56b8f56
Commit
e56b8f56
authored
May 18, 2015
by
David Hauzar
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Better error handling + 80 column lines.
parent
f951a6b3
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
66 additions
and
30 deletions
+66
-30
src/driver/parse_cvc4_z3_model.ml
src/driver/parse_cvc4_z3_model.ml
+52
-25
src/driver/parse_cvc4_z3_model_lexer.mll
src/driver/parse_cvc4_z3_model_lexer.mll
+2
-2
src/driver/parse_cvc4_z3_model_parser.mly
src/driver/parse_cvc4_z3_model_parser.mly
+12
-3
No files found.
src/driver/parse_cvc4_z3_model.ml
View file @
e56b8f56
...
...
@@ -33,9 +33,9 @@ let rec extract_element_name labels raw_string regexp =
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
)
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_element_name
labels_tail
raw_string
regexp
end
...
...
@@ -43,56 +43,83 @@ let get_element_name term raw_string =
let
labels
=
Slab
.
elements
term
.
t_label
in
let
regexp
=
Str
.
regexp
"model_trace:"
in
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. *)
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
,
element_term
,
terms_tail
)
=
match
terms
with
let
(
element_name
,
element_location
,
element_term
,
terms_tail
)
=
match
terms
with
|
[]
->
(
model_element
.
me_name
,
None
,
None
,
[]
)
|
term
::
t_tail
->
((
get_element_name
term
model_element
.
me_name
)
,
term
.
t_loc
,
Some
term
,
t_tail
)
in
let
new_model_element
=
create_model_element
~
name
:
element_name
~
value
:
model_element
.
me_value
?
location
:
element_location
?
term
:
element_term
()
in
|
term
::
t_tail
->
((
get_element_name
term
model_element
.
me_name
)
,
term
.
t_loc
,
Some
term
,
t_tail
)
in
let
new_model_element
=
create_model_element
~
name
:
element_name
~
value
:
model_element
.
me_value
?
location
:
element_location
?
term
:
element_term
()
in
let
updated_model
=
updated_model
@
[
new_model_element
]
in
update_element_names_and_locations
raw_strings_tail
terms_tail
updated_model
update_element_names_and_locations
raw_strings_tail
terms_tail
updated_model
(*
***************************************************************
** Parser written using menhir
****************************************************************
** Parser written using menhir
****************************************************************
*)
let
get_position
lexbuf
=
let
pos
=
lexbuf
.
lex_curr_p
in
let
cnum
=
pos
.
pos_cnum
-
pos
.
pos_bol
+
1
in
Loc
.
user_position
"Model string returned from the prover"
pos
.
pos_lnum
cnum
cnum
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_lexer
.
SyntaxError
->
Warning
.
emit
~
loc
:
(
get_position
lexbuf
)
"Error@ during@ lexing@ of@ smtlib@ model:@ unexpected character"
;
[]
|
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
);
let
loc
=
get_position
lexbuf
in
Warning
.
emit
~
loc
:
loc
"Error@ during@ parsing@ of@ smtlib@ model"
;
[]
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 *)
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
model_string
=
String
.
sub
input
start_m
((
String
.
length
input
)
-
start_m
)
in
let
raw_model
=
do_parsing
model_string
in
update_element_names_and_locations
raw_model
printer_mapping
.
queried_terms
[]
with
Not_found
->
[]
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."
src/driver/parse_cvc4_z3_model_lexer.mll
View file @
e56b8f56
{
open
Parse_cvc4_z3_model_parser
exception
Error
of
string
exception
SyntaxError
}
let
atom
=
[
^
'
(
''
)
''
'
'\t''\n'
]
...
...
@@ -26,5 +26,5 @@ rule token = parse
{
EOF
}
(* | space { SPACE } *)
|
_
{
raise
(
Error
(
Printf
.
sprintf
"At offset %d: unexpected character.
\n
"
(
Lexing
.
lexeme_start
lexbuf
)))
}
{
raise
SyntaxError
}
src/driver/parse_cvc4_z3_model_parser.mly
View file @
e56b8f56
...
...
@@ -72,7 +72,8 @@ other_val_str:
(* Everything that cannot be negative integer and start of an array *)
paren_other_val_str
:
|
other_than_neg_int_and_array_store
term_list
{
$
1
^
$
2
}
|
LPAREN
possible_space
other_than_const_array
possible_space
RPAREN
{
"("
^
$
3
^
")"
}
|
LPAREN
possible_space
other_than_const_array
possible_space
RPAREN
{
"("
^
$
3
^
")"
}
other_than_neg_int_and_array_store
:
|
INT_STR
{
$
1
}
...
...
@@ -88,9 +89,17 @@ other_than_const_array:
(* Example:
(store (store ((as const (Array Int Int)) 0) 1 2) 3 4) *)
array
:
|
LPAREN
possible_space
LPAREN
possible_space
AS
SPACE
CONST
possible_space
array_skipped_part
possible_space
RPAREN
possible_space
integer
possible_space
RPAREN
|
LPAREN
possible_space
LPAREN
possible_space
AS
SPACE
CONST
possible_space
array_skipped_part
possible_space
RPAREN
possible_space
integer
possible_space
RPAREN
{
Model_parser
.
array_create_constant
~
value
:$
13
}
|
LPAREN
possible_space
STORE
possible_space
array
possible_space
integer
SPACE
integer
possible_space
RPAREN
|
LPAREN
possible_space
STORE
possible_space
array
possible_space
integer
SPACE
integer
possible_space
RPAREN
{
Model_parser
.
array_add_element
~
array
:$
5
~
index
:$
7
~
value
:$
9
}
array_skipped_part
:
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment