aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-07 22:01:51 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-07 22:01:51 +0200
commit06559e65f15b379949e14bb6ed1446b6fa10e9d7 (patch)
treec25e6e3a2d30225c143c79f663aba3e908a53301 /cfrontend
parent249482aed76d209ff203f9afeeb3f10db004e8c0 (diff)
downloadcompcert-kvx-06559e65f15b379949e14bb6ed1446b6fa10e9d7.tar.gz
compcert-kvx-06559e65f15b379949e14bb6ed1446b6fa10e9d7.zip
Oexpect in frontend
Diffstat (limited to 'cfrontend')
-rw-r--r--cfrontend/Cop.v13
-rw-r--r--cfrontend/Cshmgen.v6
-rw-r--r--cfrontend/Cshmgenproof.v38
-rw-r--r--cfrontend/Ctyping.v3
-rw-r--r--cfrontend/PrintClight.ml1
-rw-r--r--cfrontend/PrintCsyntax.ml2
6 files changed, 47 insertions, 16 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' ->
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 5bd12d00..f78b52ae 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -259,6 +259,11 @@ Definition make_add_ptr_long (ce: composite_env) (ty: type) (e1 e2: expr) :=
let n := make_intconst (Int.repr sz) in
OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2))).
+Definition make_expect (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+ make_binarith (Oexpect AST.Tint) (Oexpect AST.Tint)
+ (Oexpect AST.Tfloat) (Oexpect AST.Tsingle)
+ (Oexpect AST.Tlong) (Oexpect AST.Tlong) e1 ty1 e2 ty2.
+
Definition make_add (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
match classify_add ty1 ty2 with
| add_case_pi ty si => make_add_ptr_int ce ty si e1 e2
@@ -421,6 +426,7 @@ Definition transl_binop (ce: composite_env)
(a: expr) (ta: type)
(b: expr) (tb: type) : res expr :=
match op with
+ | Cop.Oexpect => make_expect a ta b tb
| Cop.Oadd => make_add ce a ta b tb
| Cop.Osub => make_sub ce a ta b tb
| Cop.Omul => make_mul a ta b tb
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 1ceb8e4d..c5ba19d5 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -619,6 +619,11 @@ End MAKE_BIN.
Hint Extern 2 (@eq (option val) _ _) => (simpl; reflexivity) : cshm.
+Lemma make_expect_correct: binary_constructor_correct make_expect sem_expect.
+Proof.
+ apply make_binarith_correct; intros; auto.
+Qed.
+
Lemma make_add_correct: binary_constructor_correct (make_add cunit.(prog_comp_env)) (sem_add prog.(prog_comp_env)).
Proof.
assert (A: forall ty si a b c e le m va vb v,
@@ -922,22 +927,23 @@ Lemma transl_binop_correct:
eval_expr ge e le m c v.
Proof.
intros. destruct op; simpl in *.
- eapply make_add_correct; eauto.
- eapply make_sub_correct; eauto.
- eapply make_mul_correct; eauto.
- eapply make_div_correct; eauto.
- eapply make_mod_correct; eauto.
- eapply make_and_correct; eauto.
- eapply make_or_correct; eauto.
- eapply make_xor_correct; eauto.
- eapply make_shl_correct; eauto.
- eapply make_shr_correct; eauto.
- eapply make_cmp_correct; eauto.
- eapply make_cmp_correct; eauto.
- eapply make_cmp_correct; eauto.
- eapply make_cmp_correct; eauto.
- eapply make_cmp_correct; eauto.
- eapply make_cmp_correct; eauto.
+- eapply make_expect_correct; eauto.
+- eapply make_add_correct; eauto.
+- eapply make_sub_correct; eauto.
+- eapply make_mul_correct; eauto.
+- eapply make_div_correct; eauto.
+- eapply make_mod_correct; eauto.
+- eapply make_and_correct; eauto.
+- eapply make_or_correct; eauto.
+- eapply make_xor_correct; eauto.
+- eapply make_shl_correct; eauto.
+- eapply make_shr_correct; eauto.
+- eapply make_cmp_correct; eauto.
+- eapply make_cmp_correct; eauto.
+- eapply make_cmp_correct; eauto.
+- eapply make_cmp_correct; eauto.
+- eapply make_cmp_correct; eauto.
+- eapply make_cmp_correct; eauto.
Qed.
Lemma make_load_correct:
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index 00fcf8ab..bde4001f 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -111,6 +111,7 @@ Definition comparison_type (ty1 ty2: type) (m: string): res type :=
Definition type_binop (op: binary_operation) (ty1 ty2: type) : res type :=
match op with
+ | Oexpect => binarith_type ty1 ty2 "__builtin_expect"
| Oadd =>
match classify_add ty1 ty2 with
| add_case_pi ty _ | add_case_ip _ ty
@@ -1546,6 +1547,8 @@ Lemma pres_sem_binop:
Proof.
intros until m; intros TY SEM WT1 WT2.
destruct op; simpl in TY; simpl in SEM.
+- (* expect *)
+ unfold sem_expect in SEM. eapply pres_sem_binarith; eauto; intros; exact I.
- (* add *)
unfold sem_add, sem_add_ptr_int, sem_add_ptr_long in SEM; DestructCases; auto with ty.
eapply pres_sem_binarith; eauto; intros; exact I.
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index 0e735d2d..0aefde31 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -62,6 +62,7 @@ let precedence = function
| Ebinop(Oand, _, _, _) -> (8, LtoR)
| Ebinop(Oxor, _, _, _) -> (7, LtoR)
| Ebinop(Oor, _, _, _) -> (6, LtoR)
+ | Ebinop(Oexpect, _, _, _) -> (5, LtoR)
(* Expressions *)
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 03dc5837..beca056f 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -30,6 +30,7 @@ let name_unop = function
| Oabsfloat -> "__builtin_fabs"
let name_binop = function
+ | Oexpect -> "expect"
| Oadd -> "+"
| Osub -> "-"
| Omul -> "*"
@@ -158,6 +159,7 @@ let rec precedence = function
| Ebinop(Oand, _, _, _) -> (8, LtoR)
| Ebinop(Oxor, _, _, _) -> (7, LtoR)
| Ebinop(Oor, _, _, _) -> (6, LtoR)
+ | Ebinop(Oexpect, _, _, _) -> (5, LtoR) (* fixme *)
| Eseqand _ -> (5, LtoR)
| Eseqor _ -> (4, LtoR)
| Econdition _ -> (3, RtoL)