diff options
| -rw-r--r-- | backend/CSE3.v | 24 | ||||
| -rw-r--r-- | backend/CSE3analysisaux.ml | 2 | ||||
| -rw-r--r-- | backend/CSE3proof.v | 61 |
3 files changed, 78 insertions, 9 deletions
diff --git a/backend/CSE3.v b/backend/CSE3.v index df1c2bfc..482069d7 100644 --- a/backend/CSE3.v +++ b/backend/CSE3.v @@ -53,6 +53,24 @@ Definition forward_move_l_b (rb : RB.t) (xl : list reg) := Definition subst_args fmap pc xl := forward_move_l_b (PMap.get pc fmap) xl. +Definition find_cond_in_fmap fmap pc cond args := + match PMap.get pc fmap with + | Some rel => + if is_condition_present (ctx:=ctx) pc rel cond args + then Some true + else + let ncond := negate_condition cond in + if is_condition_present (ctx:=ctx) pc rel ncond args + then Some false + else let args' := subst_args fmap pc args in + if is_condition_present (ctx:=ctx) pc rel cond args' + then Some true + else if is_condition_present (ctx:=ctx) pc rel ncond args' + then Some false + else None + | None => None + end. + Definition transf_instr (fmap : PMap.t RB.t) (pc: node) (instr: instruction) := match instr with @@ -75,7 +93,11 @@ Definition transf_instr (fmap : PMap.t RB.t) | Itailcall sig ros args => Itailcall sig ros (subst_args fmap pc args) | Icond cond args s1 s2 expected => - Icond cond (subst_args fmap pc args) s1 s2 expected + let args' := subst_args fmap pc args in + match find_cond_in_fmap fmap pc cond args with + | None => Icond cond args' s1 s2 expected + | Some b => Inop (if b then s1 else s2) + end | Ijumptable arg tbl => Ijumptable (subst_arg fmap pc arg) tbl | Ireturn (Some arg) => diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index 1642a269..ab8cbeed 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -206,7 +206,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = let eq_find_oracle node eq = assert (not (is_trivial eq)); let o = Hashtbl.find_opt eq_table (flatten_eq eq) in - (if o = None then failwith "eq_find_oracle"); + (* FIXME (if o = None then failwith "eq_find_oracle"); *) (if !Clflags.option_debug_compcert > 5 then Printf.printf "@%d: eq_find %a -> %a\n" (P.to_int node) pp_eq eq (pp_option pp_P) o); diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 215f5c41..7af62b95 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -771,7 +771,28 @@ Proof. TR_AT. unfold transf_instr. rewrite FIND_COND. reflexivity. * replace bfound with b. { econstructor; eauto. - admit. + assert (is_inductive_allstep (ctx:= (context_from_hints (snd (preanalysis tenv f)))) f tenv (fst (preanalysis tenv f))) as IND by + (apply checked_is_inductive_allstep; + eapply transf_function_invariants_inductive; eassumption). + unfold is_inductive_allstep, is_inductive_step, apply_instr' in IND. + specialize IND with (pc:=pc) (pc':= if b then ifso else ifnot) (instr:= (Icond cond args ifso ifnot predb)). + cbn in IND. + rewrite H in IND. + assert (RB.ge (fst (preanalysis tenv f)) # (if b then ifso else ifnot) + match (fst (preanalysis tenv f)) # pc with + | Some x => apply_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc tenv (Icond cond args ifso ifnot predb) x + | None => None + end) as INDUCTIVE by (destruct b; intuition). + clear IND. + + change node with positive. + + destruct ((fst (preanalysis tenv f)) # pc). + 2: exfalso; exact REL. + + destruct ((fst (preanalysis tenv f)) # (if b then ifso else ifnot)). + - eapply rel_ge. exact INDUCTIVE. exact REL. + - cbn in INDUCTIVE. exfalso. exact INDUCTIVE. } unfold find_cond_in_fmap in FIND_COND. change RB.t with (option RELATION.t) in REL. @@ -796,12 +817,38 @@ Proof. inv FIND_COND. destruct b; trivial; cbn in H2; discriminate. } - rewrite <- subst_args_ok with (invariants := (fst (preanalysis tenv f))) (ctx := (context_from_hints (snd (preanalysis tenv f)))) (pc := pc) (sp:=sp) (m:=m) in COND_PRESENT_TRUE. - admit. - unfold fmap_sem. - change RB.t with (option RELATION.t). - rewrite FIND_REL. - exact REL. + clear COND_PRESENT_TRUE COND_PRESENT_FALSE. + pose proof (is_condition_present_sound pc rel cond (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) rs m REL) as COND_PRESENT_TRUE. + pose proof (is_condition_present_sound pc rel (negate_condition cond) (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) rs m REL) as COND_PRESENT_FALSE. + rewrite eval_negate_condition in COND_PRESENT_FALSE. + + destruct is_condition_present. + { rewrite subst_args_ok with (sp:=sp) (m:=m) in COND_PRESENT_TRUE. + { rewrite COND_PRESENT_TRUE in H0 by trivial. + congruence. + } + unfold fmap_sem. + change RB.t with (option RELATION.t). + rewrite FIND_REL. + exact REL. + } + destruct is_condition_present. + { rewrite subst_args_ok with (sp:=sp) (m:=m) in COND_PRESENT_FALSE. + { destruct (eval_condition cond rs ## args m) as [b0 | ]. + 2: discriminate. + inv H0. + cbn in COND_PRESENT_FALSE. + intuition. + inv H0. + inv FIND_COND. + destruct b; trivial; cbn in H2; discriminate. + } + unfold fmap_sem. + change RB.t with (option RELATION.t). + rewrite FIND_REL. + exact REL. + } + discriminate. + econstructor; split. * eapply exec_Icond with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption. ** TR_AT. unfold transf_instr. rewrite FIND_COND. |