From b3e2078df318a2d5e54de0b09963f37d63327f0a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 12 May 2022 20:47:14 +0100 Subject: Famous proven but not tested has been fixed --- src/hls/Partition.ml | 2 +- src/hls/RTLPargen.v | 2 +- src/hls/RTLPargenproof.v | 22 +++++++++++----------- 3 files changed, 13 insertions(+), 13 deletions(-) (limited to 'src') diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml index 545277b..4e699e6 100644 --- a/src/hls/Partition.ml +++ b/src/hls/Partition.ml @@ -73,7 +73,7 @@ let rec next_bblock_from_RTL is_start e (c : RTL.code) s i = if List.exists (fun x -> x = s) (fst e) then Errors.OK { bb_body = [i']; bb_exit = RBgoto s' } else if List.exists (fun x -> x = s) (snd e) && not is_start then - Errors.OK { bb_body = [RBnop]; bb_exit = RBgoto s } + Errors.OK { bb_body = []; bb_exit = RBgoto s } else begin match next_bblock_from_RTL false e c s' i_n with | Errors.OK bb -> diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 214da6f..d425049 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -227,7 +227,7 @@ We define the top-level oracle that will check if two basic blocks are equivalent after a scheduling transformation. |*) -Definition empty_trees (bb: list RTLBlock.bb) (bbt: list RTLPar.bb) : bool := +Definition empty_trees (bb: RTLBlock.bb) (bbt: RTLPar.bb) : bool := match bb with | nil => match bbt with diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index 689c11a..f975601 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -590,7 +590,7 @@ Proof. econstructor; auto. match goal with H: eval_pred _ _ _ _ |- _ => inv H end. repeat econstructor; try erewrite match_states_list; eauto. - - destruct p. match goal with H: eval_pred _ _ _ _ |- _ => inv H end. + (*- destruct p. match goal with H: eval_pred _ _ _ _ |- _ => inv H end. repeat econstructor; try erewrite match_states_list; eauto. erewrite <- eval_predf_pr_equiv; eassumption. apply PTree_matches; assumption. @@ -615,7 +615,7 @@ Proof. match goal with H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto end. - - admit. Admitted. + - admit.*) Admitted. Lemma step_instr_list_matches : forall a ge sp st st', @@ -799,22 +799,22 @@ Definition match_prog (prog : RTLBlock.program) (tprog : RTLPar.program) := (* TODO: Fix the `bb` and add matches for them. *) Inductive match_stackframes: RTLBlock.stackframe -> RTLPar.stackframe -> Prop := | match_stackframe: - forall f tf res sp pc rs rs' ps ps' bb bb', + forall f tf res sp pc rs rs' ps ps', transl_function f = OK tf -> (forall x, rs !! x = rs' !! x) -> (forall x, ps !! x = ps' !! x) -> - match_stackframes (Stackframe res f sp pc bb rs ps) - (Stackframe res tf sp pc bb' rs' ps'). + match_stackframes (Stackframe res f sp pc rs ps) + (Stackframe res tf sp pc rs' ps'). Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop := | match_state: - forall sf f sp pc rs rs' m sf' tf ps ps' bb bb' + forall sf f sp pc rs rs' m sf' tf ps ps' (TRANSL: transl_function f = OK tf) (STACKS: list_forall2 match_stackframes sf sf') (REG: forall x, rs !! x = rs' !! x) (REG: forall x, ps !! x = ps' !! x), - match_states (State sf f sp pc bb rs ps m) - (State sf' tf sp pc bb' rs' ps' m) + match_states (State sf f sp pc rs ps m) + (State sf' tf sp pc rs' ps' m) | match_returnstate: forall stack stack' v m (STACKS: list_forall2 match_stackframes stack stack'), @@ -1044,11 +1044,11 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. (* TODO: Fix these proofs, now the cf_instr is in the State. *) Lemma step_cf_instr_correct: - forall t s s', - step_cf_instr ge s t s' -> + forall t s s' cf, + step_cf_instr ge s cf t s' -> forall r, match_states s r -> - exists r', step_cf_instr tge r t r' /\ match_states s' r'. + exists r', step_cf_instr tge r cf t r' /\ match_states s' r'. Proof using TRANSL. (*induction 1; repeat semantics_simpl; -- cgit