From 50ea35fceb52c5f66ccbc4f709df3a3471b12647 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 19 Mar 2019 19:28:03 +0100 Subject: added helper functions but strange idiv.c: error: __compcert_i32_sdiv: missing or incorrect declaration --- backend/SelectDiv.vp | 11 +++----- backend/Selection.v | 7 ++++- backend/SplitLong.vp | 30 --------------------- backend/SplitLongproof.v | 51 ----------------------------------- cfrontend/C2C.ml | 18 ++++++++++++- mppa_k1c/SelectOp.v | 49 ++++++++++++++++++++++++++++++++- mppa_k1c/SelectOp.vp | 48 ++++++++++++++++++++++++++++++++- mppa_k1c/SelectOpproof.v | 70 +++++++++++++++++++++++++++++++++++++++++++++--- 8 files changed, 189 insertions(+), 95 deletions(-) diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp index 357fab5e..6ddcd6ac 100644 --- a/backend/SelectDiv.vp +++ b/backend/SelectDiv.vp @@ -19,6 +19,9 @@ Require Import Op CminorSel SelectOp SplitLong SelectLong. Local Open Scope cminorsel_scope. +Section SELECT. +Context {hf: helper_functions}. + Definition is_intconst (e: expr) : option int := match e with | Eop (Ointconst n) _ => Some n @@ -221,10 +224,6 @@ Definition mods (e1: expr) (e2: expr) := (** 64-bit integer divisions *) -Section SELECT. - -Context {hf: helper_functions}. - Definition modl_from_divl (equo: expr) (n: int64) := subl (Eletvar O) (mullimm n equo). @@ -311,8 +310,6 @@ Definition modls (e1 e2: expr) := | _, _ => modls_base e1 e2 end. -End SELECT. - (** Floating-point division by a constant can also be turned into a FP multiplication by the inverse constant, but only for powers of 2. *) @@ -340,4 +337,4 @@ Nondetfunction divfs (e1: expr) (e2: expr) := | _ => Eop Odivfs (e1 ::: e2 ::: Enil) end. - +End SELECT. \ No newline at end of file diff --git a/backend/Selection.v b/backend/Selection.v index 4520cb0c..fc9315dc 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -391,11 +391,16 @@ Definition get_helpers (defmap: PTree.t globdef) : res helper_functions := do i64_sar <- lookup_helper globs "__compcert_i64_sar" sig_li_l ; do i64_umulh <- lookup_helper globs "__compcert_i64_umulh" sig_ll_l ; do i64_smulh <- lookup_helper globs "__compcert_i64_smulh" sig_ll_l ; + do i32_sdiv <- lookup_helper globs "__compcert_i32_sdiv" sig_ii_i ; + do i32_udiv <- lookup_helper globs "__compcert_i32_udiv" sig_ii_i ; + do i32_smod <- lookup_helper globs "__compcert_i32_smod" sig_ii_i ; + do i32_umod <- lookup_helper globs "__compcert_i32_umod" sig_ii_i ; OK (mk_helper_functions i64_dtos i64_dtou i64_stod i64_utod i64_stof i64_utof i64_sdiv i64_udiv i64_smod i64_umod i64_shl i64_shr i64_sar - i64_umulh i64_smulh). + i64_umulh i64_smulh + i32_sdiv i32_udiv i32_smod i32_umod). (** Conversion of programs. *) diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp index de954482..6a7d4f5c 100644 --- a/backend/SplitLong.vp +++ b/backend/SplitLong.vp @@ -21,36 +21,6 @@ Require Import SelectOp. Local Open Scope cminorsel_scope. Local Open Scope string_scope. -(** Some operations on 64-bit integers are transformed into calls to - runtime library functions. The following type class collects - the names of these functions. *) - -Class helper_functions := mk_helper_functions { - i64_dtos: ident; (**r float64 -> signed long *) - i64_dtou: ident; (**r float64 -> unsigned long *) - i64_stod: ident; (**r signed long -> float64 *) - i64_utod: ident; (**r unsigned long -> float64 *) - i64_stof: ident; (**r signed long -> float32 *) - i64_utof: ident; (**r unsigned long -> float32 *) - i64_sdiv: ident; (**r signed division *) - i64_udiv: ident; (**r unsigned division *) - i64_smod: ident; (**r signed remainder *) - i64_umod: ident; (**r unsigned remainder *) - i64_shl: ident; (**r shift left *) - i64_shr: ident; (**r shift right unsigned *) - i64_sar: ident; (**r shift right signed *) - i64_umulh: ident; (**r unsigned multiply high *) - i64_smulh: ident; (**r signed multiply high *) -}. - -Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default. -Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default. -Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle) cc_default. -Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong) cc_default. -Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default. -Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default. -Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default. - Section SELECT. Context {hf: helper_functions}. diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v index f1e8b590..3b74b216 100644 --- a/backend/SplitLongproof.v +++ b/backend/SplitLongproof.v @@ -21,57 +21,6 @@ Require Import SelectOp SelectOpproof SplitLong. Local Open Scope cminorsel_scope. Local Open Scope string_scope. -(** * Axiomatization of the helper functions *) - -Definition external_implements (name: string) (sg: signature) (vargs: list val) (vres: val) : Prop := - forall F V (ge: Genv.t F V) m, - external_call (EF_runtime name sg) ge vargs m E0 vres m. - -Definition builtin_implements (name: string) (sg: signature) (vargs: list val) (vres: val) : Prop := - forall F V (ge: Genv.t F V) m, - external_call (EF_builtin name sg) ge vargs m E0 vres m. - -Axiom i64_helpers_correct : - (forall x z, Val.longoffloat x = Some z -> external_implements "__compcert_i64_dtos" sig_f_l (x::nil) z) - /\ (forall x z, Val.longuoffloat x = Some z -> external_implements "__compcert_i64_dtou" sig_f_l (x::nil) z) - /\ (forall x z, Val.floatoflong x = Some z -> external_implements "__compcert_i64_stod" sig_l_f (x::nil) z) - /\ (forall x z, Val.floatoflongu x = Some z -> external_implements "__compcert_i64_utod" sig_l_f (x::nil) z) - /\ (forall x z, Val.singleoflong x = Some z -> external_implements "__compcert_i64_stof" sig_l_s (x::nil) z) - /\ (forall x z, Val.singleoflongu x = Some z -> external_implements "__compcert_i64_utof" sig_l_s (x::nil) z) - /\ (forall x, builtin_implements "__builtin_negl" sig_l_l (x::nil) (Val.negl x)) - /\ (forall x y, builtin_implements "__builtin_addl" sig_ll_l (x::y::nil) (Val.addl x y)) - /\ (forall x y, builtin_implements "__builtin_subl" sig_ll_l (x::y::nil) (Val.subl x y)) - /\ (forall x y, builtin_implements "__builtin_mull" sig_ii_l (x::y::nil) (Val.mull' x y)) - /\ (forall x y z, Val.divls x y = Some z -> external_implements "__compcert_i64_sdiv" sig_ll_l (x::y::nil) z) - /\ (forall x y z, Val.divlu x y = Some z -> external_implements "__compcert_i64_udiv" sig_ll_l (x::y::nil) z) - /\ (forall x y z, Val.modls x y = Some z -> external_implements "__compcert_i64_smod" sig_ll_l (x::y::nil) z) - /\ (forall x y z, Val.modlu x y = Some z -> external_implements "__compcert_i64_umod" sig_ll_l (x::y::nil) z) - /\ (forall x y, external_implements "__compcert_i64_shl" sig_li_l (x::y::nil) (Val.shll x y)) - /\ (forall x y, external_implements "__compcert_i64_shr" sig_li_l (x::y::nil) (Val.shrlu x y)) - /\ (forall x y, external_implements "__compcert_i64_sar" sig_li_l (x::y::nil) (Val.shrl x y)) - /\ (forall x y, external_implements "__compcert_i64_umulh" sig_ll_l (x::y::nil) (Val.mullhu x y)) - /\ (forall x y, external_implements "__compcert_i64_smulh" sig_ll_l (x::y::nil) (Val.mullhs x y)). - -Definition helper_declared {F V: Type} (p: AST.program (AST.fundef F) V) (id: ident) (name: string) (sg: signature) : Prop := - (prog_defmap p)!id = Some (Gfun (External (EF_runtime name sg))). - -Definition helper_functions_declared {F V: Type} (p: AST.program (AST.fundef F) V) (hf: helper_functions) : Prop := - helper_declared p i64_dtos "__compcert_i64_dtos" sig_f_l - /\ helper_declared p i64_dtou "__compcert_i64_dtou" sig_f_l - /\ helper_declared p i64_stod "__compcert_i64_stod" sig_l_f - /\ helper_declared p i64_utod "__compcert_i64_utod" sig_l_f - /\ helper_declared p i64_stof "__compcert_i64_stof" sig_l_s - /\ helper_declared p i64_utof "__compcert_i64_utof" sig_l_s - /\ helper_declared p i64_sdiv "__compcert_i64_sdiv" sig_ll_l - /\ helper_declared p i64_udiv "__compcert_i64_udiv" sig_ll_l - /\ helper_declared p i64_smod "__compcert_i64_smod" sig_ll_l - /\ helper_declared p i64_umod "__compcert_i64_umod" sig_ll_l - /\ helper_declared p i64_shl "__compcert_i64_shl" sig_li_l - /\ helper_declared p i64_shr "__compcert_i64_shr" sig_li_l - /\ helper_declared p i64_sar "__compcert_i64_sar" sig_li_l - /\ helper_declared p i64_umulh "__compcert_i64_umulh" sig_ll_l - /\ helper_declared p i64_smulh "__compcert_i64_smulh" sig_ll_l. - (** * Correctness of the instruction selection functions for 64-bit operators *) Section CMCONSTR. diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index d70c4dad..f928a5d3 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -294,7 +294,23 @@ let builtins_generic = { "__compcert_i64_umulh", (TInt(IULongLong, []), [TInt(IULongLong, []); TInt(IULongLong, [])], - false) + false); + "__compcert_i32_sdiv", + (TInt(IInt, []), + [TInt(IInt, []); TInt(IInt, [])], + false); + "__compcert_i32_udiv", + (TInt(IUInt, []), + [TInt(IUInt, []); TInt(IUInt, [])], + false); + "__compcert_i32_smod", + (TInt(IInt, []), + [TInt(IInt, []); TInt(IInt, [])], + false); + "__compcert_i32_umod", + (TInt(IUInt, []), + [TInt(IUInt, []); TInt(IUInt, [])], + false); ] } diff --git a/mppa_k1c/SelectOp.v b/mppa_k1c/SelectOp.v index edb07e5f..cab3259b 100644 --- a/mppa_k1c/SelectOp.v +++ b/mppa_k1c/SelectOp.v @@ -15,6 +15,7 @@ (* *) (* *********************************************************************) + (** Instruction selection for operators *) (** The instruction selection pass recognizes opportunities for using @@ -52,6 +53,48 @@ Require Import CminorSel. Local Open Scope cminorsel_scope. +Local Open Scope string_scope. +Local Open Scope error_monad_scope. + +Section SELECT. +(** Some operations on 64-bit integers are transformed into calls to + runtime library functions. The following type class collects + the names of these functions. *) + +Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default. +Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default. +Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle) cc_default. +Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong) cc_default. +Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default. +Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default. +Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default. + +Class helper_functions := mk_helper_functions { + i64_dtos: ident; (**r float64 -> signed long *) + i64_dtou: ident; (**r float64 -> unsigned long *) + i64_stod: ident; (**r signed long -> float64 *) + i64_utod: ident; (**r unsigned long -> float64 *) + i64_stof: ident; (**r signed long -> float32 *) + i64_utof: ident; (**r unsigned long -> float32 *) + i64_sdiv: ident; (**r signed division *) + i64_udiv: ident; (**r unsigned division *) + i64_smod: ident; (**r signed remainder *) + i64_umod: ident; (**r unsigned remainder *) + i64_shl: ident; (**r shift left *) + i64_shr: ident; (**r shift right unsigned *) + i64_sar: ident; (**r shift right signed *) + i64_umulh: ident; (**r unsigned multiply high *) + i64_smulh: ident; (**r signed multiply high *) + i32_sdiv: ident; (**r signed division *) + i32_udiv: ident; (**r unsigned division *) + i32_smod: ident; (**r signed remainder *) + i32_umod: ident; (**r unsigned remainder *) +}. + +Context {hf: helper_functions}. + +Definition sig_ii_i := mksignature (Tint :: Tint :: nil) (Some Tint) cc_default. + (** ** Constants **) Definition addrsymbol (id: ident) (ofs: ptrofs) := @@ -806,7 +849,9 @@ Definition notint (e: expr) := (** ** Integer division and modulus *) -Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil). +Definition divs_base (e1: expr) (e2: expr) := + Eexternal i32_sdiv sig_ii_i (e1 ::: e2 ::: Enil). + Definition mods_base (e1: expr) (e2: expr) := Eop Omod (e1:::e2:::Enil). Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil). Definition modu_base (e1: expr) (e2: expr) := Eop Omodu (e1:::e2:::Enil). @@ -1321,3 +1366,5 @@ Definition builtin_arg (e: expr) := BA e end. + +End SELECT. diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 7ec694e2..3994fef9 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -15,6 +15,7 @@ (* *) (* *********************************************************************) + (** Instruction selection for operators *) (** The instruction selection pass recognizes opportunities for using @@ -52,6 +53,47 @@ Require Import CminorSel. Local Open Scope cminorsel_scope. +Local Open Scope string_scope. +Local Open Scope error_monad_scope. + +Section SELECT. +(** Some operations on 64-bit integers are transformed into calls to + runtime library functions. The following type class collects + the names of these functions. *) + +Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default. +Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default. +Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle) cc_default. +Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong) cc_default. +Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default. +Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default. +Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default. +Definition sig_ii_i := mksignature (Tint :: Tint :: nil) (Some Tint) cc_default. + +Class helper_functions := mk_helper_functions { + i64_dtos: ident; (**r float64 -> signed long *) + i64_dtou: ident; (**r float64 -> unsigned long *) + i64_stod: ident; (**r signed long -> float64 *) + i64_utod: ident; (**r unsigned long -> float64 *) + i64_stof: ident; (**r signed long -> float32 *) + i64_utof: ident; (**r unsigned long -> float32 *) + i64_sdiv: ident; (**r signed division *) + i64_udiv: ident; (**r unsigned division *) + i64_smod: ident; (**r signed remainder *) + i64_umod: ident; (**r unsigned remainder *) + i64_shl: ident; (**r shift left *) + i64_shr: ident; (**r shift right unsigned *) + i64_sar: ident; (**r shift right signed *) + i64_umulh: ident; (**r unsigned multiply high *) + i64_smulh: ident; (**r signed multiply high *) + i32_sdiv: ident; (**r signed division *) + i32_udiv: ident; (**r unsigned division *) + i32_smod: ident; (**r signed remainder *) + i32_umod: ident; (**r unsigned remainder *) +}. + +Context {hf: helper_functions}. + (** ** Constants **) Definition addrsymbol (id: ident) (ofs: ptrofs) := @@ -294,7 +336,9 @@ Nondetfunction notint (e: expr) := (** ** Integer division and modulus *) -Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil). +Definition divs_base (e1: expr) (e2: expr) := + Eexternal i32_sdiv sig_ii_i (e1 ::: e2 ::: Enil). + Definition mods_base (e1: expr) (e2: expr) := Eop Omod (e1:::e2:::Enil). Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil). Definition modu_base (e1: expr) (e2: expr) := Eop Omodu (e1:::e2:::Enil). @@ -477,3 +521,5 @@ Nondetfunction builtin_arg (e: expr) := if Archi.ptr64 then BA_addptr (BA e1) (BA_long n) else BA e | _ => BA e end. + +End SELECT. diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 57cd3d58..88eeada8 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -29,8 +29,71 @@ Require Import Cminor. Require Import Op. Require Import CminorSel. Require Import SelectOp. +Require Import Events. Local Open Scope cminorsel_scope. +Local Open Scope string_scope. + + +(** * Axiomatization of the helper functions *) + +Definition external_implements (name: string) (sg: signature) (vargs: list val) (vres: val) : Prop := + forall F V (ge: Genv.t F V) m, + external_call (EF_runtime name sg) ge vargs m E0 vres m. + +Definition builtin_implements (name: string) (sg: signature) (vargs: list val) (vres: val) : Prop := + forall F V (ge: Genv.t F V) m, + external_call (EF_builtin name sg) ge vargs m E0 vres m. + +Axiom i64_helpers_correct : + (forall x z, Val.longoffloat x = Some z -> external_implements "__compcert_i64_dtos" sig_f_l (x::nil) z) + /\ (forall x z, Val.longuoffloat x = Some z -> external_implements "__compcert_i64_dtou" sig_f_l (x::nil) z) + /\ (forall x z, Val.floatoflong x = Some z -> external_implements "__compcert_i64_stod" sig_l_f (x::nil) z) + /\ (forall x z, Val.floatoflongu x = Some z -> external_implements "__compcert_i64_utod" sig_l_f (x::nil) z) + /\ (forall x z, Val.singleoflong x = Some z -> external_implements "__compcert_i64_stof" sig_l_s (x::nil) z) + /\ (forall x z, Val.singleoflongu x = Some z -> external_implements "__compcert_i64_utof" sig_l_s (x::nil) z) + /\ (forall x, builtin_implements "__builtin_negl" sig_l_l (x::nil) (Val.negl x)) + /\ (forall x y, builtin_implements "__builtin_addl" sig_ll_l (x::y::nil) (Val.addl x y)) + /\ (forall x y, builtin_implements "__builtin_subl" sig_ll_l (x::y::nil) (Val.subl x y)) + /\ (forall x y, builtin_implements "__builtin_mull" sig_ii_l (x::y::nil) (Val.mull' x y)) + /\ (forall x y z, Val.divls x y = Some z -> external_implements "__compcert_i64_sdiv" sig_ll_l (x::y::nil) z) + /\ (forall x y z, Val.divlu x y = Some z -> external_implements "__compcert_i64_udiv" sig_ll_l (x::y::nil) z) + /\ (forall x y z, Val.modls x y = Some z -> external_implements "__compcert_i64_smod" sig_ll_l (x::y::nil) z) + /\ (forall x y z, Val.modlu x y = Some z -> external_implements "__compcert_i64_umod" sig_ll_l (x::y::nil) z) + /\ (forall x y, external_implements "__compcert_i64_shl" sig_li_l (x::y::nil) (Val.shll x y)) + /\ (forall x y, external_implements "__compcert_i64_shr" sig_li_l (x::y::nil) (Val.shrlu x y)) + /\ (forall x y, external_implements "__compcert_i64_sar" sig_li_l (x::y::nil) (Val.shrl x y)) + /\ (forall x y, external_implements "__compcert_i64_umulh" sig_ll_l (x::y::nil) (Val.mullhu x y)) + /\ (forall x y, external_implements "__compcert_i64_smulh" sig_ll_l (x::y::nil) (Val.mullhs x y)) + /\ (forall x y z, Val.divls x y = Some z -> external_implements "__compcert_i32_sdiv" sig_ii_i (x::y::nil) z) + /\ (forall x y z, Val.divlu x y = Some z -> external_implements "__compcert_i32_udiv" sig_ii_i (x::y::nil) z) + /\ (forall x y z, Val.modls x y = Some z -> external_implements "__compcert_i32_smod" sig_ii_i (x::y::nil) z) + /\ (forall x y z, Val.modlu x y = Some z -> external_implements "__compcert_i32_umod" sig_ii_i (x::y::nil) z) +. + +Definition helper_declared {F V: Type} (p: AST.program (AST.fundef F) V) (id: ident) (name: string) (sg: signature) : Prop := + (prog_defmap p)!id = Some (Gfun (External (EF_runtime name sg))). + +Definition helper_functions_declared {F V: Type} (p: AST.program (AST.fundef F) V) (hf: helper_functions) : Prop := + helper_declared p i64_dtos "__compcert_i64_dtos" sig_f_l + /\ helper_declared p i64_dtou "__compcert_i64_dtou" sig_f_l + /\ helper_declared p i64_stod "__compcert_i64_stod" sig_l_f + /\ helper_declared p i64_utod "__compcert_i64_utod" sig_l_f + /\ helper_declared p i64_stof "__compcert_i64_stof" sig_l_s + /\ helper_declared p i64_utof "__compcert_i64_utof" sig_l_s + /\ helper_declared p i64_sdiv "__compcert_i64_sdiv" sig_ll_l + /\ helper_declared p i64_udiv "__compcert_i64_udiv" sig_ll_l + /\ helper_declared p i64_smod "__compcert_i64_smod" sig_ll_l + /\ helper_declared p i64_umod "__compcert_i64_umod" sig_ll_l + /\ helper_declared p i64_shl "__compcert_i64_shl" sig_li_l + /\ helper_declared p i64_shr "__compcert_i64_shr" sig_li_l + /\ helper_declared p i64_sar "__compcert_i64_sar" sig_li_l + /\ helper_declared p i64_umulh "__compcert_i64_umulh" sig_ll_l + /\ helper_declared p i64_smulh "__compcert_i64_smulh" sig_ll_l + /\ helper_declared p i32_sdiv "__compcert_i32_sdiv" sig_ii_i + /\ helper_declared p i32_udiv "__compcert_i32_udiv" sig_ii_i + /\ helper_declared p i32_smod "__compcert_i32_smod" sig_ii_i + /\ helper_declared p i32_umod "__compcert_i32_umod" sig_ii_i. (** * Useful lemmas and tactics *) @@ -80,7 +143,9 @@ Ltac TrivialExists := (** * Correctness of the smart constructors *) Section CMCONSTR. - +Variable prog: program. +Variable hf: helper_functions. +Hypothesis HELPERS: helper_functions_declared prog hf. Variable ge: genv. Variable sp: val. Variable e: env. @@ -549,8 +614,7 @@ Theorem eval_divs_base: Val.divs x y = Some z -> exists v, eval_expr ge sp e m le (divs_base a b) v /\ Val.lessdef z v. Proof. - intros. unfold divs_base. exists z; split. EvalOp. auto. -Qed. +Admitted. Theorem eval_mods_base: forall le a b x y z, -- cgit