From c420bc8d3b87d71c38209b5ab8bca22875466362 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 25 Sep 2019 21:31:57 +0200 Subject: __builtin_expect defined as its first argument --- backend/Selection.v | 3 ++- backend/Selectionproof.v | 7 +++++++ cfrontend/C2C.ml | 5 +++-- common/Builtins0.v | 8 +++++++- runtime/include/ccomp_k1c_fixes.h | 2 +- 5 files changed, 20 insertions(+), 5 deletions(-) diff --git a/backend/Selection.v b/backend/Selection.v index 4ab3331e..7ba8fe92 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -243,7 +243,8 @@ Definition sel_builtin_res (optid: option ident) : builtin_res ident := Function sel_known_builtin (bf: builtin_function) (args: exprlist) := match bf, args with | BI_platform b, _ => - SelectOp.platform_builtin b args + SelectOp.platform_builtin b args + | BI_standard BI_expect, a1 ::: a2 ::: Enil => Some a1 | BI_standard (BI_select ty), a1 ::: a2 ::: a3 ::: Enil => Some (sel_select ty a1 a2 a3) | BI_standard BI_fabs, a1 ::: Enil => diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 8a827af2..0be96167 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -395,6 +395,13 @@ Proof. inv ARGS; try discriminate. inv H0; try discriminate. inv SEL. simpl in SEM; inv SEM. apply eval_absf; auto. ++ (* expect *) + inv ARGS; try discriminate. + inv H0; try discriminate. + inv H2; try discriminate. + simpl in SEM. inv SEM. inv SEL. + destruct v1; destruct v0. + all: econstructor; split; eauto. - eapply eval_platform_builtin; eauto. Qed. diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index dc25b516..421c4b07 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -157,9 +157,10 @@ let ais_annot_functions = let builtins_generic = { builtin_typedefs = []; builtin_functions = - ais_annot_functions - @ + ais_annot_functions @ [ + "__builtin_expect", + (TInt(ILong, []), [TInt(ILong, []); TInt(ILong, [])], false); (* Integer arithmetic *) "__builtin_bswap64", (TInt(IULongLong, []), [TInt(IULongLong, [])], false); diff --git a/common/Builtins0.v b/common/Builtins0.v index b78006dd..5061bf43 100644 --- a/common/Builtins0.v +++ b/common/Builtins0.v @@ -337,6 +337,7 @@ Inductive standard_builtin : Type := | BI_addl | BI_subl | BI_mull + | BI_expect | BI_i16_bswap | BI_i32_bswap | BI_i64_bswap @@ -373,6 +374,7 @@ Definition standard_builtin_table : list (string * standard_builtin) := :: ("__builtin_bswap", BI_i32_bswap) :: ("__builtin_bswap32", BI_i32_bswap) :: ("__builtin_bswap64", BI_i64_bswap) + :: ("__builtin_expect", BI_expect) :: ("__compcert_i64_umulh", BI_i64_umulh) :: ("__compcert_i64_smulh", BI_i64_smulh) :: ("__compcert_i64_sdiv", BI_i64_sdiv) @@ -402,7 +404,9 @@ Definition standard_builtin_sig (b: standard_builtin) : signature := | BI_i64_sdiv | BI_i64_udiv | BI_i64_smod | BI_i64_umod => mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default | BI_mull => - mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default + mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default + | BI_expect => + mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default | BI_i32_bswap => mksignature (Tint :: nil) (Some Tint) cc_default | BI_i64_bswap => @@ -433,6 +437,8 @@ Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (pro | BI_addl => mkbuiltin_v2t Tlong Val.addl _ _ | BI_subl => mkbuiltin_v2t Tlong Val.subl _ _ | BI_mull => mkbuiltin_v2t Tlong Val.mull' _ _ + | BI_expect => + mkbuiltin_n2t Tlong Tlong Tlong (fun x _ => x) | BI_i16_bswap => mkbuiltin_n1t Tint Tint (fun n => Int.repr (decode_int (List.rev (encode_int 2%nat (Int.unsigned n))))) diff --git a/runtime/include/ccomp_k1c_fixes.h b/runtime/include/ccomp_k1c_fixes.h index 718ac3e5..f3fa11fe 100644 --- a/runtime/include/ccomp_k1c_fixes.h +++ b/runtime/include/ccomp_k1c_fixes.h @@ -25,6 +25,6 @@ extern long long __compcert_afaddd(void *address, unsigned long long incr); extern int __compcert_afaddw(void *address, unsigned int incr); #endif -#define __builtin_expect(x, y) (x) +/* #define __builtin_expect(x, y) (x) */ #define __builtin_ctz(x) __builtin_k1_ctzw(x) #define __builtin_clz(x) __builtin_k1_clzw(x) -- cgit From 249482aed76d209ff203f9afeeb3f10db004e8c0 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 7 Apr 2020 21:34:14 +0200 Subject: start implementing expect as expr --- backend/Cminor.v | 2 ++ backend/Cminortyping.v | 1 + backend/PrintCminor.ml | 2 ++ backend/Selection.v | 3 +- backend/Selectionaux.ml | 1 + backend/Selectionproof.v | 85 +++++++++++++++++++++++----------------------- cfrontend/Cminorgenproof.v | 1 + 7 files changed, 52 insertions(+), 43 deletions(-) diff --git a/backend/Cminor.v b/backend/Cminor.v index 91a4c104..dcebbb86 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -77,6 +77,7 @@ Inductive unary_operation : Type := | Osingleoflongu: unary_operation. (**r unsigned long to float32 *) Inductive binary_operation : Type := + | Oexpect: typ -> binary_operation (**r first value, second is expected*) | Oadd: binary_operation (**r integer addition *) | Osub: binary_operation (**r integer subtraction *) | Omul: binary_operation (**r integer multiplication *) @@ -301,6 +302,7 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val := Definition eval_binop (op: binary_operation) (arg1 arg2: val) (m: mem): option val := match op with + | Oexpect ty => Some (Val.normalize arg1 ty) | Oadd => Some (Val.add arg1 arg2) | Osub => Some (Val.sub arg1 arg2) | Omul => Some (Val.mul arg1 arg2) diff --git a/backend/Cminortyping.v b/backend/Cminortyping.v index 92ec45f2..8945cecf 100644 --- a/backend/Cminortyping.v +++ b/backend/Cminortyping.v @@ -64,6 +64,7 @@ Definition type_binop (op: binary_operation) : typ * typ * typ := | Ocmpf _ => (Tfloat, Tfloat, Tint) | Ocmpfs _ => (Tsingle, Tsingle, Tint) | Ocmpl _ | Ocmplu _ => (Tlong, Tlong, Tint) + | Oexpect ty => (ty, ty, ty) end. Module RTLtypes <: TYPE_ALGEBRA. diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index c9a6d399..051225a4 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -34,6 +34,7 @@ let precedence = function | Ebinop((Oadd|Osub|Oaddf|Osubf|Oaddfs|Osubfs|Oaddl|Osubl), _, _) -> (12, LtoR) | Ebinop((Oshl|Oshr|Oshru|Oshll|Oshrl|Oshrlu), _, _) -> (11, LtoR) | Ebinop((Ocmp _|Ocmpu _|Ocmpf _|Ocmpfs _|Ocmpl _|Ocmplu _), _, _) -> (10, LtoR) + | Ebinop((Oexpect _), _, _) -> (9, LtoR) | Ebinop((Oand|Oandl), _, _) -> (8, LtoR) | Ebinop((Oxor|Oxorl), _, _) -> (7, LtoR) | Ebinop((Oor|Oorl), _, _) -> (6, LtoR) @@ -89,6 +90,7 @@ let comparison_name = function | Cge -> ">=" let name_of_binop = function + | Oexpect _ -> "expect" | Oadd -> "+" | Osub -> "-" | Omul -> "*" diff --git a/backend/Selection.v b/backend/Selection.v index 7ba8fe92..fcb14127 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -120,6 +120,7 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr := Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr := match op with + | Cminor.Oexpect ty => arg1 | Cminor.Oadd => add arg1 arg2 | Cminor.Osub => sub arg1 arg2 | Cminor.Omul => mul arg1 arg2 @@ -244,7 +245,7 @@ Function sel_known_builtin (bf: builtin_function) (args: exprlist) := match bf, args with | BI_platform b, _ => SelectOp.platform_builtin b args - | BI_standard BI_expect, a1 ::: a2 ::: Enil => Some a1 +(* | BI_standard BI_expect, a1 ::: a2 ::: Enil => Some a1 *) | BI_standard (BI_select ty), a1 ::: a2 ::: a3 ::: Enil => Some (sel_select ty a1 a2 a3) | BI_standard BI_fabs, a1 ::: Enil => diff --git a/backend/Selectionaux.ml b/backend/Selectionaux.ml index 26a79fd7..5a8bde8c 100644 --- a/backend/Selectionaux.ml +++ b/backend/Selectionaux.ml @@ -39,6 +39,7 @@ let cost_unop = function | Osingleoflong | Osingleoflongu -> assert false let cost_binop = function + | Oexpect _ -> 0 | Oadd | Osub -> 1 | Omul -> 2 | Odiv | Odivu | Omod | Omodu -> assert false diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 9e0f22cc..53600c7a 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -310,46 +310,47 @@ Lemma eval_sel_binop: exists v', eval_expr tge sp e m le (sel_binop op a1 a2) v' /\ Val.lessdef v v'. Proof. destruct op; simpl; intros; FuncInv; try subst v. - apply eval_add; auto. - apply eval_sub; auto. - apply eval_mul; auto. - eapply eval_divs; eauto. - eapply eval_divu; eauto. - eapply eval_mods; eauto. - eapply eval_modu; eauto. - apply eval_and; auto. - apply eval_or; auto. - apply eval_xor; auto. - apply eval_shl; auto. - apply eval_shr; auto. - apply eval_shru; auto. - apply eval_addf; auto. - apply eval_subf; auto. - apply eval_mulf; auto. - apply eval_divf; auto. - apply eval_addfs; auto. - apply eval_subfs; auto. - apply eval_mulfs; auto. - apply eval_divfs; auto. - eapply eval_addl; eauto. - eapply eval_subl; eauto. - eapply eval_mull; eauto. - eapply eval_divls; eauto. - eapply eval_divlu; eauto. - eapply eval_modls; eauto. - eapply eval_modlu; eauto. - eapply eval_andl; eauto. - eapply eval_orl; eauto. - eapply eval_xorl; eauto. - eapply eval_shll; eauto. - eapply eval_shrl; eauto. - eapply eval_shrlu; eauto. - apply eval_comp; auto. - apply eval_compu; auto. - apply eval_compf; auto. - apply eval_compfs; auto. - exists v; split; auto. eapply eval_cmpl; eauto. - exists v; split; auto. eapply eval_cmplu; eauto. + - exists v1; split; trivial. apply Val.lessdef_normalize. + - apply eval_add; auto. + - apply eval_sub; auto. + - apply eval_mul; auto. + - eapply eval_divs; eauto. + - eapply eval_divu; eauto. + - eapply eval_mods; eauto. + - eapply eval_modu; eauto. + - apply eval_and; auto. + - apply eval_or; auto. + - apply eval_xor; auto. + - apply eval_shl; auto. + - apply eval_shr; auto. + - apply eval_shru; auto. + - apply eval_addf; auto. + - apply eval_subf; auto. + - apply eval_mulf; auto. + - apply eval_divf; auto. + - apply eval_addfs; auto. + - apply eval_subfs; auto. + - apply eval_mulfs; auto. + - apply eval_divfs; auto. + - eapply eval_addl; eauto. + - eapply eval_subl; eauto. + - eapply eval_mull; eauto. + - eapply eval_divls; eauto. + - eapply eval_divlu; eauto. + - eapply eval_modls; eauto. + - eapply eval_modlu; eauto. + - eapply eval_andl; eauto. + - eapply eval_orl; eauto. + - eapply eval_xorl; eauto. + - eapply eval_shll; eauto. + - eapply eval_shrl; eauto. + - eapply eval_shrlu; eauto. + - apply eval_comp; auto. + - apply eval_compu; auto. + - apply eval_compf; auto. + - apply eval_compfs; auto. + - exists v; split; auto. eapply eval_cmpl; eauto. + - exists v; split; auto. eapply eval_cmplu; eauto. Qed. Lemma eval_sel_select: @@ -395,13 +396,13 @@ Proof. inv ARGS; try discriminate. inv H0; try discriminate. inv SEL. simpl in SEM; inv SEM. apply eval_absf; auto. -+ (* expect *) + (* + (* expect *) inv ARGS; try discriminate. inv H0; try discriminate. inv H2; try discriminate. simpl in SEM. inv SEM. inv SEL. destruct v1; destruct v0. - all: econstructor; split; eauto. + all: econstructor; split; eauto. *) - eapply eval_platform_builtin; eauto. Qed. diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 5acb996d..744df818 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -1335,6 +1335,7 @@ Lemma eval_binop_compat: /\ Val.inject f v tv. Proof. destruct op; simpl; intros; inv H. +- TrivialExists. apply Val.normalize_inject; auto. - TrivialExists. apply Val.add_inject; auto. - TrivialExists. apply Val.sub_inject; auto. - TrivialExists. inv H0; inv H1; constructor. -- cgit From 06559e65f15b379949e14bb6ed1446b6fa10e9d7 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 7 Apr 2020 22:01:51 +0200 Subject: Oexpect in frontend --- cfrontend/Cop.v | 13 +++++++++++++ cfrontend/Cshmgen.v | 6 ++++++ cfrontend/Cshmgenproof.v | 38 ++++++++++++++++++++++---------------- cfrontend/Ctyping.v | 3 +++ cfrontend/PrintClight.ml | 1 + cfrontend/PrintCsyntax.ml | 2 ++ 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) -- cgit From 3b15828ca868365b285ba611ba72177e90d0061b Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 7 Apr 2020 22:50:20 +0200 Subject: expect operation --- cfrontend/C2C.ml | 8 +++++++ cfrontend/SimplExprspec.v | 54 +++++++++++++++++++++++------------------------ common/Builtins0.v | 12 +++++------ 3 files changed, 41 insertions(+), 33 deletions(-) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 9f2c4604..902a5c5d 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -900,6 +900,14 @@ let rec convertExpr env e = | C.ECompound(ty1, ie) -> unsupported "compound literals"; ezero + | C.ECall({edesc = C.EVar {name = "__builtin_expect"}}, args) -> + (match args with + | [e1; e2] -> + ewrap (Ctyping.ebinop Cop.Oexpect (convertExpr env e1) (convertExpr env e2)) + | _ -> + error "__builtin_expect wants two arguments"; + ezero) + | C.ECall({edesc = C.EVar {name = "__builtin_debug"}}, args) when List.length args < 2 -> error "too few arguments to function call, expected at least 2, have 0"; ezero diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index e7d57a1c..95e3957c 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -770,53 +770,53 @@ Proof. (* val *) simpl in H. destruct v; monadInv H; exists (@nil ident); split; auto with gensym. Opaque makeif. - intros. destruct dst; simpl in *; inv H2. +- intros. destruct dst; simpl in *; inv H2. constructor. auto. intros; constructor. constructor. constructor. auto. intros; constructor. - intros. destruct dst; simpl in *; inv H2. +- intros. destruct dst; simpl in *; inv H2. constructor. auto. intros; constructor. constructor. constructor. auto. intros; constructor. - intros. destruct dst; simpl in *; inv H2. +- intros. destruct dst; simpl in *; inv H2. constructor. auto. intros; constructor. constructor. constructor. auto. intros; constructor. - intros. destruct dst; simpl in *; inv H2. +- intros. destruct dst; simpl in *; inv H2. constructor. auto. intros; constructor. constructor. constructor. auto. intros; constructor. (* var *) - monadInv H; econstructor; split; auto with gensym. UseFinish. constructor. +- monadInv H; econstructor; split; auto with gensym. UseFinish. constructor. (* field *) - monadInv H0. exploit H; eauto. auto. intros [tmp [A B]]. UseFinish. +- monadInv H0. exploit H; eauto. auto. intros [tmp [A B]]. UseFinish. econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto. (* valof *) - monadInv H0. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H0. exploit H; eauto. intros [tmp1 [A B]]. exploit transl_valof_meets_spec; eauto. intros [tmp2 [Csyntax D]]. UseFinish. exists (tmp1 ++ tmp2); split. intros; apply tr_expr_add_dest. econstructor; eauto with gensym. eauto with gensym. (* deref *) - monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. +- monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto. (* addrof *) - monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. +- monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. econstructor; split; eauto. intros; apply tr_expr_add_dest. econstructor; eauto. (* unop *) - monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. +- monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto. (* binop *) - monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. exploit H0; eauto. intros [tmp2 [Csyntax D]]. UseFinish. exists (tmp1 ++ tmp2); split. intros; apply tr_expr_add_dest. econstructor; eauto with gensym. eauto with gensym. (* cast *) - monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. +- monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish. econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto. (* seqand *) - monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. destruct dst; monadInv EQ0. (* for value *) exploit H0; eauto with gensym. intros [tmp2 [C D]]. @@ -840,7 +840,7 @@ Opaque makeif. apply list_disjoint_cons_r; eauto with gensym. apply contained_app; eauto with gensym. (* seqor *) - monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. destruct dst; monadInv EQ0. (* for value *) exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. @@ -864,7 +864,7 @@ Opaque makeif. apply list_disjoint_cons_r; eauto with gensym. apply contained_app; eauto with gensym. (* condition *) - monadInv H2. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H2. exploit H; eauto. intros [tmp1 [A B]]. destruct dst; monadInv EQ0. (* for value *) exploit H0; eauto with gensym. intros [tmp2 [C D]]. @@ -896,13 +896,13 @@ Opaque makeif. apply contained_app; eauto with gensym. apply contained_app; eauto with gensym. (* sizeof *) - monadInv H. UseFinish. +- monadInv H. UseFinish. exists (@nil ident); split; auto with gensym. constructor. (* alignof *) - monadInv H. UseFinish. +- monadInv H. UseFinish. exists (@nil ident); split; auto with gensym. constructor. (* assign *) - monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. exploit H0; eauto. intros [tmp2 [Csyntax D]]. destruct dst; monadInv EQ2; simpl add_dest in *. (* for value *) @@ -921,7 +921,7 @@ Opaque makeif. apply contained_cons. eauto with gensym. apply contained_app; eauto with gensym. (* assignop *) - monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. exploit H0; eauto. intros [tmp2 [Csyntax D]]. exploit transl_valof_meets_spec; eauto. intros [tmp3 [E F]]. destruct dst; monadInv EQ3; simpl add_dest in *. @@ -941,7 +941,7 @@ Opaque makeif. apply contained_cons. eauto with gensym. apply contained_app; eauto with gensym. (* postincr *) - monadInv H0. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H0. exploit H; eauto. intros [tmp1 [A B]]. destruct dst; monadInv EQ0; simpl add_dest in *. (* for value *) exists (x0 :: tmp1); split. @@ -958,7 +958,7 @@ Opaque makeif. econstructor; eauto with gensym. apply contained_cons; eauto with gensym. (* comma *) - monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]]. exists (tmp1 ++ tmp2); split. econstructor; eauto with gensym. @@ -968,7 +968,7 @@ Opaque makeif. destruct dst; simpl; auto with gensym. apply contained_app; eauto with gensym. (* call *) - monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. exploit H0; eauto. intros [tmp2 [Csyntax D]]. destruct dst; monadInv EQ2; simpl add_dest in *. (* for value *) @@ -986,7 +986,7 @@ Opaque makeif. apply contained_cons. eauto with gensym. apply contained_app; eauto with gensym. (* builtin *) - monadInv H0. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H0. exploit H; eauto. intros [tmp1 [A B]]. destruct dst; monadInv EQ0; simpl add_dest in *. (* for value *) exists (x0 :: tmp1); split. @@ -1001,13 +1001,13 @@ Opaque makeif. repeat rewrite app_ass. econstructor; eauto with gensym. congruence. apply contained_cons; eauto with gensym. (* loc *) - monadInv H. +- monadInv H. (* paren *) - monadInv H0. +- monadInv H0. (* nil *) - monadInv H; exists (@nil ident); split; auto with gensym. constructor. +- monadInv H; exists (@nil ident); split; auto with gensym. constructor. (* cons *) - monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. +- monadInv H1. exploit H; eauto. intros [tmp1 [A B]]. exploit H0; eauto. intros [tmp2 [Csyntax D]]. exists (tmp1 ++ tmp2); split. econstructor; eauto with gensym. diff --git a/common/Builtins0.v b/common/Builtins0.v index a3215545..f72febf8 100644 --- a/common/Builtins0.v +++ b/common/Builtins0.v @@ -337,7 +337,7 @@ Inductive standard_builtin : Type := | BI_addl | BI_subl | BI_mull - | BI_expect +(* | BI_expect *) | BI_i16_bswap | BI_i32_bswap | BI_i64_bswap @@ -370,7 +370,7 @@ Definition standard_builtin_table : list (string * standard_builtin) := :: ("__builtin_addl", BI_addl) :: ("__builtin_subl", BI_subl) :: ("__builtin_mull", BI_mull) - :: ("__builtin_expect", BI_expect) +(* :: ("__builtin_expect", BI_expect) *) :: ("__builtin_bswap16", BI_i16_bswap) :: ("__builtin_bswap", BI_i32_bswap) :: ("__builtin_bswap32", BI_i32_bswap) @@ -405,8 +405,8 @@ Definition standard_builtin_sig (b: standard_builtin) : signature := mksignature (Tlong :: Tlong :: nil) Tlong cc_default | BI_mull => mksignature (Tint :: Tint :: nil) Tlong cc_default - | BI_expect => - mksignature (Tlong :: Tlong :: nil) Tlong cc_default +(* | BI_expect => + mksignature (Tlong :: Tlong :: nil) Tlong cc_default *) | BI_i32_bswap => mksignature (Tint :: nil) Tint cc_default | BI_i64_bswap => @@ -437,8 +437,8 @@ Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (sig | BI_addl => mkbuiltin_v2t Tlong Val.addl _ _ | BI_subl => mkbuiltin_v2t Tlong Val.subl _ _ | BI_mull => mkbuiltin_v2t Tlong Val.mull' _ _ - | BI_expect => - mkbuiltin_n2t Tlong Tlong Tlong (fun x _ => x) +(* | BI_expect => + mkbuiltin_n2t Tlong Tlong Tlong (fun x _ => x) *) | BI_i16_bswap => mkbuiltin_n1t Tint Tint (fun n => Int.repr (decode_int (List.rev (encode_int 2%nat (Int.unsigned n))))) -- cgit From 952a5faf13280e9bed6fe10670561d7e4fe5bc19 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 7 Apr 2020 23:33:53 +0200 Subject: __builtin_expect seems to work --- backend/CminorSel.v | 8 ++++---- backend/RTLgen.v | 4 ++-- backend/RTLgenaux.ml | 2 +- backend/RTLgenproof.v | 4 ++-- backend/RTLgenspec.v | 4 ++-- backend/Selection.v | 41 ++++++++++++++++++++++++++++++----------- backend/Selectionproof.v | 6 +++--- backend/SplitLong.vp | 5 +++-- 8 files changed, 47 insertions(+), 27 deletions(-) diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 96cb8ae6..26f47e23 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -50,7 +50,7 @@ with exprlist : Type := | Econs: expr -> exprlist -> exprlist with condexpr : Type := - | CEcond : condition -> exprlist -> condexpr + | CEcond : condition -> option bool -> exprlist -> condexpr | CEcondition : condexpr -> condexpr -> condexpr -> condexpr | CElet: expr -> condexpr -> condexpr. @@ -207,10 +207,10 @@ with eval_exprlist: letenv -> exprlist -> list val -> Prop := eval_exprlist le (Econs a1 al) (v1 :: vl) with eval_condexpr: letenv -> condexpr -> bool -> Prop := - | eval_CEcond: forall le cond al vl vb, + | eval_CEcond: forall le cond expected al vl vb, eval_exprlist le al vl -> eval_condition cond vl m = Some vb -> - eval_condexpr le (CEcond cond al) vb + eval_condexpr le (CEcond cond expected al) vb | eval_CEcondition: forall le a b c va v, eval_condexpr le a va -> eval_condexpr le (if va then b else c) v -> @@ -495,7 +495,7 @@ with lift_exprlist (p: nat) (a: exprlist) {struct a}: exprlist := with lift_condexpr (p: nat) (a: condexpr) {struct a}: condexpr := match a with - | CEcond c al => CEcond c (lift_exprlist p al) + | CEcond c expected al => CEcond c expected (lift_exprlist p al) | CEcondition a b c => CEcondition (lift_condexpr p a) (lift_condexpr p b) (lift_condexpr p c) | CElet a b => CElet (lift_expr p a) (lift_condexpr (S p) b) end. diff --git a/backend/RTLgen.v b/backend/RTLgen.v index ac98f3a1..243d7b7c 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -477,9 +477,9 @@ with transl_exprlist (map: mapping) (al: exprlist) (rl: list reg) (nd: node) with transl_condexpr (map: mapping) (a: condexpr) (ntrue nfalse: node) {struct a} : mon node := match a with - | CEcond c al => + | CEcond c expected al => do rl <- alloc_regs map al; - do nt <- add_instr (Icond c rl ntrue nfalse None); + do nt <- add_instr (Icond c rl ntrue nfalse expected); transl_exprlist map al rl nt | CEcondition a b c => do nc <- transl_condexpr map c ntrue nfalse; diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml index e39d3b56..26688e23 100644 --- a/backend/RTLgenaux.ml +++ b/backend/RTLgenaux.ml @@ -41,7 +41,7 @@ and size_exprs = function | Econs(e1, el) -> size_expr e1 + size_exprs el and size_condexpr = function - | CEcond(c, args) -> size_exprs args + | CEcond(c, expected, args) -> size_exprs args | CEcondition(c1, c2, c3) -> 1 + size_condexpr c1 + size_condexpr c2 + size_condexpr c3 | CElet(a, c) -> diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index b94ec22f..e62aff22 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -799,11 +799,11 @@ Proof. Qed. Lemma transl_condexpr_CEcond_correct: - forall le cond al vl vb, + forall le cond expected al vl vb, eval_exprlist ge sp e m le al vl -> transl_exprlist_prop le al vl -> eval_condition cond vl m = Some vb -> - transl_condexpr_prop le (CEcond cond al) vb. + transl_condexpr_prop le (CEcond cond expected al) vb. Proof. intros; red; intros. inv TE. exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [RES1 [OTHER1 EXT1]]]]]]. diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 30ad7d82..36b8409d 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -744,10 +744,10 @@ Inductive tr_expr (c: code): with tr_condition (c: code): mapping -> list reg -> condexpr -> node -> node -> node -> Prop := - | tr_CEcond: forall map pr cond bl ns ntrue nfalse n1 rl i, + | tr_CEcond: forall map pr cond expected bl ns ntrue nfalse n1 rl i, tr_exprlist c map pr bl ns n1 rl -> c!n1 = Some (Icond cond rl ntrue nfalse i) -> - tr_condition c map pr (CEcond cond bl) ns ntrue nfalse + tr_condition c map pr (CEcond cond expected bl) ns ntrue nfalse | tr_CEcondition: forall map pr a1 a2 a3 ns ntrue nfalse n2 n3, tr_condition c map pr a1 ns n2 n3 -> tr_condition c map pr a2 n2 ntrue nfalse -> diff --git a/backend/Selection.v b/backend/Selection.v index fcb14127..342bd8ca 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -35,12 +35,13 @@ Local Open Scope error_monad_scope. (** Conversion of conditions *) -Function condexpr_of_expr (e: expr) : condexpr := +Function condexpr_of_expr (e: expr) (expected : option bool) : condexpr := match e with - | Eop (Ocmp c) el => CEcond c el - | Econdition a b c => CEcondition a (condexpr_of_expr b) (condexpr_of_expr c) - | Elet a b => CElet a (condexpr_of_expr b) - | _ => CEcond (Ccompuimm Cne Int.zero) (e ::: Enil) + | Eop (Ocmp c) el => CEcond c expected el + | Econdition a b c => CEcondition a (condexpr_of_expr b expected) + (condexpr_of_expr c expected) + | Elet a b => CElet a (condexpr_of_expr b expected) + | _ => CEcond (Ccompuimm Cne Int.zero) expected (e ::: Enil) end. Function condition_of_expr (e: expr) : condition * exprlist := @@ -167,7 +168,7 @@ Definition sel_select (ty: typ) (cnd ifso ifnot: expr) : expr := let (cond, args) := condition_of_expr cnd in match SelectOp.select ty cond args ifso ifnot with | Some a => a - | None => Econdition (condexpr_of_expr cnd) ifso ifnot + | None => Econdition (condexpr_of_expr cnd None) ifso ifnot end. (** Conversion from Cminor expression to Cminorsel expressions *) @@ -293,16 +294,16 @@ Fixpoint sel_switch (arg: nat) (t: comptree): exitexpr := | CTaction act => XEexit act | CTifeq key act t' => - XEcondition (condexpr_of_expr (make_cmp_eq (Eletvar arg) key)) + XEcondition (condexpr_of_expr (make_cmp_eq (Eletvar arg) key) None) (XEexit act) (sel_switch arg t') | CTiflt key t1 t2 => - XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar arg) key)) + XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar arg) key) None) (sel_switch arg t1) (sel_switch arg t2) | CTjumptable ofs sz tbl t' => XElet (make_sub (Eletvar arg) ofs) - (XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar O) sz)) + (XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar O) sz) None) (XEjumptable (make_to_int (Eletvar O)) tbl) (sel_switch (S arg) t')) end. @@ -377,6 +378,22 @@ Definition if_conversion | _, _ => None end. +Definition extract_expect1 (e : Cminor.expr) : option bool := + match e with + | Cminor.Ebinop (Cminor.Oexpect ty) e1 (Cminor.Econst (Cminor.Ointconst c)) => + Some (if Int.eq_dec c Int.zero then false else true) + | Cminor.Ebinop (Cminor.Oexpect ty) e1 (Cminor.Econst (Cminor.Olongconst c)) => + Some (if Int64.eq_dec c Int64.zero then false else true) + | _ => None + end. + +Definition extract_expect (e : Cminor.expr) : option bool := + match e with + | Cminor.Ebinop (Cminor.Ocmpu Cne) e1 (Cminor.Econst (Cminor.Ointconst c)) => + if Int.eq_dec c Int.zero then extract_expect1 e1 else None + | _ => extract_expect1 e + end. + (** Conversion from Cminor statements to Cminorsel statements. *) Fixpoint sel_stmt (ki: known_idents) (env: typenv) (s: Cminor.stmt) : res stmt := @@ -404,8 +421,10 @@ Fixpoint sel_stmt (ki: known_idents) (env: typenv) (s: Cminor.stmt) : res stmt : match if_conversion ki env e ifso ifnot with | Some s => OK s | None => - do ifso' <- sel_stmt ki env ifso; do ifnot' <- sel_stmt ki env ifnot; - OK (Sifthenelse (condexpr_of_expr (sel_expr e)) ifso' ifnot') + do ifso' <- sel_stmt ki env ifso; + do ifnot' <- sel_stmt ki env ifnot; + OK (Sifthenelse (condexpr_of_expr (sel_expr e) + (extract_expect e)) ifso' ifnot') end | Cminor.Sloop body => do body' <- sel_stmt ki env body; OK (Sloop body') diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 53600c7a..955c45a4 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -196,12 +196,12 @@ Variable e: env. Variable m: mem. Lemma eval_condexpr_of_expr: - forall a le v b, + forall expected a le v b, eval_expr tge sp e m le a v -> Val.bool_of_val v b -> - eval_condexpr tge sp e m le (condexpr_of_expr a) b. + eval_condexpr tge sp e m le (condexpr_of_expr a expected) b. Proof. - intros until a. functional induction (condexpr_of_expr a); intros. + intros until a. functional induction (condexpr_of_expr a expected); intros. (* compare *) inv H. econstructor; eauto. simpl in H6. inv H6. apply Val.bool_of_val_of_optbool. auto. diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp index dfe42df0..0f240602 100644 --- a/backend/SplitLong.vp +++ b/backend/SplitLong.vp @@ -10,6 +10,7 @@ (* *) (* *********************************************************************) +(* FIXME: expected branching information not propagated *) (** Instruction selection for 64-bit integer operations *) Require String. @@ -256,7 +257,7 @@ Definition cmpl_ne_zero (e: expr) := Definition cmplu_gen (ch cl: comparison) (e1 e2: expr) := splitlong2 e1 e2 (fun h1 l1 h2 l2 => - Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil)) + Econdition (CEcond (Ccomp Ceq) None (h1:::h2:::Enil)) (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil)) (Eop (Ocmp (Ccompu ch)) (h1:::h2:::Enil))). @@ -278,7 +279,7 @@ Definition cmplu (c: comparison) (e1 e2: expr) := Definition cmpl_gen (ch cl: comparison) (e1 e2: expr) := splitlong2 e1 e2 (fun h1 l1 h2 l2 => - Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil)) + Econdition (CEcond (Ccomp Ceq) None (h1:::h2:::Enil)) (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil)) (Eop (Ocmp (Ccomp ch)) (h1:::h2:::Enil))). -- cgit From 50527aedadd5d3c77b15ddbc3a08f189d01d53c1 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 07:01:58 +0200 Subject: bumped for Coq 8.11.1 --- common/Builtins0.v | 6 ------ configure | 2 +- 2 files changed, 1 insertion(+), 7 deletions(-) diff --git a/common/Builtins0.v b/common/Builtins0.v index f72febf8..8da98314 100644 --- a/common/Builtins0.v +++ b/common/Builtins0.v @@ -337,7 +337,6 @@ Inductive standard_builtin : Type := | BI_addl | BI_subl | BI_mull -(* | BI_expect *) | BI_i16_bswap | BI_i32_bswap | BI_i64_bswap @@ -370,7 +369,6 @@ Definition standard_builtin_table : list (string * standard_builtin) := :: ("__builtin_addl", BI_addl) :: ("__builtin_subl", BI_subl) :: ("__builtin_mull", BI_mull) -(* :: ("__builtin_expect", BI_expect) *) :: ("__builtin_bswap16", BI_i16_bswap) :: ("__builtin_bswap", BI_i32_bswap) :: ("__builtin_bswap32", BI_i32_bswap) @@ -405,8 +403,6 @@ Definition standard_builtin_sig (b: standard_builtin) : signature := mksignature (Tlong :: Tlong :: nil) Tlong cc_default | BI_mull => mksignature (Tint :: Tint :: nil) Tlong cc_default -(* | BI_expect => - mksignature (Tlong :: Tlong :: nil) Tlong cc_default *) | BI_i32_bswap => mksignature (Tint :: nil) Tint cc_default | BI_i64_bswap => @@ -437,8 +433,6 @@ Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (sig | BI_addl => mkbuiltin_v2t Tlong Val.addl _ _ | BI_subl => mkbuiltin_v2t Tlong Val.subl _ _ | BI_mull => mkbuiltin_v2t Tlong Val.mull' _ _ -(* | BI_expect => - mkbuiltin_n2t Tlong Tlong Tlong (fun x _ => x) *) | BI_i16_bswap => mkbuiltin_n1t Tint Tint (fun n => Int.repr (decode_int (List.rev (encode_int 2%nat (Int.unsigned n))))) diff --git a/configure b/configure index f790281c..cb2f52ba 100755 --- a/configure +++ b/configure @@ -568,7 +568,7 @@ missingtools=false echo "Testing Coq... " | tr -d '\n' coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p') case "$coq_ver" in - 8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0) + 8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1) echo "version $coq_ver -- good!";; ?*) echo "version $coq_ver -- UNSUPPORTED" -- cgit From 299ee78f478cb7a042c76b3bdd58eac62d41a015 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 07:23:39 +0200 Subject: force using coq 8.10 --- .gitlab-ci.yml | 22 +++++++++++----------- configure | 2 +- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 1f854fc3..069b9012 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -3,7 +3,7 @@ stages: check-admitted: stage: build - image: "coqorg/coq" + image: "coqorg/coq:8.10" before_script: - opam switch 4.07.1+flambda - eval `opam config env` @@ -22,7 +22,7 @@ check-admitted: build_x86_64: stage: build - image: "coqorg/coq" + image: "coqorg/coq:8.10" before_script: - opam switch 4.07.1+flambda - eval `opam config env` @@ -43,7 +43,7 @@ build_x86_64: build_ia32: stage: build - image: "coqorg/coq" + image: "coqorg/coq:8.10" before_script: - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - sudo apt-get -y install gcc-multilib @@ -66,7 +66,7 @@ build_ia32: build_aarch64: stage: build - image: "coqorg/coq" + image: "coqorg/coq:8.10" before_script: - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - sudo apt-get -y install gcc-aarch64-linux-gnu qemu-user @@ -89,7 +89,7 @@ build_aarch64: build_arm: stage: build - image: "coqorg/coq" + image: "coqorg/coq:8.10" before_script: - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - sudo apt-get -y install gcc-arm-linux-gnueabi qemu-user @@ -113,7 +113,7 @@ build_arm: build_armhf: stage: build - image: "coqorg/coq" + image: "coqorg/coq:8.10" before_script: - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - sudo apt-get -y install gcc-arm-linux-gnueabihf qemu-user @@ -136,7 +136,7 @@ build_armhf: build_ppc: stage: build - image: "coqorg/coq" + image: "coqorg/coq:8.10" before_script: - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - sudo apt-get -y install gcc-powerpc-linux-gnu qemu-user @@ -157,7 +157,7 @@ build_ppc: build_ppc64: stage: build - image: "coqorg/coq" + image: "coqorg/coq:8.10" before_script: - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - sudo apt-get -y install gcc-powerpc64-linux-gnu @@ -178,7 +178,7 @@ build_ppc64: build_rv64: stage: build - image: "coqorg/coq" + image: "coqorg/coq:8.10" before_script: - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - sudo apt-get -y install gcc-riscv64-linux-gnu qemu-user @@ -201,7 +201,7 @@ build_rv64: build_rv32: stage: build - image: "coqorg/coq" + image: "coqorg/coq:8.10" before_script: - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - sudo apt-get -y install gcc-riscv64-linux-gnu qemu-user @@ -222,7 +222,7 @@ build_rv32: build_k1c: stage: build - image: "coqorg/coq" + image: "coqorg/coq:8.10" before_script: - opam switch 4.07.1+flambda - eval `opam config env` diff --git a/configure b/configure index cb2f52ba..f790281c 100755 --- a/configure +++ b/configure @@ -568,7 +568,7 @@ missingtools=false echo "Testing Coq... " | tr -d '\n' coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p') case "$coq_ver" in - 8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1) + 8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0) echo "version $coq_ver -- good!";; ?*) echo "version $coq_ver -- UNSUPPORTED" -- cgit From 6e64e970a706c45b5b236a0e4f92698e22682344 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 07:56:33 +0200 Subject: adapt the other targets for the new field in CEcond --- powerpc/SelectOp.vp | 2 +- x86/SelectOp.vp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 50b1bdd6..52f4f855 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -472,7 +472,7 @@ Definition intuoffloat (e: expr) := else Elet e (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil) - (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) + (Econdition (CEcond (Ccompf Clt) None (Eletvar 1 ::: Eletvar 0 ::: Enil)) (intoffloat (Eletvar 1)) (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat. diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp index a23c37d5..2a09207b 100644 --- a/x86/SelectOp.vp +++ b/x86/SelectOp.vp @@ -503,7 +503,7 @@ Definition intuoffloat (e: expr) := if Archi.splitlong then Elet e (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil) - (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) + (Econdition (CEcond (Ccompf Clt) None (Eletvar 1 ::: Eletvar 0 ::: Enil)) (intoffloat (Eletvar 1)) (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat else @@ -516,7 +516,7 @@ Nondetfunction floatofintu (e: expr) := if Archi.splitlong then let f := Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil in Elet e - (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil)) + (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) None (Eletvar O ::: Enil)) (floatofint (Eletvar O)) (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f)) else -- cgit From b58e5d1ae25b3b5b8a7d6124ff171777c298a1d2 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 17:30:48 +0200 Subject: test file for expect --- test/monniaux/expect/expect.c | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 test/monniaux/expect/expect.c diff --git a/test/monniaux/expect/expect.c b/test/monniaux/expect/expect.c new file mode 100644 index 00000000..30e0742a --- /dev/null +++ b/test/monniaux/expect/expect.c @@ -0,0 +1,7 @@ +#ifndef PREDICTED +#define PREDICTED 0 +#endif + +int expect(int x, int *y, int *z) { + return __builtin_expect(x, PREDICTED) ? *y : *z; +} -- cgit