diff options
Diffstat (limited to 'backend/Op.v')
-rw-r--r-- | backend/Op.v | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/backend/Op.v b/backend/Op.v index 707bcb0a..5665d725 100644 --- a/backend/Op.v +++ b/backend/Op.v @@ -175,10 +175,10 @@ Definition eval_operation | Some b => Some (Vptr b ofs) end | Oaddrstack ofs, nil => offset_sp sp ofs - | Ocast8signed, v1 :: nil => Some (Val.cast8signed v1) - | Ocast8unsigned, v1 :: nil => Some (Val.cast8unsigned v1) - | Ocast16signed, v1 :: nil => Some (Val.cast16signed v1) - | Ocast16unsigned, v1 :: nil => Some (Val.cast16unsigned v1) + | Ocast8signed, v1 :: nil => Some (Val.sign_ext 8 v1) + | Ocast8unsigned, v1 :: nil => Some (Val.zero_ext 8 v1) + | Ocast16signed, v1 :: nil => Some (Val.sign_ext 16 v1) + | Ocast16unsigned, v1 :: nil => Some (Val.zero_ext 16 v1) | Oadd, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.add n1 n2)) | Oadd, Vint n1 :: Vptr b2 n2 :: nil => Some (Vptr b2 (Int.add n2 n1)) | Oadd, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.add n1 n2)) @@ -632,10 +632,10 @@ Definition eval_operation_total (sp: val) (op: operation) (vl: list val) : val : | Ofloatconst n, nil => Vfloat n | Oaddrsymbol s ofs, nil => find_symbol_offset s ofs | Oaddrstack ofs, nil => Val.add sp (Vint ofs) - | Ocast8signed, v1::nil => Val.cast8signed v1 - | Ocast8unsigned, v1::nil => Val.cast8unsigned v1 - | Ocast16signed, v1::nil => Val.cast16signed v1 - | Ocast16unsigned, v1::nil => Val.cast16unsigned v1 + | Ocast8signed, v1::nil => Val.sign_ext 8 v1 + | Ocast8unsigned, v1::nil => Val.zero_ext 8 v1 + | Ocast16signed, v1::nil => Val.sign_ext 16 v1 + | Ocast16unsigned, v1::nil => Val.zero_ext 16 v1 | Oadd, v1::v2::nil => Val.add v1 v2 | Oaddimm n, v1::nil => Val.add v1 (Vint n) | Osub, v1::v2::nil => Val.sub v1 v2 @@ -843,10 +843,10 @@ Proof. exists v2; auto. destruct (Genv.find_symbol genv i); inv H0. TrivialExists. exists v1; auto. - exists (Val.cast8signed v2); split. auto. apply Val.cast8signed_lessdef; auto. - exists (Val.cast8unsigned v2); split. auto. apply Val.cast8unsigned_lessdef; auto. - exists (Val.cast16signed v2); split. auto. apply Val.cast16signed_lessdef; auto. - exists (Val.cast16unsigned v2); split. auto. apply Val.cast16unsigned_lessdef; auto. + exists (Val.sign_ext 8 v2); split. auto. apply Val.sign_ext_lessdef; auto. + exists (Val.zero_ext 8 v2); split. auto. apply Val.zero_ext_lessdef; auto. + exists (Val.sign_ext 16 v2); split. auto. apply Val.sign_ext_lessdef; auto. + exists (Val.zero_ext 16 v2); split. auto. apply Val.zero_ext_lessdef; auto. destruct (eq_block b b0); inv H0. TrivialExists. destruct (Int.eq i0 Int.zero); inv H0; TrivialExists. destruct (Int.eq i0 Int.zero); inv H0; TrivialExists. |