Commit 6d1052d2 authored by Sylvain Dailler's avatar Sylvain Dailler

Allow locations to be printed in the counterexample tab.

Source_and_ce now takes locations as arguments too. The server now uses
the source to compute a new list of locations which corresponds to correct
locations in a file where counterexample comments are added.
parent 546ef906
......@@ -411,25 +411,55 @@ let get_padding line =
Str.matched_string line
with Not_found -> ""
(* This assumes that l is sorted and split the list of locations in two:
those that are applied on this line and the others. For those that are on
this line, we split the locations that appear on several lines. *)
let rec partition_loc line lc l =
match l with
| (hd,a) :: tl ->
let (hdf, hdl, hdfc, hdlc) = Loc.get hd in
if hdl = line then
if hdlc > lc then
let old_sloc = Loc.user_position hdf hdl hdfc lc in
let newlc = hdlc - lc in
let new_sloc = Loc.user_position hdf (hdl + 1) 1 newlc in
let (rem_loc, new_loc) = partition_loc line lc tl in
((new_sloc,a) :: rem_loc, (old_sloc,a) :: new_loc)
else
let (rem_loc, new_loc) = partition_loc line lc tl in
(rem_loc, (hd,a) :: new_loc)
else
(l, [])
| _ -> (l, [])
(* Change a locations so that it points to a different line number *)
let add_offset off (loc, a) =
let (f, l, fc, lc) = Loc.get loc in
(Loc.user_position f (l + off) fc lc, a)
let interleave_line
start_comment
end_comment
me_name_trans
model_file
(source_code, line_number)
(source_code, line_number, offset, remaining_locs, locs)
line =
let remaining_locs, list_loc =
partition_loc line_number (String.length line) remaining_locs
in
let list_loc = List.map (add_offset offset) list_loc in
try
let model_elements = IntMap.find line_number model_file in
print_model_elements print_model_value_human me_name_trans str_formatter model_elements ~sep:"; ";
let cntexmp_line =
(get_padding line) ^
start_comment ^
(flush_str_formatter ()) ^
end_comment in
start_comment ^
(flush_str_formatter ()) ^
end_comment in
(source_code ^ line ^ cntexmp_line ^ "\n", line_number + 1)
(source_code ^ line ^ cntexmp_line ^ "\n", line_number + 1, offset + 1, remaining_locs, list_loc @ locs)
with Not_found ->
(source_code ^ line, line_number + 1)
(source_code ^ line, line_number + 1, offset, remaining_locs, list_loc @ locs)
let interleave_with_source
......@@ -438,21 +468,29 @@ let interleave_with_source
?(me_name_trans = why_name_trans)
model
~filename
~source_code =
~rel_filename
~source_code
~locations =
let locations =
List.sort (fun x y -> compare (fst x) (fst y))
(List.filter (fun x -> let (f, _, _, _) = Loc.get (fst x) in f = rel_filename) locations)
in
try
let model_file = StringMap.find filename model.model_files in
let src_lines_up_to_last_cntexmp_el source_code model_file =
let (last_cntexmp_line, _) = IntMap.max_binding model_file in
Str.bounded_split (Str.regexp "^") source_code (last_cntexmp_line+1)
in
let (source_code, _) = List.fold_left
(interleave_line
start_comment end_comment me_name_trans model_file)
("", 1)
(src_lines_up_to_last_cntexmp_el source_code model_file) in
source_code
let (source_code, _, _, _, gen_loc) =
List.fold_left
(interleave_line
start_comment end_comment me_name_trans model_file)
("", 1, 0, locations, [])
(src_lines_up_to_last_cntexmp_el source_code model_file)
in
source_code, gen_loc
with Not_found ->
source_code
source_code, locations
(*
......
......@@ -260,8 +260,10 @@ val interleave_with_source :
?me_name_trans:(model_element_name -> string) ->
model ->
filename:string ->
rel_filename:string ->
source_code:string ->
string
locations:(Loc.position * 'a) list ->
string * (Loc.position * 'a) list
(** 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
......@@ -273,10 +275,14 @@ val interleave_with_source :
@param me_name_trans see print_model
@param model counter-example model
@param filename the file name of the source
@param rel_filename the file name of the source relative to the session
@param source_code the input source code
@param locations the source locations that are found in the code
@return the source code with added comments with information
about counter-example model
about counter-example model. The second part of the pair are
locations modified so that it takes into account that counterexamples
were added.
*)
(*
......
......@@ -949,6 +949,8 @@ let counterexample_view =
~packing:scrolled_counterexample_view#add
()
(* Allow colors locations on counterexample view *)
let () = create_colors counterexample_view
let message_zone =
let sv = GBin.scrolled_window
......@@ -1159,10 +1161,13 @@ let move_to_line ~yalign (v : GSourceView2.source_view) line =
(* Add a color tag on the right locations on the correct file.
If the file was not open yet, nothing is done *)
let color_loc ~color loc =
let color_loc ?(ce=false) ~color loc =
let f, l, b, e = Loc.get loc in
try
let (_, v, _, _) = get_source_view_table f in
let v = if ce then counterexample_view else
let (_, v, _, _) = get_source_view_table f in
v
in
let color = convert_color color in
color_loc ~color v l b e
with
......@@ -1203,6 +1208,14 @@ let apply_loc_on_source (l: (Loc.position * color) list) =
in
scroll_to_loc ~force_tab_switch:false loc_of_goal
(* Erase the colors and apply the colors given by l (which come from the task)
to the counterexample tab *)
let apply_loc_on_ce (l: (Loc.position * color) list) =
erase_color_loc counterexample_view;
List.iter (fun (loc, color) ->
color_loc ~ce:true ~color loc) l
(*******************)
(* The "View" menu *)
(*******************)
......@@ -2283,10 +2296,11 @@ let treat_notification n =
with
| Not_found -> create_source_view file_name content
end
| Source_and_ce (content) ->
| Source_and_ce (content, list_loc) ->
begin
messages_notebook#goto_page counterexample_page;
counterexample_view#source_buffer#set_text content;
apply_loc_on_ce list_loc
end
| Dead _ ->
print_message ~kind:1 ~notif_kind:"Server Dead ?"
......
......@@ -100,8 +100,8 @@ type notification =
etc) *)
| File_contents of string * string
(* File_contents (filename, contents) *)
| Source_and_ce of string
(* Source interleaved with counterexamples: contents *)
| Source_and_ce of string * (Loc.position * color) list
(* Source interleaved with counterexamples: contents and list color loc *)
type ide_request =
| Command_req of node_ID * string
......
......@@ -108,8 +108,8 @@ type notification =
etc) *)
| File_contents of string * string
(** File_contents (filename, contents) *)
| Source_and_ce of string
(** Source interleaved with counterexamples: contents *)
| Source_and_ce of string * (Loc.position * color) list
(** Source interleaved with counterexamples: contents and list color loc *)
type ide_request =
| Command_req of node_ID * string
......
......@@ -329,7 +329,7 @@ let print_notify fmt n =
print_msg fmt msg
| Dead s -> fprintf fmt "dead :%s" s
| File_contents (_f, _s) -> fprintf fmt "file contents"
| Source_and_ce (_s) -> fprintf fmt "source and ce"
| Source_and_ce (_s, _list_loc) -> fprintf fmt "source and ce"
| Task (ni, _s, list_loc) ->
fprintf fmt "task for node_ID %d which contains a list of loc %a"
ni print_list_loc list_loc
......@@ -894,22 +894,15 @@ end
in
task_text, loc_color_list
(* This notify the counterexample tab which should contain a counterexample
interleaved with source code
*)
let notify_ce_tab s res any =
let create_ce_tab s res any list_loc =
let f = get_encapsulating_file s any in
let filename = Sysutil.absolutize_filename
(Session_itp.get_dir s) (file_name f)
in
let source_code = Sysutil.file_contents filename in
let ce_result =
Model_parser.interleave_with_source ?start_comment:None ?end_comment:None
?me_name_trans:None res.Call_provers.pr_model ~filename:filename
~source_code:source_code
in
P.notify (Source_and_ce ce_result)
Model_parser.interleave_with_source ?start_comment:None ?end_comment:None
?me_name_trans:None res.Call_provers.pr_model ~filename:filename ~rel_filename:(file_name f)
~source_code:source_code ~locations:list_loc
let send_task nid show_full_context loc =
let d = get_server_data () in
......@@ -944,10 +937,10 @@ end
let pa = get_proof_attempt_node d.cont.controller_session pid in
let parid = pa.parent in
let name = Pp.string_of Whyconf.print_prover pa.prover in
let s, list_loc = task_of_id d parid show_full_context loc in
let s, old_list_loc = task_of_id d parid show_full_context loc in
let prover_text = s ^ "\n====================> Prover: " ^ name ^ "\n" in
(* Display the result of the prover *)
let prover_ce =
begin
match pa.proof_state with
| Some res ->
let result =
......@@ -956,18 +949,26 @@ end
in
let ce_result =
Pp.string_of (Model_parser.print_model_human ?me_name_trans:None)
res.Call_provers.pr_model
res.Call_provers.pr_model
in
if ce_result = "" then
result ^ "\n\n" ^ "The prover did not return counterexamples."
let result_pr =
result ^ "\n\n" ^ "The prover did not return counterexamples."
in
P.notify (Task (nid, prover_text ^ result_pr, old_list_loc))
else
begin
notify_ce_tab d.cont.controller_session res any;
result ^ "\n\n" ^ "Counterexample suggested by the prover:\n\n" ^ ce_result
let result_pr =
result ^ "\n\n" ^ "Counterexample suggested by the prover:\n\n" ^ ce_result
in
let (source_result, list_loc) =
create_ce_tab d.cont.controller_session res any old_list_loc
in
P.notify (Source_and_ce (source_result, list_loc));
P.notify (Task (nid, prover_text ^ result_pr, old_list_loc))
end
| None -> "Result of the prover not available.\n"
in
P.notify (Task (nid, prover_text ^ prover_ce, list_loc))
| None -> P.notify (Task (nid, "Result of the prover not available.\n", old_list_loc))
end
| AFile f ->
P.notify (Task (nid, "File " ^ file_name f, []))
| ATn tid ->
......
......@@ -370,9 +370,10 @@ let print_notification_to_json (n: notification): json =
convert_record ["notification", cc n;
"file", String f;
"content", String s]
| Source_and_ce (s) ->
| Source_and_ce (s, list_loc) ->
convert_record ["notification", cc n;
"content", String s])
"content", String s;
"loc_list", convert_list_loc list_loc])
let print_notification fmt (n: notification) =
Format.fprintf fmt "%a" print_json (print_notification_to_json n)
......@@ -705,7 +706,8 @@ let parse_notification constr j =
| "Source_and_ce" ->
let s = get_string (get_field j "content") in
Source_and_ce(s)
let l = get_field j "loc_list" in
Source_and_ce(s, parse_list_loc l)
| s -> raise (NotNotification ("<from parse_notification> " ^ s))
......
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