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
120
Issues
120
List
Boards
Labels
Service Desk
Milestones
Merge Requests
17
Merge Requests
17
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
d1e919a3
Commit
d1e919a3
authored
Jun 03, 2015
by
David Hauzar
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Better data structure for storing counter-example model.
parent
947e68e1
Changes
5
Hide whitespace changes
Inline
Side-by-side
Showing
5 changed files
with
197 additions
and
83 deletions
+197
-83
src/core/model_parser.ml
src/core/model_parser.ml
+149
-14
src/core/model_parser.mli
src/core/model_parser.mli
+43
-5
src/driver/call_provers.ml
src/driver/call_provers.ml
+2
-2
src/driver/call_provers.mli
src/driver/call_provers.mli
+1
-1
src/driver/parse_smtv2_model.ml
src/driver/parse_smtv2_model.ml
+2
-61
No files found.
src/core/model_parser.ml
View file @
d1e919a3
...
...
@@ -11,6 +11,15 @@
open
Stdlib
open
Format
open
Term
open
Ident
open
Printer
(*
***************************************************************
** Counter-example model values
****************************************************************
*)
type
model_value
=
|
Integer
of
string
...
...
@@ -68,6 +77,12 @@ print_model_value fmt value =
|
Other
s
->
fprintf
fmt
"%s"
s
|
Array
a
->
print_array
fmt
a
(*
***************************************************************
** Model elements
***************************************************************
*)
type
model_element
=
{
me_name
:
string
;
me_value
:
model_value
;
...
...
@@ -87,40 +102,160 @@ 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
"
\n
%s at %a = %a"
m_element
.
me_name
print_location
m_element
print_model_value
m_element
.
me_value
;
print_model
fmt
t
end
(*
***************************************************************
** Model definitions
***************************************************************
*)
module
IntMap
=
Map
.
Make
(
struct
type
t
=
int
let
compare
=
compare
end
)
module
StringMap
=
Map
.
Make
(
String
)
type
model_file
=
model_element
list
IntMap
.
t
type
model
=
model_file
StringMap
.
t
let
empty_model
=
StringMap
.
empty
let
empty_model_file
=
IntMap
.
empty
type
model_parser
=
string
->
Printer
.
printer_mapping
->
model
type
raw_model_parser
=
string
->
model_element
list
(*
***************************************************************
** Quering the model
***************************************************************
*)
let
print_model_element
fmt
m_element
=
fprintf
fmt
" %s = %a
\n
"
m_element
.
me_name
print_model_value
m_element
.
me_value
let
print_model_elements
fmt
line
m_elements
=
fprintf
fmt
" Line %d:
\n
"
line
;
List
.
iter
(
print_model_element
fmt
)
m_elements
let
print_model_file
fmt
filename
model_file
=
fprintf
fmt
"File %s:
\n
"
filename
;
IntMap
.
iter
(
print_model_elements
fmt
)
model_file
let
print_model
fmt
model
=
StringMap
.
iter
(
print_model_file
fmt
)
model
let
model_to_string
model
=
print_model
str_formatter
model
;
flush_str_formatter
()
type
model_parser
=
string
->
Printer
.
printer_mapping
->
model_element
list
let
get_model_file
model
filename
=
try
StringMap
.
find
filename
model
with
Not_found
->
empty_model_file
type
reg_model_parser
=
Pp
.
formatted
*
model_parser
let
get_elements
model_file
line_number
=
try
IntMap
.
find
line_number
model_file
with
Not_found
->
[]
let
model_parsers
:
reg_model_parser
Hstr
.
t
=
Hstr
.
create
17
(*
***************************************************************
** Building the model from raw model
***************************************************************
*)
let
add_to_model
model
model_element
=
match
model_element
.
me_location
with
|
None
->
model
|
Some
pos
->
let
(
filename
,
line_number
,
_
,
_
)
=
Loc
.
get
pos
in
let
model_file
=
get_model_file
model
filename
in
let
elements
=
get_elements
model_file
line_number
in
let
elements
=
model_element
::
elements
in
let
model_file
=
IntMap
.
add
line_number
elements
model_file
in
StringMap
.
add
filename
model_file
model
(* Estabilish mapping to why3 code *)
let
rec
extract_element_name
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_element_name
labels_tail
raw_string
regexp
end
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
let
rec
build_model_rec
raw_model
terms
model
=
match
raw_model
with
|
[]
->
model
|
model_element
::
raw_strings_tail
->
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
let
model
=
add_to_model
model
new_model_element
in
build_model_rec
raw_strings_tail
terms_tail
model
let
build_model
raw_model
printer_mapping
=
build_model_rec
raw_model
printer_mapping
.
queried_terms
empty_model
(*
***************************************************************
** Registering model parser
***************************************************************
*)
exception
KnownModelParser
of
string
exception
UnknownModelParser
of
string
type
reg_model_parser
=
Pp
.
formatted
*
raw_model_parser
let
model_parsers
:
reg_model_parser
Hstr
.
t
=
Hstr
.
create
17
let
make_mp_from_raw
(
raw_mp
:
raw_model_parser
)
=
fun
input
printer_mapping
->
let
raw_model
=
raw_mp
input
in
build_model
raw_model
printer_mapping
let
register_model_parser
~
desc
s
p
=
if
Hstr
.
mem
model_parsers
s
then
raise
(
KnownModelParser
s
);
Hstr
.
replace
model_parsers
s
(
desc
,
p
)
let
lookup_model_parser
s
=
let
lookup_
raw_
model_parser
s
=
try
snd
(
Hstr
.
find
model_parsers
s
)
with
Not_found
->
raise
(
UnknownModelParser
s
)
let
lookup_model_parser
s
=
make_mp_from_raw
(
lookup_raw_model_parser
s
)
let
list_model_parsers
()
=
Hstr
.
fold
(
fun
k
(
desc
,_
)
acc
->
(
k
,
desc
)
::
acc
)
model_parsers
[]
let
()
=
register_model_parser
~
desc
:
"Model@ parser@ with@ no@ output@ (used@ if@ the@ solver@ does@ not@ support@ models."
"no_model"
(
fun
_
_
->
[]
)
(
fun
_
->
[]
)
src/core/model_parser.mli
View file @
d1e919a3
...
...
@@ -9,7 +9,11 @@
(* *)
(********************************************************************)
(** Counter-example model values *)
(*
***************************************************************
** Counter-example model values
****************************************************************
*)
type
model_value
=
|
Integer
of
string
|
Array
of
model_array
...
...
@@ -44,6 +48,12 @@ val array_add_element :
val
print_model_value
:
Format
.
formatter
->
model_value
->
unit
(*
***************************************************************
** Model elements
***************************************************************
*)
(** Counter-example model elements. Each element represents
a counter-example for a single source-code element.*)
type
model_element
=
{
...
...
@@ -73,13 +83,41 @@ val create_model_element :
@param term : why term corresponding to the element *)
val
print_model
:
Format
.
formatter
->
model_element
list
->
unit
(*
***************************************************************
** Model definitions
***************************************************************
*)
type
model
val
empty_model
:
model
(*
***************************************************************
** Quering the model
***************************************************************
*)
val
model_to_string
:
model_element
list
->
string
val
print_model
:
Format
.
formatter
->
model
->
unit
val
model_to_string
:
model
->
string
(*
***************************************************************
** Registering model parser
***************************************************************
*)
type
model_parser
=
string
->
Printer
.
printer_mapping
->
model
(** Parses the input string into model elements, estabilishes
a mapping between these elements and mapping from printer
and builds model data structure.
*)
type
model_parser
=
string
->
Printer
.
printer_mapping
->
model_element
list
type
raw_model_parser
=
string
->
model_element
list
(** Parses the input string into model elements. *)
val
register_model_parser
:
desc
:
Pp
.
formatted
->
string
->
model_parser
->
unit
val
register_model_parser
:
desc
:
Pp
.
formatted
->
string
->
raw_
model_parser
->
unit
val
lookup_model_parser
:
string
->
model_parser
...
...
src/driver/call_provers.ml
View file @
d1e919a3
...
...
@@ -101,7 +101,7 @@ type prover_result = {
pr_output
:
string
;
pr_time
:
float
;
pr_steps
:
int
;
(* -1 if unknown *)
pr_model
:
model
_element
list
;
pr_model
:
model
;
}
type
prover_result_parser
=
{
...
...
@@ -135,7 +135,7 @@ let print_steps fmt s =
let
print_prover_result
fmt
{
pr_answer
=
ans
;
pr_status
=
status
;
pr_output
=
out
;
pr_time
=
t
;
pr_steps
=
s
;
pr_model
=
m
}
=
fprintf
fmt
"%a (%.2fs%a)"
print_prover_answer
ans
t
print_steps
s
;
if
m
<>
[]
then
begin
if
m
<>
Model_parser
.
empty_model
then
begin
fprintf
fmt
"
\n
Counter-example model:"
;
Model_parser
.
print_model
fmt
m
end
;
...
...
src/driver/call_provers.mli
View file @
d1e919a3
...
...
@@ -44,7 +44,7 @@ type prover_result = {
pr_steps
:
int
;
(** The number of steps taken by the prover (-1 if not available) *)
(** The model produced by a the solver *)
pr_model
:
model
_element
list
;
pr_model
:
model
;
}
val
print_prover_answer
:
Format
.
formatter
->
prover_answer
->
unit
...
...
src/driver/parse_smtv2_model.ml
View file @
d1e919a3
...
...
@@ -10,66 +10,12 @@
(********************************************************************)
(* Parses the model returned by CVC4 and Z3. *)
open
Printer
open
Ident
open
Term
open
Model_parser
open
Lexing
let
debug
=
Debug
.
register_info_flag
"parse_smtv2_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
->
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_element_name
labels_tail
raw_string
regexp
end
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. *)
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
|
[]
->
(
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
let
updated_model
=
updated_model
@
[
new_model_element
]
in
update_element_names_and_locations
raw_strings_tail
terms_tail
updated_model
(*
***************************************************************
...
...
@@ -104,7 +50,7 @@ let do_parsing model =
(* Parses the model returned by CVC4 or Z3.
Returns the list of pairs term - value *)
let
parse
input
printer_mapping
=
let
parse
input
=
try
let
r
=
Str
.
regexp
"unknown
\\
|sat"
in
ignore
(
Str
.
search_forward
r
input
0
);
...
...
@@ -112,12 +58,7 @@ let parse input printer_mapping =
let
model_string
=
String
.
sub
input
match_end
((
String
.
length
input
)
-
match_end
)
in
let
raw_model
=
do_parsing
model_string
in
update_element_names_and_locations
raw_model
printer_mapping
.
queried_terms
[]
do_parsing
model_string
with
|
Not_found
->
[]
...
...
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