added helper functions but strange

idiv.c: error: __compcert_i32_sdiv: missing or incorrect declaration

3 files changed, 162 insertions, 5 deletions

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,