Commit 68b3134d authored by David Hauzar's avatar David Hauzar

Adding information about the line that corresponds to the VC check

to the counter-example model.

This line must be marked with the label "model_vc".
If VC line is postcondition, it can be marked with the label
"model_func" or "model_func:func_name". Terms corresponding to
old values of arguments will be marked with @old, term corresponding
to the function result will be marked with @result or
func_name@result if func_name was given.

Pretty printing of model element names in counter-example.
Possibility to print differently model elements corresponding to
function result, old values of function arguments and other model
elements.
parent 01f845fe
......@@ -15,6 +15,12 @@ open Term
open Ident
open Printer
(*
let debug = Debug.register_info_flag "model_parser"
~desc:"Print@ debugging@ messages@ about@ parsing@ \
the@ counter-example@ model."
*)
(*
***************************************************************
** Counter-example model values
......@@ -24,7 +30,7 @@ open Printer
type model_value =
| Integer of string
| Array of model_array
| Other of string
| Unparsed of string
and arr_index = {
arr_index_key : int;
arr_index_value : model_value;
......@@ -74,7 +80,7 @@ print_model_value_sanit sanit_print fmt value =
(* Prints model value. *)
match value with
| Integer s -> sanit_print fmt s
| Other s -> sanit_print fmt s
| Unparsed s -> sanit_print fmt s
| Array a -> print_array sanit_print fmt a
let print_model_value fmt value =
......@@ -86,16 +92,37 @@ let print_model_value fmt value =
** Model elements
***************************************************************
*)
type model_element_type =
| Result
| Old
| Other
type model_element = {
me_name : string;
me_type : model_element_type;
me_value : model_value;
me_location : Loc.position option;
me_term : Term.term option;
}
let split_me_name name =
let splitted = Str.bounded_split (Str.regexp_string "@") name 2 in
match splitted with
| [first] -> (first, "")
| first::[second] ->
(first, second)
| _ -> (* here, "_" can only stand for [] *)
("", "")
let create_model_element ~name ~value ?location ?term () =
let (name, type_s) = split_me_name name in
let t = match type_s with
| "result" -> Result
| "old" -> Old
| _ -> Other in
{
me_name = name;
me_type = t;
me_value = value;
me_location = location;
me_term = term;
......@@ -131,27 +158,38 @@ type raw_model_parser = string -> model_element list
** Quering the model
***************************************************************
*)
let print_model_element fmt m_element =
let print_model_element me_name_trans fmt m_element =
let me_name = me_name_trans (m_element.me_name, m_element.me_type) in
fprintf fmt "%s = %a"
m_element.me_name print_model_value m_element.me_value
me_name print_model_value m_element.me_value
let print_model_elements ?(sep = "\n") fmt m_elements =
Pp.print_list (fun fmt () -> Pp.string fmt sep) print_model_element fmt m_elements
let print_model_elements ?(sep = "\n") me_name_trans fmt m_elements =
Pp.print_list (fun fmt () -> Pp.string fmt sep) (print_model_element me_name_trans) fmt m_elements
let print_model_file fmt filename model_file =
fprintf fmt "File %s:\n" filename;
let print_model_file fmt me_name_trans filename model_file =
fprintf fmt "File %s:" filename;
IntMap.iter
(fun line m_elements ->
fprintf fmt "Line %d:\n" line;
print_model_elements fmt m_elements)
fprintf fmt "\nLine %d:\n" line;
print_model_elements me_name_trans fmt m_elements)
model_file
let print_model fmt model =
StringMap.iter (print_model_file fmt) model
let why_name_trans (me_name, me_type) =
match me_type with
| Result -> "result"
| Old -> "old" ^ " " ^ me_name
| Other -> me_name
let print_model
?(me_name_trans = why_name_trans)
fmt
~model () =
StringMap.iter (print_model_file fmt me_name_trans) model
let model_to_string model =
print_model str_formatter model;
let model_to_string
?(me_name_trans = why_name_trans)
model =
print_model ~me_name_trans str_formatter ~model ();
flush_str_formatter ()
let get_model_file model filename =
......@@ -173,10 +211,16 @@ let get_padding line =
Str.matched_string line
with Not_found -> ""
let interleave_line start_comment end_comment model_file (source_code, line_number) line =
let interleave_line
start_comment
end_comment
me_name_trans
model_file
(source_code, line_number)
line =
try
let model_elements = IntMap.find line_number model_file in
print_model_elements str_formatter model_elements ~sep:"; ";
print_model_elements me_name_trans str_formatter model_elements ~sep:"; ";
let cntexmp_line =
(get_padding line) ^
start_comment ^
......@@ -191,14 +235,16 @@ let interleave_line start_comment end_comment model_file (source_code, line_numb
let interleave_with_source
?(start_comment="(* ")
?(end_comment=" *)")
?(me_name_trans = why_name_trans)
model
filename
source_code =
~filename
~source_code =
try
let model_file = StringMap.find filename model in
let lines = Str.split (Str.regexp "^") source_code in
let (source_code, _) = List.fold_left
(interleave_line start_comment end_comment model_file)
(interleave_line
start_comment end_comment me_name_trans model_file)
("", 1)
lines in
source_code
......@@ -215,34 +261,41 @@ let print_model_value_json fmt me_value =
let model_elements_to_map_bindings model_elements =
List.fold_left
(fun map_bindings me ->
(me.me_name, me.me_value)::map_bindings
(me, me.me_value)::map_bindings
)
[]
model_elements
let print_model_elements_json fmt model_elements =
let print_model_elements_json me_name_to_str fmt model_elements =
Json.map_bindings
(fun i -> i)
me_name_to_str
print_model_value_json
fmt
(model_elements_to_map_bindings model_elements)
let print_model_elements_on_lines_json fmt model_file =
let print_model_elements_on_lines_json me_name_to_str fmt model_file =
Json.map_bindings
(fun i -> string_of_int i)
print_model_elements_json
(print_model_elements_json me_name_to_str)
fmt
(IntMap.bindings model_file)
let print_model_json fmt model =
let print_model_json
?(me_name_trans = why_name_trans)
fmt
~model =
let me_name_to_str = fun me ->
me_name_trans (me.me_name, me.me_type) in
Json.map_bindings
(fun s -> s)
print_model_elements_on_lines_json
(print_model_elements_on_lines_json me_name_to_str)
fmt
(StringMap.bindings model)
let model_to_string_json model =
print_model_json str_formatter model;
let model_to_string_json
?(me_name_trans = why_name_trans)
model =
print_model_json str_formatter ~me_name_trans ~model;
flush_str_formatter ()
......
......@@ -17,7 +17,7 @@
type model_value =
| Integer of string
| Array of model_array
| Other of string
| Unparsed of string
and arr_index = {
arr_index_key : int;
arr_index_value : model_value;
......@@ -54,11 +54,22 @@ val print_model_value : Format.formatter -> model_value -> unit
** Model elements
***************************************************************
*)
type model_element_type =
| Result
(* Result of a function call (if the counter-example is for postcondition) *)
| Old
(* Old value of function argument (if the counter-example is for postcondition) *)
| Other
(** Counter-example model elements. Each element represents
a counter-example for a single source-code element.*)
type model_element = {
me_name : string;
(** The name of the source-code element. *)
me_type : model_element_type;
(** The type of model element. *)
me_value : model_value;
(** Counter-example value for the element. *)
me_location : Loc.position option;
......@@ -98,21 +109,68 @@ val empty_model : model
***************************************************************
*)
val print_model : Format.formatter -> model -> unit
val print_model :
?me_name_trans:((string * model_element_type) -> string) ->
Format.formatter ->
model:model ->
unit ->
unit
(** Prints the counter-example model
@param me_name_trans the transformation of the model elements
names. The input is a pair consisting of the name of model
element and type of the model element. The output is the
name of the model element that should be displayed.
@param model the counter-example model to print
*)
val model_to_string :
?me_name_trans:((string * model_element_type) -> string) ->
model ->
string
(** See print_model *)
val model_to_string : model -> string
val print_model_json :
?me_name_trans:((string * model_element_type) -> string) ->
Format.formatter ->
model:model ->
unit
(** Prints counter-example model to json format.
val print_model_json : Format.formatter -> model -> unit
@param me_name_trans see print_model
@model the counter-example model to print.
*)
val model_to_string_json : model -> string
val model_to_string_json :
?me_name_trans:((string * model_element_type) -> string) ->
model ->
string
(** See print_model_json *)
val interleave_with_source :
?start_comment:string ->
?end_comment:string ->
?me_name_trans:((string * model_element_type) -> string) ->
model ->
string ->
string ->
filename:string ->
source_code:string ->
string
(** Given a source code and a counter-example model interleaves
the source code with information in about the counter-example.
That is, for each location in counter-example trace creates
a comment in the output source code with information about
values of counter-example model elements.
@param start_comment the string that starts a comment
@param end_comment the string that ends a comment
@param me_name_trans see print_model
@param model counter-example model
@param filename the file name of the source
@param source_code the input source code
@return the source code with added comments with information
about counter-example model
*)
(*
***************************************************************
......
......@@ -137,7 +137,7 @@ let print_prover_result fmt
fprintf fmt "%a (%.2fs%a)" print_prover_answer ans t print_steps s;
if m <> Model_parser.empty_model then begin
fprintf fmt "\nCounter-example model:";
Model_parser.print_model fmt m
Model_parser.print_model fmt ~model:m ()
end;
if ans == HighFailure then
fprintf fmt "@\nProver exit status: %a@\nProver output:@\n%s@."
......@@ -168,8 +168,9 @@ type pre_prover_call = unit -> prover_call
let save f = f ^ ".save"
let debug_print_model model =
Debug.dprintf debug "Call_provers: %s@." (Model_parser.model_to_string model)
let model_str = Model_parser.model_to_string model in
Debug.dprintf debug "Call_provers: %s@." model_str
let parse_prover_run res_parser time out ret on_timelimit timelimit ~printer_mapping =
let ans = match ret with
......
......@@ -23,16 +23,16 @@ output:
pairs:
| possible_space { [] }
| possible_space LPAREN term SPACE value RPAREN pairs
| possible_space LPAREN term SPACE value RPAREN pairs
{ (Model_parser.create_model_element ~name:$3 ~value:$5 ())::$7 }
possible_space:
| { "" }
| SPACE { $1 }
term:
| text { $1 }
| LPAREN term_list RPAREN
| LPAREN term_list RPAREN
{ "(" ^ $2 ^ ")" }
term_list:
......@@ -52,25 +52,25 @@ text_without_int:
value:
| integer { $1 }
| other_val_str { Model_parser.Other $1 }
| other_val_str { Model_parser.Unparsed $1 }
| array { Model_parser.Array $1 }
integer:
| INT_STR { Model_parser.Integer $1 }
| LPAREN possible_space MINUS_INT_STR possible_space RPAREN
| LPAREN possible_space MINUS_INT_STR possible_space RPAREN
{ Model_parser.Integer $3 }
(* Everything that cannot be integer (positive and negative) and array. *)
other_val_str:
| text_without_int { $1 }
| LPAREN possible_space RPAREN { "(" ^ $2 ^ ")" }
| LPAREN possible_space paren_other_val_str RPAREN
| LPAREN possible_space paren_other_val_str RPAREN
{ "(" ^ $3 ^ ")" }
(* 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
| LPAREN possible_space other_than_const_array possible_space RPAREN
{ "(" ^ $3 ^ ")" }
other_than_neg_int_and_array_store:
......@@ -87,19 +87,18 @@ 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
| LPAREN possible_space
STORE possible_space array possible_space integer SPACE integer
possible_space
RPAREN
possible_space
RPAREN
{ Model_parser.array_add_element ~array:$5 ~index:$7 ~value:$9 }
array_skipped_part:
| LPAREN term_list RPAREN {}
......@@ -643,12 +643,10 @@ let update_tabs a =
match a.S.proof_state with
| S.Done r ->
if r.Call_provers.pr_model <> Model_parser.empty_model then begin
Model_parser.model_to_string r.Call_provers.pr_model ^ "\n" ^
Model_parser.model_to_string_json r.Call_provers.pr_model ^ "\n\n" ^
(Model_parser.interleave_with_source
r.Call_provers.pr_model
!current_file
(Sysutil.file_contents !current_file))
Model_parser.interleave_with_source
r.Call_provers.pr_model
~filename:!current_file
~source_code:(Sysutil.file_contents !current_file)
end else
""
| _ -> ""
......
......@@ -43,7 +43,7 @@ end
| Lstr lab ->
lab = model_label
let model_lab_present labels =
let model_lab_present labels =
try
ignore(List.find is_model_label labels);
true
......@@ -55,9 +55,9 @@ end
let is_model_trace_label l =
match l with
| Lpos _ -> false
| Lstr lab ->
| Lstr lab ->
try
ignore(Str.search_forward model_trace_regexp lab.lab_string 0);
ignore(Str.search_forward model_trace_regexp lab.Ident.lab_string 0);
true
with Not_found -> false
......@@ -69,10 +69,10 @@ end
false
let add_model_trace name labels =
if (model_lab_present labels) && (not (model_trace_lab_present labels)) then
if (model_lab_present labels) && (not (model_trace_lab_present labels)) then
(Lstr (Ident.create_label ("model_trace:" ^ name)))::labels
else
labels
labels
let add_lab id l =
let l = add_model_trace id.id_str l in
......
......@@ -87,7 +87,7 @@ type vc_line_info = {
mutable vc_loc : Loc.position option;
(* the position of VC line *)
mutable vc_func_name : string option;
(* the name of the function (just for the case VC is
(* the name of the function. None if VC is not generated for
postcondition or precondition) *)
}
......@@ -170,23 +170,47 @@ let label_starts_with regexp l =
let get_label labels regexp =
Slab.choose (Slab.filter (label_starts_with regexp) labels)
let labels_at_vc_pos ~labels =
let add_old lab_str =
try
let pos = Str.search_forward (Str.regexp "@") lab_str 0 in
let after = String.sub lab_str pos ((String.length lab_str)-pos) in
if after = "@init" then
(String.sub lab_str 0 pos) ^ "@old"
else lab_str
with Not_found -> lab_str ^ "@old"
let model_trace_for_postcondition ~labels =
(* Modifies the model_trace label of a term in the postcondition:
- if term corresponds to the initial value of a function
parameter, model_trace label will have postfix @old
- if term corresponds to the return value of a function, add
model_trace label in a form function_name@result
*)
try
let trace_label = get_label labels model_trace_regexp in
try
ignore(Str.search_forward (Str.regexp "@") trace_label.lab_string 0);
let lab_str = add_old trace_label.lab_string in
if lab_str = trace_label.lab_string then
labels
with Not_found ->
else
let other_labels = Slab.remove trace_label labels in
let new_label = Ident.create_label (trace_label.lab_string^"@"^"old") in
Slab.add new_label other_labels
Slab.add
(Ident.create_label lab_str)
other_labels
with Not_found ->
(* no model_trace label => the term represents the return value *)
Slab.add
(Ident.create_label
("model_trace:" ^ (Opt.get_def "" vc_line_info.vc_func_name) ^ "@result"))
labels
let get_fun_name name =
let splitted = Str.bounded_split (Str.regexp_string ":") name 2 in
match splitted with
| _::[second] ->
second
| _ ->
""
let check_enter_vc_line t =
(* Check whether the term corresponding to the line of VC is entered.
If it is entered, extract the location of VC line and if the VC is
......@@ -198,11 +222,8 @@ let check_enter_vc_line t =
vc_line_info.vc_loc <- t.t_loc;
try
(* Extract the function name from "model_func" label *)
let fun_label = get_label t.t_label (Str.regexp "model_func:") in
let str_lab = fun_label.lab_string in
let func_name_start = 11 in
let func_name_len = (String.length str_lab) - 11 in
vc_line_info.vc_func_name <- Some (String.sub str_lab func_name_start func_name_len);
let fun_label = get_label t.t_label (Str.regexp "model_func") in
vc_line_info.vc_func_name <- Some (get_fun_name fun_label.lab_string);
with Not_found ->
(* No label "model_func" => the VC is not postcondition or precondition *)
()
......@@ -262,7 +283,11 @@ let rec print_term info fmt t =
match vc_line_info.vc_loc with
| None -> ()
| Some loc ->
let labels = labels_at_vc_pos ~labels:ls.ls_name.id_label in
let labels = match vc_line_info.vc_func_name with
| None ->
ls.ls_name.id_label
| Some _ ->
model_trace_for_postcondition ~labels:ls.ls_name.id_label in
let t_check_pos = t_label ~loc labels t in
info.info_model <- S.add t_check_pos info.info_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