diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-09 08:02:36 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-09 08:02:36 +0100 |
commit | a36948c2af873559e5df4a2d96fdbc5bbfcfaca8 (patch) | |
tree | 29f34dce4fde3af7073c6090fbc59faac24f1bdf | |
parent | 5787da9e4d024dc3a3190bff0fe29385abbcece9 (diff) | |
download | compcert-kvx-a36948c2af873559e5df4a2d96fdbc5bbfcfaca8.tar.gz compcert-kvx-a36948c2af873559e5df4a2d96fdbc5bbfcfaca8.zip |
fix bug and forward in proofs
-rw-r--r-- | backend/ForwardMoves.v | 3 | ||||
-rw-r--r-- | backend/ForwardMovesproof.v | 17 |
2 files changed, 18 insertions, 2 deletions
diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v index 0e71b6b5..660d0458 100644 --- a/backend/ForwardMoves.v +++ b/backend/ForwardMoves.v @@ -250,13 +250,14 @@ Fixpoint kill_builtin_res (res : builtin_res reg) (rel : RELATION.t) := Definition apply_instr instr x := match instr with | Inop _ + | Icond _ _ _ _ | Istore _ _ _ _ _ => Some x | Iop Omove (src :: nil) dst _ => Some (move src dst x) | Iop _ _ dst _ | Iload _ _ _ _ dst _ | Icall _ _ _ dst _ => Some (kill dst x) | Ibuiltin _ _ res _ => Some (kill_builtin_res res x) - | Icond _ _ _ _ | Itailcall _ _ _ | Ijumptable _ _ | Ireturn _ => RB.bot + | Itailcall _ _ _ | Ijumptable _ _ | Ireturn _ => RB.bot end. Definition apply_instr' code (pc : node) (ro : RB.t) : RB.t := diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v index 99b546c7..aa516df4 100644 --- a/backend/ForwardMovesproof.v +++ b/backend/ForwardMovesproof.v @@ -403,7 +403,22 @@ Proof. rewrite subst_args_ok; eassumption. constructor; auto. - admit. + simpl in *. + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + apply get_rb_sem_ge with (rb2 := map # pc); trivial. + replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. + destruct b; tauto. + } + unfold apply_instr'. + unfold get_rb_sem in *. + destruct (map # pc) in *; try contradiction. + rewrite H. + reflexivity. (* jumptbl *) - econstructor; split. |