(********************************************************************) (* *) (* The Why3 Verification Platform / The Why3 Development Team *) (* Copyright 2010-2015 -- INRIA - CNRS - Paris-Sud University *) (* *) (* This software is distributed under the terms of the GNU Lesser *) (* General Public License version 2.1, with the special exception *) (* on linking described in file LICENSE. *) (* *) (********************************************************************) open Decl open Term open Ident (** For see intro_vc_vars_counterexmp.mli for detailed description of this transformation. *) let meta_vc_location = Theory.register_meta_excl "vc_location" [Theory.MTstring] ~desc:"Location@ of@ the@ term@ that@ triggers@ vc@ in@ the@ form@ file:line:col." let model_label = Ident.create_label "model" (* Identifies terms that should be in counterexample and should not be projected. *) let model_projected_label = Ident.create_label "model_projected" (* Identifies terms that should be in counterexample and should be projected. *) let model_vc_label = Ident.create_label "model_vc" (* Identifies the term that triggers the VC. *) let model_vc_post_label = Ident.create_label "model_vc_post" (* Identifies the postcondition that triggers the VC. *) let model_trace_regexp = Str.regexp "model_trace:" (* The term labeled with "model_trace:name" will be in counterexample with name "name" *) (* Information about the term that triggers VC. *) type vc_term_info = { mutable vc_inside : bool; (* true if the term that triggers VC is currently processed *) mutable vc_loc : Loc.position option; (* the position of the term that triggers VC *) mutable vc_pre_or_post : bool; (* true if VC was generated for precondition or postcondition *) } let label_starts_with regexp l = try ignore(Str.search_forward regexp l.lab_string 0); true with Not_found -> false let get_label labels regexp = Slab.choose (Slab.filter (label_starts_with regexp) labels) let is_model_vc_label l = if l = model_vc_label || l = model_vc_post_label then true else false let check_enter_vc_term t info = (* Check whether the term that triggers VC is entered. If it is entered, extract the location of the term and if the VC is postcondition or precondition of a function, extract the name of the corresponding function. *) if Slab.exists is_model_vc_label t.t_label then begin info.vc_inside <- true; info.vc_loc <- t.t_loc; info.vc_pre_or_post <- Slab.mem model_vc_post_label t.t_label; end let check_exit_vc_term t info = (* Check whether the term triggering VC is exited. *) if Slab.exists is_model_vc_label t.t_label then begin info.vc_inside <- false; end 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 Returns labels with model_trace label modified if there exist model_trace label in labels, labels otherwise. *) try let trace_label = get_label labels model_trace_regexp in let lab_str = add_old trace_label.lab_string in if lab_str = trace_label.lab_string then labels else let other_labels = Slab.remove trace_label labels in Slab.add (Ident.create_label lab_str) other_labels with Not_found -> labels let rec do_intro info t = check_enter_vc_term t info; let defs = match t.t_node with | Tapp (ls, tl) -> begin match tl with | [] -> if info.vc_inside then begin match info.vc_loc with | None -> [] | Some loc -> (* variable inside the term T that triggers VC. If the variable should be in counterexample, introduce new constant in location loc with all labels necessary for collecting the it for counterexample and make it equal to the variable *) let is_counterexample_label l = if l = model_label || l = model_projected_label then true else false in if Slab.exists is_counterexample_label ls.ls_name.id_label then let const_label = if info.vc_pre_or_post then model_trace_for_postcondition ~labels:ls.ls_name.id_label else ls.ls_name.id_label in let const_name = ls.ls_name.id_string^"_vc_constant" in let axiom_name = ls.ls_name.id_string^"_vc_axiom" in Intro_projections_counterexmp.intro_const_equal_to_term ~term:t ~const_label ~const_loc:loc ~const_name ~axiom_name else [] end else [] | _ -> List.fold_left (fun defs term -> List.append defs (do_intro info term)) [] tl end; | Tbinop (_, f1, f2) -> List.append (do_intro info f1) (do_intro info f2) | Tquant (_, fq) -> let _, _, f = t_open_quant fq in do_intro info f | Tlet (t, tb) -> let _, f = t_open_bound tb in List.append (do_intro info t) (do_intro info f) | Tnot f -> do_intro info f | Tif (f1, f2, f3) -> List.append (List.append (do_intro info f1) (do_intro info f2)) (do_intro info f3) | Tcase (t, _) -> do_intro info t (* todo: handle the second argument of Tcase *) | _ -> [] in check_exit_vc_term t info; defs let do_intro_vc_vars_counterexmp info pr f = List.append (do_intro info f) [(create_prop_decl Pgoal pr f)] let intro_vc_vars_counterexmp2 task = let info = { vc_inside = false; vc_loc = None; vc_pre_or_post = false; } in (* Do introduction and find location of term triggering VC *) let do_intro_trans = Trans.goal (do_intro_vc_vars_counterexmp info) in let task = (Trans.apply do_intro_trans) task in (* Pass meta with location of the term triggering VC to printer *) let vc_loc_meta = Theory.lookup_meta "vc_location" in let g,task = Task.task_separate_goal task in let pos_str = match info.vc_loc with | None -> "" | Some loc -> let (file, line, col1, col2) = Loc.get loc in file ^ ":" ^ (string_of_int line) ^ ":" ^ (string_of_int col1) ^ ":" ^ (string_of_int col2) in let task = Task.add_meta task vc_loc_meta [Theory.MAstr pos_str] in Task.add_tdecl task g let intro_vc_vars_counterexmp = Trans.store intro_vc_vars_counterexmp2 let () = Trans.register_transform "intro_vc_vars_counterexmp" intro_vc_vars_counterexmp ~desc:"Introduce." let get_location_of_vc task = let meta_args = Task.on_meta_excl meta_vc_location task in match meta_args with | Some [Theory.MAstr loc_str] -> let splitted = Strings.bounded_split ':' loc_str 4 in let loc = match splitted with | [filename; line; col1; col2] -> let line = int_of_string line in let col1 = int_of_string col1 in let col2 = int_of_string col2 in Some (Loc.user_position filename line col1 col2) | _ -> None in loc | _ -> None