note description: "Summary description for {AFX_FIX_SKELETON}." author: "" date: "$Date$" revision: "$Revision$" deferred class AFX_FIX_SKELETON inherit SHARED_SERVER AFX_SHARED_STATE_SERVER AFX_STATE_PARTITIONER REFACTORING_HELPER AFX_SHARED_BEHAVIOR_CONSTRUCTOR SHARED_EIFFEL_PARSER AFX_FIX_ID_SERVER AFX_SOLVER_FACTORY feature -- Access exception_spot: AFX_EXCEPTION_SPOT -- Exception related information precondition: EPA_STATE -- Fix precondition postcondition: EPA_STATE -- Fix postcondition guard_condition: detachable EPA_EXPRESSION -- Expression used as guard in the generated fix. -- If attached, generate fix like: (p is this guard): -- if p then -- snippet -- end -- -- If False, generate fix like: -- snippet relevant_ast: LINKED_LIST [AFX_AST_STRUCTURE_NODE] -- Relevant AST nodes, that may be modified by current fix. -- The order of the nodes in the list is important. -- If the list is empty, the fix is to be generated at the end of the recipient. -- Note: all the nodes in the list should also exist in `exception_spot'.`recipient_ast_structure'. fixes: LINKED_LIST [AFX_FIX] -- List of possible fixes all of which conforms to current skeleton -- Generated by the last `generate'. relevant_break_points: TUPLE [passing_bpslot: INTEGER; failing_bpslot: INTEGER] -- Relevant break points, one for passing runs, one for failing runs. -- Those break points will be used to infer state invariants. deferred end config: AFX_CONFIG -- Config for current AutoFix session test_case_execution_status: HASH_TABLE [AFX_TEST_CASE_EXECUTION_STATUS, STRING] -- Table of test case execution status -- Key is the UUID of a test case, value is the execution status -- assoicated with that test case feature -- Access ranking: AFX_FIX_RANKING -- Ranking for Current fix skeleton feature -- Status report is_relevant_ast_valid: BOOLEAN -- Is `relevant_ast' valid? do Result := True end is_afore: BOOLEAN -- Is Current an afore fix skeleton? do end is_wrap: BOOLEAN -- Is Current a wrap fix skeleton? do end is_simplification_needed: BOOLEAN -- Should precondition and postcondition be simplified? is_guard_condition_in_negation_form: BOOLEAN -- Is `guard_condition' in negation form? feature -- Setting set_guard_condition (a_condition: like guard_condition) -- Set `guard_condition' with `a_condition'. do guard_condition := a_condition ensure guard_condition_set: guard_condition = a_condition end set_precondition (a_precondition: like precondition) -- Set `precondition' with `a_precondition'. do precondition := a_precondition ensure precondition_set: precondition = a_precondition end set_postcondition (a_postcondition: like postcondition) -- Set `postcondition' with `a_postcondition'. do postcondition := a_postcondition ensure postcondition_set: postcondition = a_postcondition end set_relevant_ast (a_asts: like relevant_ast) -- Set `relevant_ast' with `a_asts'. do relevant_ast.wipe_out relevant_ast.append (a_asts) end set_ranking (a_ranking: like ranking) -- Set `ranking' with `a_ranking'. do ranking := a_ranking ensure ranking_set: ranking = a_ranking end set_is_simplification_needed (b: BOOLEAN) -- Set `is_simplification_needed' with `b'. do is_simplification_needed := b ensure is_simplification_needed_set: is_simplification_needed = b end set_is_guard_condition_in_negation_form (b: BOOLEAN) -- Set `is_guard_condition_in_negation_form' with `b'. do is_guard_condition_in_negation_form := b ensure is_guard_condition_in_negation_form_set: is_guard_condition_in_negation_form = b end feature -- Basic operations generate -- Generate fixes and store result in `fixes'. local l_passing_bpslot: INTEGER l_failing_bpslot: INTEGER l_contracts: like actual_fix_contracts l_precondition: detachable EPA_STATE l_postcondition: detachable EPA_STATE l_pre_hie: like state_hierarchy l_post_hie: like state_hierarchy l_premises: ARRAY [EPA_EXPRESSION] l_premise_skeleton: AFX_STATE_SKELETON l_premise_combi: LINKED_LIST [AFX_STATE_SKELETON] i, k: INTEGER l_snippets: like fix_snippets l_fix: AFX_FIX do create fixes.make -- Decide precondition and postcondition for the fix. l_contracts := actual_fix_contracts l_precondition := l_contracts.precondition l_postcondition := l_contracts.postcondition if l_precondition /= Void and then l_postcondition /= Void then -- and then not l_postcondition.is_empty then -- Postcondition are too large, we need to shrink it. if l_postcondition.count > config.max_fix_postcondition_assertion then l_postcondition := state_shrinker.shrinked_state (l_postcondition, config.max_fix_postcondition_assertion, exception_spot) end -- We only proceed if the postcondition is small enough. if l_postcondition.count <= config.max_fix_postcondition_assertion then -- Get all combinations of premises that we want to include in a fix. l_pre_hie := state_hierarchy (l_precondition) l_post_hie:= state_hierarchy (l_postcondition) l_snippets := fix_snippets (l_pre_hie, l_post_hie) generate_fixes_from_snippet (l_snippets, l_precondition, l_postcondition, False) else -- When the postcondition is too large, we just shortcut the original code, without trying to change the state. generate_fixes_from_snippet (l_snippets, l_precondition, l_postcondition, True) end end end feature{NONE} -- Implementation actual_fix_contracts: TUPLE [precondition: detachable EPA_STATE; postcondition: detachable EPA_STATE] -- Actual pre-/postconditions for current fix -- `precondition' or `postcondition' may be empty. local l_precondition: detachable EPA_STATE l_postcondition: detachable EPA_STATE l_bpslots: TUPLE [passing_bpslot: INTEGER; failing_bpslot: INTEGER] l_failing_state: detachable EPA_STATE l_necessary_conditions: AFX_STATE_SKELETON l_culprit_predicate: detachable EPA_EXPRESSION l_abq_analyzer: EPA_ABQ_STRUCTURE_ANALYZER l_value: BOOLEAN l_pre_equation: EPA_EQUATION l_post_equation: EPA_EQUATION l_culprits: LINKED_LIST [EPA_EXPRESSION] do l_bpslots := relevant_break_points -- Calculate actual precondition for current fix: -- 1. If the precondition is given, use the given one; -- 2. otherwise, use an empty precondition if attached {EPA_STATE} precondition as l_pre then if attached {AFX_DELAYED_STATE} l_pre as l_delayed_pre then l_delayed_pre.set_invariants_in_passing_runs (passing_state (l_bpslots.passing_bpslot)) l_delayed_pre.set_invariants_in_failing_runs (failing_state (l_bpslots.failing_bpslot)) l_precondition := l_delayed_pre.actual_state else l_precondition := l_pre end else create l_precondition.make (10, exception_spot.recipient_class_, exception_spot.recipient_) end -- Calculate actual postcondition for current fix: -- 1. If the postcondition is given, use the given one; -- 2. otherwise, calculate the postcodition from two break points. if attached {EPA_STATE} postcondition as l_post then if attached {AFX_DELAYED_STATE} l_post as l_delayed_post then l_delayed_post.set_invariants_in_passing_runs (passing_state (l_bpslots.passing_bpslot)) l_delayed_post.set_invariants_in_failing_runs (failing_state (l_bpslots.failing_bpslot)) l_postcondition := l_delayed_post.actual_state else l_postcondition := l_post end else Result := Void end -- When simplification is enabled (It is only enabled if the failing assertion is a single ABQ.), try -- to find out the necessary condition of the failing assertion. if is_simplification_needed then l_precondition := Void l_postcondition := Void l_failing_state := failing_state (l_bpslots.failing_bpslot) if l_failing_state /= Void then l_failing_state := state_shrinker.shrinked_state (l_failing_state, l_failing_state.count, exception_spot) -- Find out the set of ABQS which implies the negation of the failing assertion. l_necessary_conditions := solver_launcher.valid_premises (skeleton_with_value (l_failing_state), not exception_spot.failing_assertion, skeleton_from_state (l_failing_state).theory) if l_necessary_conditions.count > 1 then l_culprits := strongest_predicates (l_necessary_conditions, skeleton_from_state (l_failing_state).theory) if l_culprits.count >= 1 then l_culprit_predicate := l_culprits.first end elseif l_necessary_conditions.count = 1 then l_culprit_predicate := l_necessary_conditions.first else l_culprit_predicate := Void end if l_culprit_predicate /= Void then l_culprit_predicate := abq_predicate_from_equation_expression (l_culprit_predicate.text, l_culprit_predicate.class_, l_culprit_predicate.feature_) if attached guard_condition and then is_guard_condition_in_negation_form then set_guard_condition (l_culprit_predicate) else set_guard_condition (not l_culprit_predicate) end create l_abq_analyzer l_abq_analyzer.analyze (l_culprit_predicate) check l_abq_analyzer.is_matched end l_culprit_predicate := l_abq_analyzer.argumentless_boolean_query l_value := (l_abq_analyzer.negation_count \\ 2) = 0 create l_pre_equation.make (l_culprit_predicate, create {EPA_BOOLEAN_VALUE}.make (l_value)) create l_post_equation.make (l_culprit_predicate, create {EPA_BOOLEAN_VALUE}.make (not l_value)) l_precondition := equation_as_state (l_pre_equation) l_postcondition := equation_as_state (l_post_equation) end end end Result := [l_precondition, l_postcondition] end abq_predicate_from_equation_expression (a_text: STRING; a_class: CLASS_C; a_feature: FEATURE_I): EPA_AST_EXPRESSION -- ABQ predicate from `a_text' local l_parts: LIST [STRING] l_abq: STRING l_value: STRING l_text: STRING do l_parts := a_text.split ('=') check l_parts.count = 2 end l_abq := l_parts.first l_value := l_parts.last l_abq.left_adjust l_abq.right_adjust l_value.left_adjust l_value.right_adjust check l_value.is_boolean end if l_value.to_boolean then l_text := l_abq.twin else l_text := "not " + l_abq end create Result.make_with_text (a_class, a_feature, l_text, a_feature.written_class) end strongest_predicates (a_skeleton: AFX_STATE_SKELETON; a_theory: AFX_THEORY): LINKED_LIST [EPA_EXPRESSION] -- Expressions in `a_skeleton' which implies all the rest expressions in `a_skeleton'. -- `a_theory' is in which the reasoning is based. -- For example, if `a_skeleton' contains 3 predicates a, b, and c. -- If a->b and a->c, then a will be in the result. local l_tbl: HASH_TABLE [EPA_EXPRESSION, EPA_EXPRESSION] l_cursor: DS_HASH_SET_CURSOR [EPA_EXPRESSION] l_temp_skeleton: AFX_STATE_SKELETON l_implication: EPA_EXPRESSION l_implications: LINKED_LIST [EPA_EXPRESSION] l_valid_imps: LINKED_LIST [EPA_EXPRESSION] do create Result.make create l_implications.make create l_tbl.make (a_skeleton.count) l_tbl.compare_objects from l_cursor := a_skeleton.new_cursor l_cursor.start until l_cursor.after loop l_temp_skeleton := a_skeleton.cloned_object l_temp_skeleton.remove (l_cursor.item) l_implication := l_cursor.item implies l_temp_skeleton.anded l_tbl.put (l_cursor.item, l_implication) l_implications.extend (l_implication) l_cursor.forth end -- Collect all valid implications. l_valid_imps := solver_launcher.valid_expressions (l_implications, a_theory) if not l_valid_imps.is_empty then from l_valid_imps.start until l_valid_imps.after loop Result.extend (l_tbl.item (l_valid_imps.item_for_iteration)) l_valid_imps.forth end end end feature_body_compound_ast: EIFFEL_LIST [INSTRUCTION_AS] -- AST node for body of `exception_spot'.`recipient_' -- It is the compound part of a DO_AS. do if attached {BODY_AS} exception_spot.recipient_.body.body as l_body then if attached {ROUTINE_AS} l_body.content as l_routine then if attached {DO_AS} l_routine.routine_body as l_do then Result := l_do.compound end end end end feature_as_ast: FEATURE_AS -- AST for feature `exception_spot'.`recipient_' do Result := exception_spot.recipient_.e_feature.ast end generate_fixes_from_snippet (a_snippets: LINKED_LIST [TUPLE [snippet: STRING_8; ranking: INTEGER_32]]; a_precondition: EPA_STATE; a_postcondition: EPA_STATE; a_ignore_state_change: BOOLEAN) -- Generate fixes from `a_snippets' and store result in `fixes'. -- `a_precondition' and `a_postcondition' are not directly used for fix generation, -- they are passed to the actually generated fixes to provide better logging information. -- `a_ignore_state_change' indicates whether the fix generator try to change the state. deferred end state_hierarchy (a_state: EPA_STATE): HASH_TABLE [HASH_TABLE [EPA_STATE, STRING], EPA_EXPRESSION] -- hierarchically partitioned states from `a_state' local l_imp_parts: HASH_TABLE [EPA_STATE, EPA_EXPRESSION] l_prefix_parts: HASH_TABLE [EPA_STATE, STRING] do create Result.make (20) Result.compare_objects from l_imp_parts := partitions_by_premise (a_state) l_imp_parts.start until l_imp_parts.after loop l_prefix_parts := partitions_by_expression_prefix (l_imp_parts.item_for_iteration) Result.put (l_prefix_parts, l_imp_parts.key_for_iteration) l_imp_parts.forth end debug ("autofix") io.put_string ("== Original State =============================%N") io.put_string (a_state.debug_output + "%N") io.put_string ("== Hierarchy =============================%N") from Result.start until Result.after loop io.put_string ("Premise: " + Result.key_for_iteration.text + "%N") from Result.item_for_iteration.start until Result.item_for_iteration.after loop io.put_string ("%T" + Result.item_for_iteration.key_for_iteration + "%N") io.put_string (Result.item_for_iteration.item_for_iteration.debug_output + "%N") Result.item_for_iteration.forth end Result.forth end end end passing_state (a_passing_bpslot: INTEGER): detachable EPA_STATE -- State invariant (containg only predicates) from passing test cases at break point `a_passing_bpslot'. -- If no data is associated with the break point, return Void. local l_passing_state: EPA_STATE l_state: TUPLE [passing: AFX_DAIKON_RESULT; failing: AFX_DAIKON_RESULT] do l_state := state_server.state_for_fault (exception_spot.test_case_info) l_passing_state := l_state.passing.daikon_table.item (a_passing_bpslot) if l_passing_state = Void then l_passing_state := l_state.passing.daikon_table.item (exception_spot.recipient_.number_of_breakpoint_slots) end if l_passing_state /= Void then Result := l_passing_state.only_predicates end end failing_state (a_failing_bpslot: INTEGER): detachable EPA_STATE -- State invariant (containg only predicates) from failing test cases at break point `a_failing_bpslot'. -- If no data is associated with the break point, return Void. local l_failing_state: EPA_STATE l_state: TUPLE [passing: AFX_DAIKON_RESULT; failing: AFX_DAIKON_RESULT] do l_state := state_server.state_for_fault (exception_spot.test_case_info) l_failing_state := l_state.failing.daikon_table.item (a_failing_bpslot) if l_failing_state /= Void then Result := l_failing_state.only_predicates end end state_invariant_difference (a_passing_bpslot: INTEGER; a_failing_bpslot: INTEGER): detachable EPA_STATE -- State invariant difference between break point `a_passing_bpslot' in passing runs and -- break point `a_failing_bpslot' in failing runs. -- If no data is associated with either break point, return Void. local l_snippets: LINKED_LIST [ETR_TRANSFORMABLE] l_tran: ETR_TRANSFORMABLE l_passing_state: EPA_STATE l_failing_state: EPA_STATE l_state: TUPLE [passing: AFX_DAIKON_RESULT; failing: AFX_DAIKON_RESULT] l_state_diff: EPA_STATE do l_state := state_server.state_for_fault (exception_spot.test_case_info) l_passing_state := l_state.passing.daikon_table.item (a_passing_bpslot) l_failing_state := l_state.failing.daikon_table.item (a_failing_bpslot) if l_passing_state /= Void and then l_failing_state /= Void then l_passing_state := l_passing_state.only_predicates l_failing_state := l_failing_state.only_predicates Result := l_passing_state.subtraction (l_failing_state) end end state_transitions (a_source_state: HASH_TABLE [EPA_STATE, STRING]; a_target_state: HASH_TABLE [EPA_STATE, STRING]): LINKED_LIST [TUPLE [transitions: DS_LIST [STRING]; ranking: INTEGER]] -- List of transitions to direct state from `a_source_state' to `a_target_state' local l_source_state: DS_HASH_TABLE [EPA_STATE, STRING] l_target_state: DS_HASH_TABLE [EPA_STATE, STRING] l_class: CLASS_C l_feature: detachable FEATURE_I l_empty: LINKED_LIST [STRING] l_fixes: DS_ARRAYED_LIST [AFX_STATE_TRANSITION_FIX] do l_source_state := hash_table_to_ds_hash_table (a_source_state) l_target_state := hash_table_to_ds_hash_table (a_target_state) create l_empty.make l_target_state.do_all_with_key (agent ( item: EPA_STATE; key: STRING; a_list: LINKED_LIST [STRING]) do if item.is_empty then a_list.extend (key) end end (?, ?, l_empty)) l_empty.do_all (agent l_target_state.remove) -- Duplicate object path expression prefixes from target state to source state. fixme ("This may not be necessary in the future. 18.12.2009 Jasonw") l_target_state.do_all_with_key ( agent (item: EPA_STATE; key: STRING; data: DS_HASH_TABLE [EPA_STATE, STRING]) local l_dummy_state: EPA_STATE do if not data.has (key) then create l_dummy_state.make (0, item.class_, item.feature_) data.force (l_dummy_state, key) end end (?, ?, l_source_state)) l_fixes := state_transitions_from_model (l_source_state, l_target_state, exception_spot.recipient_written_class, Void, Void, False) create Result.make l_fixes.do_all ( agent (a_fix:AFX_STATE_TRANSITION_FIX; a_list: LINKED_LIST [TUPLE [transitions: DS_LIST [STRING]; ranking: INTEGER]]) do a_list.extend ([a_fix.call_sequence, a_fix.rank]) end (?, Result)) ensure result_attached: Result /= Void end hash_table_to_ds_hash_table (a_hash_table: HASH_TABLE [EPA_STATE, STRING]): DS_HASH_TABLE [EPA_STATE, STRING] -- DS_HASH_TABLE from HASH_TABLE local l_cursor: CURSOR do fixme ("To be removed. 18.12.2009 Jasonw") create Result.make (a_hash_table.count) Result.set_key_equality_tester (string_equality_tester) l_cursor := a_hash_table.cursor from a_hash_table.start until a_hash_table.after loop Result.force (a_hash_table.item_for_iteration, a_hash_table.key_for_iteration) a_hash_table.forth end a_hash_table.go_to (l_cursor) end call_sequences (a_source_state: like state_hierarchy; a_target_state: like state_hierarchy): HASH_TABLE [LINKED_LIST [TUPLE [transitions: DS_LIST [STRING]; ranking: INTEGER]], EPA_EXPRESSION] -- Possible call sequences to change the system from `a_source_state' to `a_target_state'. local l_source: detachable HASH_TABLE [EPA_STATE, STRING] do create Result.make (10) from a_target_state.start until a_target_state.after loop check a_target_state.key_for_iteration /= Void end l_source := a_source_state.item (a_target_state.key_for_iteration) if l_source = Void then create l_source.make (0) l_source.compare_objects end Result.force (state_transitions (l_source, a_target_state.item_for_iteration), a_target_state.key_for_iteration) a_target_state.forth end end text_of_fix (a_premise: EPA_EXPRESSION; a_sequences: DS_LIST [STRING]): STRING -- local l_tab: STRING do create Result.make (512) if not a_premise.is_true_expression then Result.append ("if ") Result.append (a_premise.text) Result.append (" then%N") l_tab := "%T" else l_tab := "" end from a_sequences.start until a_sequences.after loop Result.append (l_tab) Result.append (a_sequences.item_for_iteration) Result.append ("%N") a_sequences.forth end if not a_premise.is_true_expression then Result.append ("end%N") end end text_of_fixes (a_candidates: HASH_TABLE [LINKED_LIST [TUPLE [transitions: DS_LIST [STRING]; ranking: INTEGER]], EPA_EXPRESSION]): LINKED_LIST [TUPLE [snippet: STRING; ranking: INTEGER]] local l_array: ARRAY [TUPLE [seq: LINKED_LIST [TUPLE [transitions: DS_LIST [STRING]; ranking: INTEGER]]; premise: EPA_EXPRESSION]] i, j, c: INTEGER l_done: BOOLEAN l_ranking: INTEGER l_fix: STRING l_data: TUPLE [seq: LINKED_LIST [TUPLE [transitions: DS_LIST [STRING]; ranking: INTEGER]]; premise: EPA_EXPRESSION] l_premise: EPA_EXPRESSION l_finished: BOOLEAN l_premise_ranking: INTEGER do create Result.make c := a_candidates.count create l_array.make (1, c) from i := 1 a_candidates.start until a_candidates.after loop check a_candidates.key_for_iteration /= Void end a_candidates.item_for_iteration.start a_candidates.item_for_iteration.back l_array.put ([a_candidates.item_for_iteration, a_candidates.key_for_iteration], i) i := i + 1 a_candidates.forth end from i := 1 until l_done loop l_array.item (i).seq.forth if l_array.item (i).seq.after then l_array.item (i).seq.start l_array.item (i).seq.back i := i - 1 if i = 0 then l_done := True end else if i = c then create l_fix.make (1024) l_ranking := 0 from l_finished := False j := 1 until j > c or else l_finished loop l_data := l_array.item (j) l_premise := l_data.premise -- Call sequences generated to satisfy an implication are considered to be more complicated. if l_premise.is_true_expression then -- Simpler case. l_premise_ranking := 1 else -- Complicated case. l_premise_ranking := 2 end l_finished := l_data.seq.item_for_iteration.transitions.is_empty if not l_finished then l_fix.append (text_of_fix (l_premise, l_data.seq.item_for_iteration.transitions)) l_ranking := l_ranking + l_data.seq.item_for_iteration.ranking * (-1) * l_premise_ranking j := j + 1 end end if not l_finished then Result.extend ([l_fix, l_ranking]) end else i := i + 1 end end end end fix_snippets (a_source_state: like state_hierarchy; a_target_state: like state_hierarchy): LINKED_LIST [TUPLE [snippet: STRING; ranking: INTEGER]] -- Fix snippets to change the system from `a_source_state' to `a_target_state' local l_sequences: like call_sequences l_premise_skeleton: AFX_STATE_SKELETON i, k: INTEGER l_combinations: LINKED_LIST [AFX_STATE_SKELETON] l_temp: HASH_TABLE [LINKED_LIST [TUPLE [transitions: DS_LIST [STRING]; ranking: INTEGER]], EPA_EXPRESSION] l_comb: AFX_STATE_SKELETON do create Result.make l_sequences := call_sequences (a_source_state, a_target_state) create l_premise_skeleton.make_basic (exception_spot.recipient_class_, exception_spot.recipient_, 0) l_sequences.current_keys.do_all (agent l_premise_skeleton.force_last) from i := 1 k := 1 until i > k loop -- Get a combination of premises. l_combinations := l_premise_skeleton.combinations (i) from l_combinations.start until l_combinations.after loop l_comb := l_combinations.item_for_iteration create l_temp.make (l_comb.count) l_temp.compare_objects from l_comb.start until l_comb.after loop l_temp.force (l_sequences.item (l_comb.item_for_iteration), l_comb.item_for_iteration) l_comb.forth end Result.append (text_of_fixes (l_temp)) l_combinations.forth end i := i + 1 end end print_fix (a_fix: AFX_FIX) -- Print `a_fix'. local l_printer: ETR_AST_STRUCTURE_PRINTER l_output: ETR_AST_STRING_OUTPUT l_feat_text: STRING do if a_fix.feature_text.has_substring ("should not happen") then l_feat_text := a_fix.feature_text else entity_feature_parser.parse_from_string (a_fix.text , Void) create l_output.make_with_indentation_string ("%T") create l_printer.make_with_output (l_output) l_printer.print_ast_to_output (entity_feature_parser.feature_node) l_feat_text := l_output.string_representation end io.put_string ("------------------------------------------------%N") io.put_string (a_fix.information) io.put_string ("%N") io.put_string (l_feat_text) io.put_string ("%N") end end