diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-04-01 18:16:05 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-04-01 18:23:11 +0200 |
| commit | 0c95673ef97195eae6213db92c2f69ef1d1ff48e (patch) | |
| tree | d586db7c5cc4952e525706e19105256b95bf9a7c /mppa_k1c/Op.v | |
| parent | 1036dcaa7a99870aa1859a9a1c683ad8f9b3b0d8 (diff) | |
| download | compcert-kvx-0c95673ef97195eae6213db92c2f69ef1d1ff48e.tar.gz compcert-kvx-0c95673ef97195eae6213db92c2f69ef1d1ff48e.zip | |
Started to add addressing with register + register, Mach -> Asm not done yet
Diffstat (limited to 'mppa_k1c/Op.v')
| -rw-r--r-- | mppa_k1c/Op.v | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index c4338857..d533a504 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -187,6 +187,7 @@ Inductive operation : Type := addressing. *) Inductive addressing: Type := + | Aindexed2: addressing (**r Address is [r1 + r2] *) | Aindexed: ptrofs -> addressing (**r Address is [r1 + offset] *) | Aglobal: ident -> ptrofs -> addressing (**r Address is global plus offset *) | Ainstack: ptrofs -> addressing. (**r Address is [stack_pointer + offset] *) @@ -385,6 +386,7 @@ Definition eval_addressing (F V: Type) (genv: Genv.t F V) (sp: val) (addr: addressing) (vl: list val) : option val := match addr, vl with + | Aindexed2, v1 :: v2 :: nil => Some (Val.addl v1 v2) | Aindexed n, v1 :: nil => Some (Val.offset_ptr v1 n) | Aglobal s ofs, nil => Some (Genv.symbol_address genv s ofs) | Ainstack n, nil => Some (Val.offset_ptr sp n) @@ -569,6 +571,7 @@ Definition type_of_operation (op: operation) : list typ * typ := Definition type_of_addressing (addr: addressing) : list typ := match addr with + | Aindexed2 => Tptr :: Tptr :: nil | Aindexed _ => Tptr :: nil | Aglobal _ _ => nil | Ainstack _ => nil @@ -914,6 +917,7 @@ Qed. Definition offset_addressing (addr: addressing) (delta: Z) : option addressing := match addr with + | Aindexed2 => None | Aindexed n => Some(Aindexed (Ptrofs.add n (Ptrofs.repr delta))) | Aglobal id n => Some(Aglobal id (Ptrofs.add n (Ptrofs.repr delta))) | Ainstack n => Some(Ainstack (Ptrofs.add n (Ptrofs.repr delta))) @@ -1337,9 +1341,10 @@ Lemma eval_addressing_inj: exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2. Proof. intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists. - apply Val.offset_ptr_inject; auto. - apply H; simpl; auto. - apply Val.offset_ptr_inject; auto. + - apply Val.addl_inject; auto. + - apply Val.offset_ptr_inject; auto. + - apply H; simpl; auto. + - apply Val.offset_ptr_inject; auto. Qed. End EVAL_COMPAT. |