diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-02-20 15:04:15 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-02-20 15:05:56 +0100 |
| commit | 20cb5c46636c5a855efd49ea6459af12211d7bd0 (patch) | |
| tree | 8ec790fda676dce1f8074189d8012092ef8e28f5 /mppa_k1c | |
| parent | a17303a44371cd867a4df647bf566f4a101bf5aa (diff) | |
| download | compcert-kvx-20cb5c46636c5a855efd49ea6459af12211d7bd0.tar.gz compcert-kvx-20cb5c46636c5a855efd49ea6459af12211d7bd0.zip | |
Remove unnecessary and error prone FR constructor for pregs
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Asmblock.v | 7 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 6 | ||||
| -rw-r--r-- | mppa_k1c/Asmexpand.ml | 1 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 2 |
4 files changed, 5 insertions, 11 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index a582e866..b9c50517 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -65,17 +65,15 @@ Proof. decide equality. Defined. (** basic register *) Inductive preg: Type := - | IR: gpreg -> preg (**r integer registers *) - | FR: gpreg -> preg (**r float registers *) + | IR: gpreg -> preg (**r integer general purpose registers *) | RA: preg | PC: preg . Coercion IR: gpreg >-> preg. -Coercion FR: gpreg >-> preg. Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}. -Proof. decide equality. apply ireg_eq. apply freg_eq. Defined. +Proof. decide equality. apply ireg_eq. Defined. Module PregEq. Definition t := preg. @@ -1436,7 +1434,6 @@ Definition data_preg (r: preg) : bool := | IR GPRA => false | IR RTMP => false | IR _ => true - | FR _ => true | PC => false end. diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 14a84b6a..9cba8402 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -1076,8 +1076,8 @@ Lemma nextblock_preserves: rs r = rs' r.
Proof.
intros. destruct r; try discriminate.
- - subst. Simpl.
- - subst. Simpl.
+ subst. Simpl.
+(* - subst. Simpl. *)
Qed.
Lemma cons3_app {A: Type}:
@@ -1274,7 +1274,7 @@ Proof. assert (forall r : preg, r <> PC -> rs' r = rs2 r).
{ intros. destruct r.
- destruct g. all: rewrite INV; Simpl; auto.
- - destruct g. all: rewrite INV; Simpl; auto.
+(* - destruct g. all: rewrite INV; Simpl; auto. *)
- rewrite INV; Simpl; auto.
- contradiction. }
eauto with asmgen.
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml index 59e8c383..cf06ebaf 100644 --- a/mppa_k1c/Asmexpand.ml +++ b/mppa_k1c/Asmexpand.ml @@ -519,7 +519,6 @@ let int_reg_to_dwarf = let open Asmblock in function let preg_to_dwarf = let open Asmblock in function | IR r -> int_reg_to_dwarf r - | FR r -> int_reg_to_dwarf r | RA -> 65 (* FIXME - No idea what is $ra DWARF number in k1-gdb *) | _ -> assert false diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index da3cf75f..bbb608de 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -64,13 +64,11 @@ module Target (*: TARGET*) = let preg oc = let open Asmblock in function | IR r -> ireg oc r - | FR r -> ireg oc r | RA -> output_string oc "$ra" | _ -> assert false let preg_annot = let open Asmblock in function | IR r -> int_reg_name r - | FR r -> int_reg_name r | RA -> "$ra" | _ -> assert false |