diff options
Diffstat (limited to 'mppa_k1c/Asmblock.v')
| -rw-r--r-- | mppa_k1c/Asmblock.v | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 4f9fc34d..03c7e6d5 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -179,6 +179,8 @@ Inductive ex_instruction : Type := | Pbuiltin: external_function -> list (builtin_arg preg) -> builtin_res preg -> ex_instruction (**r built-in function (pseudo) *) + | Pdiv (**r 32 bits integer division, call to __divdi3 *) + | Pdivu (**r 32 bits integer division, call to __udivdi3 *) . (** FIXME: comment not up to date ! @@ -523,9 +525,8 @@ Proof. assert (b :: body = nil). eapply H; eauto. discriminate. - destruct body; destruct exit. all: simpl; auto; try constructor. - + exploreInst. + + exploreInst; try discriminate. simpl. contradiction. - discriminate. + intros. discriminate. Qed. @@ -1437,10 +1438,20 @@ Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) | (None, _) => Stuck end - (** Pseudo-instructions *) | Pbuiltin ef args res => Stuck (**r treated specially below *) + | Pdiv => + match Val.divs (rs GPR0) (rs GPR1) with + | Some v => Next (rs # GPR0 <- v # RA <- (rs RA)) m + | None => Stuck + end + + | Pdivu => + match Val.divu (rs GPR0) (rs GPR1) with + | Some v => Next (rs # GPR0 <- v # RA <- (rs RA)) m + | None => Stuck + end end | None => Next rs m end. |