diff options
Diffstat (limited to 'arm')
| -rw-r--r-- | arm/Machregs.v | 6 | ||||
| -rw-r--r-- | arm/PrintOp.ml | 1 | ||||
| -rw-r--r-- | arm/TargetPrinter.ml | 2 |
3 files changed, 7 insertions, 2 deletions
diff --git a/arm/Machregs.v b/arm/Machregs.v index b43f9be6..e97df790 100644 --- a/arm/Machregs.v +++ b/arm/Machregs.v @@ -58,7 +58,7 @@ Proof. Qed. Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. - + Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete @@ -161,6 +161,9 @@ Definition destroyed_by_setstack (ty: typ): list mreg := nil. Definition destroyed_at_function_entry: list mreg := R12 :: nil. +Definition destroyed_at_indirect_call: list mreg := + R0 :: R1 :: R2 :: R3 :: nil. + Definition temp_for_parent_frame: mreg := R12. @@ -177,6 +180,7 @@ Global Opaque destroyed_by_op destroyed_by_load destroyed_by_store destroyed_by_cond destroyed_by_jumptable destroyed_by_builtin destroyed_by_setstack destroyed_at_function_entry temp_for_parent_frame + destroyed_at_indirect_call mregs_for_operation mregs_for_builtin. (** Two-address operations. Return [true] if the first argument and diff --git a/arm/PrintOp.ml b/arm/PrintOp.ml index 71e1dfc3..642fff80 100644 --- a/arm/PrintOp.ml +++ b/arm/PrintOp.ml @@ -120,6 +120,7 @@ let print_operation reg pp = function | Ointuoffloat, [r1] -> fprintf pp "intuoffloat(%a)" reg r1 | Ofloatofint, [r1] -> fprintf pp "floatofint(%a)" reg r1 | Ofloatofintu, [r1] -> fprintf pp "floatofintu(%a)" reg r1 + | Ofloatofsingle, [r1] -> fprintf pp "floatofsingle(%a)" reg r1 | Ointofsingle, [r1] -> fprintf pp "intofsingle(%a)" reg r1 | Ointuofsingle, [r1] -> fprintf pp "intuofsingle(%a)" reg r1 | Osingleofint, [r1] -> fprintf pp "singleofint(%a)" reg r1 diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 95cae3f7..6d194369 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -382,7 +382,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = end | (fr, Single, sr) :: act -> let n = fixup_incoming oc act in - if fr = sr then n else begin + if (2*fr) = sr then n else begin fprintf oc " vmov.f32 s%d, s%d\n" (2*fr) sr; 1 + n end |