diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-07 22:01:51 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-07 22:01:51 +0200 |
commit | 06559e65f15b379949e14bb6ed1446b6fa10e9d7 (patch) | |
tree | c25e6e3a2d30225c143c79f663aba3e908a53301 /cfrontend/Cop.v | |
parent | 249482aed76d209ff203f9afeeb3f10db004e8c0 (diff) | |
download | compcert-kvx-06559e65f15b379949e14bb6ed1446b6fa10e9d7.tar.gz compcert-kvx-06559e65f15b379949e14bb6ed1446b6fa10e9d7.zip |
Oexpect in frontend
Diffstat (limited to 'cfrontend/Cop.v')
-rw-r--r-- | cfrontend/Cop.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index 143e87a3..47a02851 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -33,6 +33,7 @@ Inductive unary_operation : Type := | Oabsfloat : unary_operation. (**r floating-point absolute value *) Inductive binary_operation : Type := + | Oexpect : binary_operation (**r return first argument *) | Oadd : binary_operation (**r addition (binary [+]) *) | Osub : binary_operation (**r subtraction (binary [-]) *) | Omul : binary_operation (**r multiplication (binary [*]) *) @@ -763,6 +764,14 @@ Definition sem_mul (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val : (fun n1 n2 => Some(Vsingle(Float32.mul n1 n2))) v1 t1 v2 t2 m. +Definition sem_expect (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val := + sem_binarith + (fun sg n1 n2 => Some(Vint n1)) + (fun sg n1 n2 => Some(Vlong n1)) + (fun n1 n2 => Some(Vfloat n1)) + (fun n1 n2 => Some(Vsingle n1)) + v1 t1 v2 t2 m. + Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val := sem_binarith (fun sg n1 n2 => @@ -1050,6 +1059,7 @@ Definition sem_binary_operation (v1: val) (t1: type) (v2: val) (t2:type) (m: mem): option val := match op with + | Oexpect => sem_expect v1 t1 v2 t2 m | Oadd => sem_add cenv v1 t1 v2 t2 m | Osub => sem_sub cenv v1 t1 v2 t2 m | Omul => sem_mul v1 t1 v2 t2 m @@ -1290,6 +1300,9 @@ Lemma sem_binary_operation_inj: exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ Val.inject f v tv. Proof. unfold sem_binary_operation; intros; destruct op. +- (* expect *) + unfold sem_expect in *. + eapply sem_binarith_inject; eauto; intros; exact I. - (* add *) assert (A: forall cenv ty si v1' v2' tv1' tv2', Val.inject f v1' tv1' -> Val.inject f v2' tv2' -> |