diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-22 12:48:30 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-22 12:48:30 +0100 |
commit | c5836e2d5f6a7183db97905040376f68459ad465 (patch) | |
tree | 40d22c3a7de3de84984d86e2c83c3cdbceda60f2 | |
parent | 0b393f7e37315e055eddc5cfba8333639ca265be (diff) | |
parent | a72d1d49ff2d77d0e384c81a8bf2c69bc926194a (diff) | |
download | compcert-kvx-c5836e2d5f6a7183db97905040376f68459ad465.tar.gz compcert-kvx-c5836e2d5f6a7183db97905040376f68459ad465.zip |
Merge branch 'mppa-mul' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-mul
-rw-r--r-- | Makefile | 2 | ||||
-rw-r--r-- | arm/Machregsaux.ml | 5 | ||||
-rw-r--r-- | arm/Machregsaux.mli | 2 | ||||
-rw-r--r-- | arm/SelectLong.vp | 2 | ||||
-rw-r--r-- | arm/SelectLongproof.v | 1 | ||||
-rw-r--r-- | arm/SelectOp.vp | 8 | ||||
-rw-r--r-- | arm/SelectOpproof.v | 28 | ||||
-rw-r--r-- | backend/IRC.ml | 9 | ||||
-rw-r--r-- | backend/IRC.mli | 1 | ||||
-rw-r--r-- | backend/OpHelpers.v | 42 | ||||
-rw-r--r-- | backend/OpHelpersproof.v | 78 | ||||
-rw-r--r-- | backend/Regalloc.ml | 2 | ||||
-rw-r--r-- | backend/SelectDiv.vp | 2 | ||||
-rw-r--r-- | backend/SelectDivproof.v | 1 | ||||
-rw-r--r-- | backend/Selection.v | 2 | ||||
-rw-r--r-- | backend/Selectionproof.v | 1 | ||||
-rw-r--r-- | backend/SplitLong.vp | 1 | ||||
-rw-r--r-- | backend/SplitLongproof.v | 3 | ||||
-rw-r--r-- | mppa_k1c/Asm.v | 5 | ||||
-rw-r--r-- | mppa_k1c/Asmblock.v | 16 | ||||
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 29 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 12 | ||||
-rw-r--r-- | mppa_k1c/ConstpropOp.v | 613 | ||||
-rw-r--r-- | mppa_k1c/Machregsaux.ml | 5 | ||||
-rw-r--r-- | mppa_k1c/Machregsaux.mli | 2 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 1 | ||||
-rw-r--r-- | mppa_k1c/SelectLong.vp | 1 | ||||
-rw-r--r-- | mppa_k1c/SelectLongproof.v | 1 | ||||
-rw-r--r-- | mppa_k1c/SelectOp.vp | 39 | ||||
-rw-r--r-- | mppa_k1c/SelectOpproof.v | 69 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 4 | ||||
-rw-r--r-- | powerpc/Machregsaux.ml | 5 | ||||
-rw-r--r-- | powerpc/Machregsaux.mli | 2 | ||||
-rw-r--r-- | powerpc/SelectLong.vp | 2 | ||||
-rw-r--r-- | powerpc/SelectLongproof.v | 1 | ||||
-rw-r--r-- | powerpc/SelectOp.vp | 8 | ||||
-rw-r--r-- | powerpc/SelectOpproof.v | 28 | ||||
-rw-r--r-- | riscV/Machregsaux.ml | 5 | ||||
-rw-r--r-- | riscV/Machregsaux.mli | 2 | ||||
-rw-r--r-- | riscV/SelectLong.vp | 2 | ||||
-rw-r--r-- | riscV/SelectLongproof.v | 1 | ||||
-rw-r--r-- | riscV/SelectOp.vp | 7 | ||||
-rw-r--r-- | riscV/SelectOpproof.v | 29 | ||||
-rw-r--r-- | test/monniaux/mbedtls/mbedtls_Kalray.patch | 63 | ||||
-rw-r--r-- | test/mppa/instr/andd.c | 5 | ||||
-rw-r--r-- | test/mppa/instr/div32.c (renamed from test/mppa/instr/addw.c) | 2 | ||||
-rw-r--r-- | test/mppa/instr/divf32.c (renamed from test/mppa/instr/faddw.c) | 2 | ||||
-rw-r--r-- | test/mppa/instr/divf64.c (renamed from test/mppa/instr/faddd.c) | 2 | ||||
-rw-r--r-- | test/mppa/instr/divu32.c (renamed from test/mppa/instr/cast_U32_S64.c) | 2 | ||||
-rw-r--r-- | test/mppa/instr/f32.c | 8 | ||||
-rw-r--r-- | test/mppa/instr/f64.c | 8 | ||||
-rw-r--r-- | test/mppa/instr/i32.c | 87 | ||||
-rw-r--r-- | test/mppa/instr/i64.c | 107 | ||||
-rw-r--r-- | test/mppa/instr/individual/andw.c (renamed from test/mppa/instr/andw.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/branch.c (renamed from test/mppa/instr/branch.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/branchz.c (renamed from test/mppa/instr/branchz.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/branchzu.c (renamed from test/mppa/instr/branchzu.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/call.c (renamed from test/mppa/instr/call.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/cast_S32_S64.c (renamed from test/mppa/instr/cast_S32_S64.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/cast_S64_U32.c (renamed from test/mppa/instr/cast_S64_U32.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/cb.deqz.c (renamed from test/mppa/instr/cb.deqz.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/cb.dgez.c (renamed from test/mppa/instr/cb.dgez.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/cb.dgtz.c (renamed from test/mppa/instr/cb.dgtz.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/cb.dlez.c (renamed from test/mppa/instr/cb.dlez.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/cb.dltz.c (renamed from test/mppa/instr/cb.dltz.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/cb.dnez.c (renamed from test/mppa/instr/cb.dnez.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/cb.wgez.c (renamed from test/mppa/instr/cb.wgez.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/cb.wgtz.c (renamed from test/mppa/instr/cb.wgtz.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/cb.wlez.c (renamed from test/mppa/instr/cb.wlez.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/cb.wltz.c (renamed from test/mppa/instr/cb.wltz.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/compd.eq.c (renamed from test/mppa/instr/compd.eq.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/compd.geu.c (renamed from test/mppa/instr/compd.geu.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/compd.gt.c (renamed from test/mppa/instr/compd.gt.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/compd.le.c (renamed from test/mppa/instr/compd.le.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/compd.leu.c (renamed from test/mppa/instr/compd.leu.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/compd.lt.c (renamed from test/mppa/instr/compd.lt.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/compd.ltu.c (renamed from test/mppa/instr/compd.ltu.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/compd.ne.c (renamed from test/mppa/instr/compd.ne.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/compw.eq.c (renamed from test/mppa/instr/compw.eq.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/compw.geu.c (renamed from test/mppa/instr/compw.geu.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/compw.gt.c (renamed from test/mppa/instr/compw.gt.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/compw.gtu.c (renamed from test/mppa/instr/compw.gtu.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/compw.le.c (renamed from test/mppa/instr/compw.le.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/compw.leu.c (renamed from test/mppa/instr/compw.leu.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/compw.lt.c (renamed from test/mppa/instr/compw.lt.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/compw.ltu.c (renamed from test/mppa/instr/compw.ltu.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/compw.ne.c (renamed from test/mppa/instr/compw.ne.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/div2.c (renamed from test/mppa/instr/div2.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/doubleconv.c (renamed from test/mppa/instr/doubleconv.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/floatconv.c (renamed from test/mppa/instr/floatconv.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/fmuld.c (renamed from test/mppa/instr/fmuld.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/fmulw.c (renamed from test/mppa/instr/fmulw.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/fnegd.c (renamed from test/mppa/instr/fnegd.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/fnegw.c (renamed from test/mppa/instr/fnegw.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/for.c (renamed from test/mppa/instr/for.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/forvar.c (renamed from test/mppa/instr/forvar.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/forvarl.c (renamed from test/mppa/instr/forvarl.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/fsbfd.c (renamed from test/mppa/instr/fsbfd.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/fsbfw.c (renamed from test/mppa/instr/fsbfw.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/indirect_call.c (renamed from test/mppa/instr/indirect_call.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/indirect_tailcall.c (renamed from test/mppa/instr/indirect_tailcall.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/lbs.c (renamed from test/mppa/instr/lbs.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/lbz.c (renamed from test/mppa/instr/lbz.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/muld.c (renamed from test/mppa/instr/muld.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/mulw.c (renamed from test/mppa/instr/mulw.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/negd.c (renamed from test/mppa/instr/negd.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/ord.c (renamed from test/mppa/instr/ord.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/sbfd.c (renamed from test/mppa/instr/sbfd.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/sbfw.c (renamed from test/mppa/instr/sbfw.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/simple.c (renamed from test/mppa/instr/simple.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/sllw.c (renamed from test/mppa/instr/sllw.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/srad.c (renamed from test/mppa/instr/srad.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/srld.c (renamed from test/mppa/instr/srld.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/tailcall.c (renamed from test/mppa/instr/tailcall.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/udivd.c (renamed from test/mppa/instr/udivd.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/umodd.c (renamed from test/mppa/instr/umodd.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/individual/xord.c (renamed from test/mppa/instr/xord.c) | 0 | ||||
-rw-r--r-- | test/mppa/instr/modi32.c | 5 | ||||
-rw-r--r-- | test/mppa/instr/modui32.c | 7 | ||||
-rw-r--r-- | test/mppa/instr/ui32.c | 12 | ||||
-rw-r--r-- | test/mppa/instr/ui64.c (renamed from test/mppa/instr/compd.gtu.c) | 3 | ||||
-rw-r--r-- | test/mppa/interop/i32.c (renamed from test/mppa/interop/i_manyiargs.c) | 6 | ||||
-rw-r--r-- | test/mppa/interop/i64.c (renamed from test/mppa/interop/ll_manyllargs.c) | 8 | ||||
-rw-r--r-- | test/mppa/interop/individual/i_multiiargs.c (renamed from test/mppa/interop/i_multiiargs.c) | 2 | ||||
-rw-r--r-- | test/mppa/interop/individual/i_oneiarg.c (renamed from test/mppa/interop/i_oneiarg.c) | 2 | ||||
-rw-r--r-- | test/mppa/interop/individual/ll_multillargs.c (renamed from test/mppa/interop/ll_multillargs.c) | 2 | ||||
-rw-r--r-- | test/mppa/interop/individual/ll_onellarg.c (renamed from test/mppa/interop/ll_onellarg.c) | 2 | ||||
-rw-r--r-- | test/mppa/interop/individual/ll_void.c (renamed from test/mppa/interop/ll_void.c) | 2 | ||||
-rw-r--r-- | test/mppa/interop/individual/void_void.c (renamed from test/mppa/interop/void_void.c) | 2 | ||||
-rw-r--r-- | x86/Conventions1.v | 3 | ||||
-rw-r--r-- | x86/Machregsaux.ml | 9 | ||||
-rw-r--r-- | x86/Machregsaux.mli | 2 | ||||
-rw-r--r-- | x86/SelectLong.vp | 2 | ||||
-rw-r--r-- | x86/SelectLongproof.v | 1 | ||||
-rw-r--r-- | x86/SelectOp.vp | 8 | ||||
-rw-r--r-- | x86/SelectOpproof.v | 29 |
136 files changed, 595 insertions, 877 deletions
@@ -72,7 +72,7 @@ COMMON=Errors.v AST.v Linking.v \ # Back-end modules (in backend/, $(ARCH)/) BACKEND=\ - Cminor.v Op.v CminorSel.v \ + Cminor.v Op.v CminorSel.v OpHelpers.v OpHelpersproof.v \ SelectOp.v SelectDiv.v SplitLong.v SelectLong.v Selection.v \ SelectOpproof.v SelectDivproof.v SplitLongproof.v \ SelectLongproof.v Selectionproof.v \ diff --git a/arm/Machregsaux.ml b/arm/Machregsaux.ml index ce5c67f6..14c75155 100644 --- a/arm/Machregsaux.ml +++ b/arm/Machregsaux.ml @@ -33,3 +33,8 @@ let register_by_name s = let can_reserve_register r = List.mem r Conventions1.int_callee_save_regs || List.mem r Conventions1.float_callee_save_regs + +let class_of_type = function + | AST.Tint | AST.Tlong -> 0 + | AST.Tfloat | AST.Tsingle -> 1 + | AST.Tany32 | AST.Tany64 -> assert false diff --git a/arm/Machregsaux.mli b/arm/Machregsaux.mli index 9404568d..d7117c21 100644 --- a/arm/Machregsaux.mli +++ b/arm/Machregsaux.mli @@ -16,3 +16,5 @@ val name_of_register: Machregs.mreg -> string option val register_by_name: string -> Machregs.mreg option val is_scratch_register: string -> bool val can_reserve_register: Machregs.mreg -> bool + +val class_of_type: AST.typ -> int diff --git a/arm/SelectLong.vp b/arm/SelectLong.vp index cc7a38f6..b4cdd0e3 100644 --- a/arm/SelectLong.vp +++ b/arm/SelectLong.vp @@ -16,6 +16,6 @@ Require Import Coqlib. Require Import Compopts. Require Import AST Integers Floats. Require Import Op CminorSel. -Require Import SelectOp SplitLong. +Require Import OpHelpers SelectOp SplitLong. (** This file is empty because we use the default implementation provided in [SplitLong]. *) diff --git a/arm/SelectLongproof.v b/arm/SelectLongproof.v index a82c082c..a65a38d4 100644 --- a/arm/SelectLongproof.v +++ b/arm/SelectLongproof.v @@ -16,6 +16,7 @@ Require Import String Coqlib Maps Integers Floats Errors. Require Archi. Require Import AST Values Memory Globalenvs Events. Require Import Cminor Op CminorSel. +Require Import OpHelpers OpHelpersproof. Require Import SelectOp SelectOpproof SplitLong SplitLongproof. Require Import SelectLong. diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index c361df65..f3f01730 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -42,6 +42,7 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Op. +Require Import OpHelpers. Require Import CminorSel. Local Open Scope cminorsel_scope. @@ -508,3 +509,10 @@ Nondetfunction builtin_arg (e: expr) := | Eop (Oaddimm n) (e1:::Enil) => BA_addptr (BA e1) (BA_int n) | _ => BA e end. + +(* floats *) +Definition divf_base (e1: expr) (e2: expr) := + Eop Odivf (e1 ::: e2 ::: Enil). + +Definition divfs_base (e1: expr) (e2: expr) := + Eop Odivfs (e1 ::: e2 ::: Enil). diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index d4aac9b6..212bcfd7 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -24,6 +24,7 @@ Require Import Cminor. Require Import Op. Require Import CminorSel. Require Import SelectOp. +Require Import OpHelpers OpHelpersproof. Local Open Scope cminorsel_scope. Local Transparent Archi.ptr64. @@ -76,8 +77,10 @@ Ltac TrivialExists := (** * Correctness of the smart constructors *) Section CMCONSTR. - -Variable ge: genv. +Variable prog: program. +Variable hf: helper_functions. +Hypothesis HELPERS: helper_functions_declared prog hf. +Let ge := Genv.globalenv prog. Variable sp: val. Variable e: env. Variable m: mem. @@ -893,4 +896,25 @@ Proof. - constructor; auto. Qed. + +(* floating-point division without HELPERS *) +Theorem eval_divf_base: + forall le a b x y, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + exists v, eval_expr ge sp e m le (divf_base a b) v /\ Val.lessdef (Val.divf x y) v. +Proof. + intros; unfold divf_base. + TrivialExists. +Qed. + +Theorem eval_divfs_base: + forall le a b x y, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + exists v, eval_expr ge sp e m le (divfs_base a b) v /\ Val.lessdef (Val.divfs x y) v. +Proof. + intros; unfold divfs_base. + TrivialExists. +Qed. End CMCONSTR. diff --git a/backend/IRC.ml b/backend/IRC.ml index c7b1bf04..67da47da 100644 --- a/backend/IRC.ml +++ b/backend/IRC.ml @@ -15,6 +15,7 @@ open Camlcoq open AST open Registers open Machregs +open Machregsaux open Locations open Conventions1 open XTL @@ -237,13 +238,9 @@ type graph = { according to their types. A variable can be forced into class 2 by giving it a negative spill cost. *) -let class_of_type = function - | Tint | Tlong -> 0 - | Tfloat | Tsingle -> 0 (* normal: 1 *) - | Tany32 | Tany64 -> assert false -let class_of_reg r = 0 - (* normal: if Conventions1.is_float_reg r then 1 else 0 *) +let class_of_reg r = + if Conventions1.is_float_reg r then 1 else 0 let class_of_loc = function | R r -> class_of_reg r diff --git a/backend/IRC.mli b/backend/IRC.mli index 30b6d5c1..f7bbf9c5 100644 --- a/backend/IRC.mli +++ b/backend/IRC.mli @@ -43,5 +43,4 @@ val coloring: graph -> (var -> loc) val reserved_registers: mreg list ref (* Auxiliaries to deal with register classes *) -val class_of_type: AST.typ -> int val class_of_loc: loc -> int diff --git a/backend/OpHelpers.v b/backend/OpHelpers.v new file mode 100644 index 00000000..53414dab --- /dev/null +++ b/backend/OpHelpers.v @@ -0,0 +1,42 @@ +Require Import Coqlib. +Require Import AST Integers Floats. +Require Import Op CminorSel. + +(** Some arithmetic operations 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. +Definition sig_ff_f := mksignature (Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default. +Definition sig_ss_s := mksignature (Tsingle :: Tsingle :: nil) (Some Tsingle) 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 *) + f64_div: ident; (**float division*) + f32_div: ident; (**float division*) +}. diff --git a/backend/OpHelpersproof.v b/backend/OpHelpersproof.v new file mode 100644 index 00000000..63040c5f --- /dev/null +++ b/backend/OpHelpersproof.v @@ -0,0 +1,78 @@ +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Memory. +Require Import Globalenvs. +Require Import Cminor. +Require Import Op. +Require Import CminorSel. +Require Import Events. +Require Import OpHelpers. + +(** * 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 arith_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.divs x y = Some z -> external_implements "__compcert_i32_sdiv" sig_ii_i (x::y::nil) z) + /\ (forall x y z, Val.divu x y = Some z -> external_implements "__compcert_i32_udiv" sig_ii_i (x::y::nil) z) + /\ (forall x y z, Val.mods x y = Some z -> external_implements "__compcert_i32_smod" sig_ii_i (x::y::nil) z) + /\ (forall x y z, Val.modu x y = Some z -> external_implements "__compcert_i32_umod" sig_ii_i (x::y::nil) z) + /\ (forall x y z, Val.divfs x y = z -> external_implements "__compcert_f32_div" sig_ss_s (x::y::nil) z) + /\ (forall x y z, Val.divf x y = z -> external_implements "__compcert_f64_div" sig_ff_f (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 + /\ helper_declared p f32_div "__compcert_f32_div" sig_ss_s + /\ helper_declared p f64_div "__compcert_f64_div" sig_ff_f +. diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index 19aba4f6..7db8a866 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -1067,7 +1067,7 @@ let make_parmove srcs dsts itmp ftmp k = | Locations.S(sl, ofs, ty), R rd -> code := LTL.Lgetstack(sl, ofs, ty, rd) :: !code | Locations.S(sls, ofss, tys), Locations.S(sld, ofsd, tyd) -> - let tmp = temp_for (class_of_type tys) in + let tmp = temp_for (Machregsaux.class_of_type tys) in (* code will be reversed at the end *) code := LTL.Lsetstack(tmp, sld, ofsd, tyd) :: LTL.Lgetstack(sls, ofss, tys, tmp) :: !code diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp index 7241d028..9f852616 100644 --- a/backend/SelectDiv.vp +++ b/backend/SelectDiv.vp @@ -15,7 +15,7 @@ Require Import Coqlib. Require Import Compopts. Require Import AST Integers Floats. -Require Import Op CminorSel SelectOp SplitLong SelectLong. +Require Import Op CminorSel OpHelpers SelectOp SplitLong SelectLong. Local Open Scope cminorsel_scope. diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index dbd3f58d..e2249ddb 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -15,6 +15,7 @@ Require Import Zquot Coqlib. Require Import AST Integers Floats Values Memory Globalenvs Events. Require Import Cminor Op CminorSel. +Require Import OpHelpers OpHelpersproof. Require Import SelectOp SelectOpproof SplitLong SplitLongproof SelectLong SelectLongproof SelectDiv. Local Open Scope cminorsel_scope. diff --git a/backend/Selection.v b/backend/Selection.v index aba84049..05a06abf 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -26,7 +26,7 @@ Require String. Require Import Coqlib Maps. Require Import AST Errors Integers Globalenvs Switch. Require Cminor. -Require Import Op CminorSel. +Require Import Op CminorSel OpHelpers. Require Import SelectOp SplitLong SelectLong SelectDiv. Require Machregs. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 5a0fafaf..50ff377a 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -16,6 +16,7 @@ Require Import FunInd. Require Import Coqlib Maps. Require Import AST Linking Errors Integers Values Memory Events Globalenvs Smallstep. Require Import Switch Cminor Op CminorSel. +Require Import OpHelpers OpHelpersproof. Require Import SelectOp SelectDiv SplitLong SelectLong Selection. Require Import SelectOpproof SelectDivproof SplitLongproof SelectLongproof. diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp index 6a7d4f5c..dfe42df0 100644 --- a/backend/SplitLong.vp +++ b/backend/SplitLong.vp @@ -16,6 +16,7 @@ Require String. Require Import Coqlib. Require Import AST Integers Floats. Require Import Op CminorSel. +Require Import OpHelpers. Require Import SelectOp. Local Open Scope cminorsel_scope. diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v index a74276c7..6718ba5b 100644 --- a/backend/SplitLongproof.v +++ b/backend/SplitLongproof.v @@ -16,6 +16,7 @@ Require Import String. Require Import Coqlib Maps. Require Import AST Errors Integers Floats. Require Import Values Memory Globalenvs Events Cminor Op CminorSel. +Require Import OpHelpers OpHelpersproof. Require Import SelectOp SelectOpproof SplitLong. Local Open Scope cminorsel_scope. @@ -33,7 +34,7 @@ Variable sp: val. Variable e: env. Variable m: mem. -Ltac UseHelper := decompose [Logic.and] i64_helpers_correct; eauto. +Ltac UseHelper := decompose [Logic.and] arith_helpers_correct; eauto. Ltac DeclHelper := red in HELPERS; decompose [Logic.and] HELPERS; eauto. Lemma eval_helper: diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 493f4a05..0ca554ab 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -50,9 +50,6 @@ Inductive instruction : Type := | Psemi (**r semi colon separating bundles *)
| Pnop (**r instruction that does nothing *)
- | Pdiv (**r 32 bits integer division *)
- | Pdivu (**r 32 bits integer division *)
-
(** builtins *)
| Pclzll (rd rs: ireg)
| Pstsud (rd rs1 rs2: ireg)
@@ -218,8 +215,6 @@ Inductive instruction : Type := Definition control_to_instruction (c: control) :=
match c with
| PExpand (Asmblock.Pbuiltin ef args res) => Pbuiltin ef args res
- | PExpand (Asmblock.Pdiv) => Pdiv
- | PExpand (Asmblock.Pdivu) => Pdivu
| PCtlFlow Asmblock.Pret => Pret
| PCtlFlow (Asmblock.Pcall l) => Pcall l
| PCtlFlow (Asmblock.Picall r) => Picall r
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index d335801e..fdec8ed2 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -178,10 +178,7 @@ Inductive ex_instruction : Type := | Pbtbl (r: ireg) (tbl: list label) (**r N-way branch through a jump table *) *) | Pbuiltin: external_function -> list (builtin_arg preg) - -> builtin_res preg -> ex_instruction (**r built-in function (pseudo) *) - | Pdiv (**r 32 bits integer division, call to __divdi3 *) - | Pdivu (**r 32 bits integer division, call to __udivdi3 *) -. + -> builtin_res preg -> ex_instruction (**r built-in function (pseudo) *). (** FIXME: comment not up to date ! @@ -1486,17 +1483,6 @@ Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) (** Pseudo-instructions *) | Pbuiltin ef args res => Stuck (**r treated specially below *) - | Pdiv => - match Val.divs (rs GPR0) (rs GPR1) with - | Some v => Next (rs # GPR0 <- v # RA <- (rs RA)) m - | None => Stuck - end - - | Pdivu => - match Val.divu (rs GPR0) (rs GPR1) with - | Some v => Next (rs # GPR0 <- v # RA <- (rs RA)) m - | None => Stuck - end end | None => Next rs m end. diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 501ec212..ad96ae87 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -540,8 +540,6 @@ Definition trans_control (ctl: control) : macro := | Pj_l l => [(#PC, Op (Control (Oj_l l)) (Name (#PC) @ Enil))] | Pcb bt r l => [(#PC, Op (Control (Ocb bt l)) (Name (#r) @ Name (#PC) @ Enil))] | Pcbu bt r l => [(#PC, Op (Control (Ocbu bt l)) (Name (#r) @ Name (#PC) @ Enil))] - | Pdiv => [(#GPR0, Op (Control Odiv) (Name (#GPR0) @ Name (#GPR1) @ Enil)); (#RA, Name (#RA))] - | Pdivu => [(#GPR0, Op (Control Odivu) (Name (#GPR0) @ Name (#GPR1) @ Enil)); (#RA, Name (#RA))] | Pbuiltin ef args res => [(#PC, Op (Control (OError)) Enil)] end. @@ -863,22 +861,6 @@ Proof. intros. destruct ex. - simpl in *. inv H1. destruct c; destruct i; try discriminate. all: try (inv H0; eexists; split; try split; [ simpl control_eval; pose (H3 PC); simpl in e; rewrite e; reflexivity | Simpl | intros rr; destruct rr; Simpl]). - (* Pdiv *) - + destruct (Val.divs _ _) eqn:DIVS; try discriminate. inv H0. unfold nextblock in DIVS. repeat (rewrite Pregmap.gso in DIVS; try discriminate). - eexists; split; try split. - * simpl control_eval. pose (H3 PC); simpl in e; rewrite e; clear e. simpl. - Simpl. pose (H3 GPR0); rewrite e; clear e. pose (H3 GPR1); rewrite e; clear e. rewrite DIVS. - Simpl. - * Simpl. - * intros rr; destruct rr; Simpl. destruct (preg_eq GPR0 g); Simpl. rewrite e. Simpl. - (* Pdivu *) - + destruct (Val.divu _ _) eqn:DIVU; try discriminate. inv H0. unfold nextblock in DIVU. repeat (rewrite Pregmap.gso in DIVU; try discriminate). - eexists; split; try split. - * simpl control_eval. pose (H3 PC); simpl in e; rewrite e; clear e. simpl. - Simpl. pose (H3 GPR0); rewrite e; clear e. pose (H3 GPR1); rewrite e; clear e. rewrite DIVU. - Simpl. - * Simpl. - * intros rr; destruct rr; Simpl. destruct (preg_eq GPR0 g); Simpl. rewrite e. Simpl. (* Pj_l *) + unfold goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (nextblock _ _ _) eqn:NB; try discriminate. inv H0. eexists; split; try split. @@ -1070,12 +1052,6 @@ Lemma exec_exit_none: Proof. intros. inv H0. destruct ex as [ctl|]; try discriminate. destruct ctl; destruct i; try reflexivity; try discriminate. -(* Pdiv *) - - simpl in *. pose (H3 GPR0); rewrite e in H1; clear e. pose (H3 GPR1); rewrite e in H1; clear e. - destruct (Val.divs _ _); try discriminate; auto. -(* Pdivu *) - - simpl in *. pose (H3 GPR0); rewrite e in H1; clear e. pose (H3 GPR1); rewrite e in H1; clear e. - destruct (Val.divu _ _); try discriminate; auto. (* Pj_l *) - simpl in *. pose (H3 PC); simpl in e; rewrite e in H1. clear e. unfold goto_label_deps in H1. unfold goto_label. @@ -1187,11 +1163,6 @@ Lemma forward_simu_exit_stuck: Proof. intros. inv H1. destruct ex as [ctl|]; try discriminate. destruct ctl; destruct i; try discriminate; try (simpl; reflexivity). -(* Pdiv *) - - simpl in *. pose (H3 GPR0); simpl in e; rewrite e; clear e. pose (H3 GPR1); simpl in e; rewrite e; clear e. - destruct (Val.divs _ _); try discriminate; auto. - - simpl in *. pose (H3 GPR0); simpl in e; rewrite e; clear e. pose (H3 GPR1); simpl in e; rewrite e; clear e. - destruct (Val.divu _ _); try discriminate; auto. (* Pj_l *) - simpl in *. pose (H3 PC); simpl in e; rewrite e. unfold goto_label_deps. unfold goto_label in H0. destruct (label_pos _ _ _); auto. clear e. destruct (rs PC); auto. discriminate. diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 5b00a64f..c03e319c 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -425,18 +425,6 @@ Definition transl_op OK (mulimm32 rd rs1 n ::i k) | Omulhs, _ => Error(msg "Asmblockgen.transl_op: Omulhs") (* Normalement pas émis *) | Omulhu, _ => Error(msg "Asmblockgen.transl_op: Omulhu") (* Normalement pas émis *) - | Odiv, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odiv: 32-bits division not supported yet. Please use 64-bits.") - (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Pdivw rd rs1 rs2 :: k) *) - | Odivu, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odivu: 32-bits division not supported yet. Please use 64-bits.") - (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Pdivuw rd rs1 rs2 :: k) *) - | Omod, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Omod: 32-bits modulo not supported yet. Please use 64-bits.") - (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Premw rd rs1 rs2 :: k) *) - | Omodu, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Omodu: 32-bits modulo not supported yet. Please use 64-bits.") - (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Premuw rd rs1 rs2 :: k) *) | Oand, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pandw rd rs1 rs2 ::i k) diff --git a/mppa_k1c/ConstpropOp.v b/mppa_k1c/ConstpropOp.v deleted file mode 100644 index e7391ab5..00000000 --- a/mppa_k1c/ConstpropOp.v +++ /dev/null @@ -1,613 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Strength reduction for operators and conditions. - This is the machine-dependent part of [Constprop]. *) - -Require Archi. -Require Import Coqlib Compopts. -Require Import AST Integers Floats. -Require Import Op Registers. -Require Import ValueDomain. - -(** * Converting known values to constants *) - -Definition const_for_result (a: aval) : option operation := - match a with - | I n => Some(Ointconst n) - | L n => if Archi.ptr64 then Some(Olongconst n) else None - | F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None - | FS n => if Compopts.generate_float_constants tt then Some(Osingleconst n) else None - | Ptr(Gl id ofs) => Some(Oaddrsymbol id ofs) - | Ptr(Stk ofs) => Some(Oaddrstack ofs) - | _ => None - end. - -(** * Operator strength reduction *) - -(** We now define auxiliary functions for strength reduction of - operators and addressing modes: replacing an operator with a cheaper - one if some of its arguments are statically known. These are again - large pattern-matchings expressed in indirect style. *) - -(** Original definition: -<< -Nondetfunction cond_strength_reduction - (cond: condition) (args: list reg) (vl: list aval) := - match cond, args, vl with - | Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil => - (Ccompimm (swap_comparison c) n1, r2 :: nil) - | Ccomp c, r1 :: r2 :: nil, v1 :: I n2 :: nil => - (Ccompimm c n2, r1 :: nil) - | Ccompu c, r1 :: r2 :: nil, I n1 :: v2 :: nil => - (Ccompuimm (swap_comparison c) n1, r2 :: nil) - | Ccompu c, r1 :: r2 :: nil, v1 :: I n2 :: nil => - (Ccompuimm c n2, r1 :: nil) - | Ccompl c, r1 :: r2 :: nil, L n1 :: v2 :: nil => - (Ccomplimm (swap_comparison c) n1, r2 :: nil) - | Ccompl c, r1 :: r2 :: nil, v1 :: L n2 :: nil => - (Ccomplimm c n2, r1 :: nil) - | Ccomplu c, r1 :: r2 :: nil, L n1 :: v2 :: nil => - (Ccompluimm (swap_comparison c) n1, r2 :: nil) - | Ccomplu c, r1 :: r2 :: nil, v1 :: L n2 :: nil => - (Ccompluimm c n2, r1 :: nil) - | _, _, _ => - (cond, args) - end. ->> -*) - -Inductive cond_strength_reduction_cases: forall (cond: condition) (args: list reg) (vl: list aval), Type := - | cond_strength_reduction_case1: forall c r1 r2 n1 v2, cond_strength_reduction_cases (Ccomp c) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | cond_strength_reduction_case2: forall c r1 r2 v1 n2, cond_strength_reduction_cases (Ccomp c) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | cond_strength_reduction_case3: forall c r1 r2 n1 v2, cond_strength_reduction_cases (Ccompu c) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | cond_strength_reduction_case4: forall c r1 r2 v1 n2, cond_strength_reduction_cases (Ccompu c) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | cond_strength_reduction_case5: forall c r1 r2 n1 v2, cond_strength_reduction_cases (Ccompl c) (r1 :: r2 :: nil) (L n1 :: v2 :: nil) - | cond_strength_reduction_case6: forall c r1 r2 v1 n2, cond_strength_reduction_cases (Ccompl c) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | cond_strength_reduction_case7: forall c r1 r2 n1 v2, cond_strength_reduction_cases (Ccomplu c) (r1 :: r2 :: nil) (L n1 :: v2 :: nil) - | cond_strength_reduction_case8: forall c r1 r2 v1 n2, cond_strength_reduction_cases (Ccomplu c) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | cond_strength_reduction_default: forall (cond: condition) (args: list reg) (vl: list aval), cond_strength_reduction_cases cond args vl. - -Definition cond_strength_reduction_match (cond: condition) (args: list reg) (vl: list aval) := - match cond as zz1, args as zz2, vl as zz3 return cond_strength_reduction_cases zz1 zz2 zz3 with - | Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil => cond_strength_reduction_case1 c r1 r2 n1 v2 - | Ccomp c, r1 :: r2 :: nil, v1 :: I n2 :: nil => cond_strength_reduction_case2 c r1 r2 v1 n2 - | Ccompu c, r1 :: r2 :: nil, I n1 :: v2 :: nil => cond_strength_reduction_case3 c r1 r2 n1 v2 - | Ccompu c, r1 :: r2 :: nil, v1 :: I n2 :: nil => cond_strength_reduction_case4 c r1 r2 v1 n2 - | Ccompl c, r1 :: r2 :: nil, L n1 :: v2 :: nil => cond_strength_reduction_case5 c r1 r2 n1 v2 - | Ccompl c, r1 :: r2 :: nil, v1 :: L n2 :: nil => cond_strength_reduction_case6 c r1 r2 v1 n2 - | Ccomplu c, r1 :: r2 :: nil, L n1 :: v2 :: nil => cond_strength_reduction_case7 c r1 r2 n1 v2 - | Ccomplu c, r1 :: r2 :: nil, v1 :: L n2 :: nil => cond_strength_reduction_case8 c r1 r2 v1 n2 - | cond, args, vl => cond_strength_reduction_default cond args vl - end. - -Definition cond_strength_reduction (cond: condition) (args: list reg) (vl: list aval) := - match cond_strength_reduction_match cond args vl with - | cond_strength_reduction_case1 c r1 r2 n1 v2 => (* Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - (Ccompimm (swap_comparison c) n1, r2 :: nil) - | cond_strength_reduction_case2 c r1 r2 v1 n2 => (* Ccomp c, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - (Ccompimm c n2, r1 :: nil) - | cond_strength_reduction_case3 c r1 r2 n1 v2 => (* Ccompu c, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - (Ccompuimm (swap_comparison c) n1, r2 :: nil) - | cond_strength_reduction_case4 c r1 r2 v1 n2 => (* Ccompu c, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - (Ccompuimm c n2, r1 :: nil) - | cond_strength_reduction_case5 c r1 r2 n1 v2 => (* Ccompl c, r1 :: r2 :: nil, L n1 :: v2 :: nil *) - (Ccomplimm (swap_comparison c) n1, r2 :: nil) - | cond_strength_reduction_case6 c r1 r2 v1 n2 => (* Ccompl c, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - (Ccomplimm c n2, r1 :: nil) - | cond_strength_reduction_case7 c r1 r2 n1 v2 => (* Ccomplu c, r1 :: r2 :: nil, L n1 :: v2 :: nil *) - (Ccompluimm (swap_comparison c) n1, r2 :: nil) - | cond_strength_reduction_case8 c r1 r2 v1 n2 => (* Ccomplu c, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - (Ccompluimm c n2, r1 :: nil) - | cond_strength_reduction_default cond args vl => - (cond, args) - end. - - -Definition make_cmp_base (c: condition) (args: list reg) (vl: list aval) := - let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args'). - -Definition make_cmp_imm_eq (c: condition) (args: list reg) (vl: list aval) - (n: int) (r1: reg) (v1: aval) := - if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil) - else if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil) - else make_cmp_base c args vl. - -Definition make_cmp_imm_ne (c: condition) (args: list reg) (vl: list aval) - (n: int) (r1: reg) (v1: aval) := - if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil) - else if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil) - else make_cmp_base c args vl. - -(** Original definition: -<< -Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) := - match c, args, vl with - | Ccompimm Ceq n, r1 :: nil, v1 :: nil => - make_cmp_imm_eq c args vl n r1 v1 - | Ccompimm Cne n, r1 :: nil, v1 :: nil => - make_cmp_imm_ne c args vl n r1 v1 - | Ccompuimm Ceq n, r1 :: nil, v1 :: nil => - make_cmp_imm_eq c args vl n r1 v1 - | Ccompuimm Cne n, r1 :: nil, v1 :: nil => - make_cmp_imm_ne c args vl n r1 v1 - | _, _, _ => - make_cmp_base c args vl - end. ->> -*) - -Inductive make_cmp_cases: forall (c: condition) (args: list reg) (vl: list aval), Type := - | make_cmp_case1: forall n r1 v1, make_cmp_cases (Ccompimm Ceq n) (r1 :: nil) (v1 :: nil) - | make_cmp_case2: forall n r1 v1, make_cmp_cases (Ccompimm Cne n) (r1 :: nil) (v1 :: nil) - | make_cmp_case3: forall n r1 v1, make_cmp_cases (Ccompuimm Ceq n) (r1 :: nil) (v1 :: nil) - | make_cmp_case4: forall n r1 v1, make_cmp_cases (Ccompuimm Cne n) (r1 :: nil) (v1 :: nil) - | make_cmp_default: forall (c: condition) (args: list reg) (vl: list aval), make_cmp_cases c args vl. - -Definition make_cmp_match (c: condition) (args: list reg) (vl: list aval) := - match c as zz1, args as zz2, vl as zz3 return make_cmp_cases zz1 zz2 zz3 with - | Ccompimm Ceq n, r1 :: nil, v1 :: nil => make_cmp_case1 n r1 v1 - | Ccompimm Cne n, r1 :: nil, v1 :: nil => make_cmp_case2 n r1 v1 - | Ccompuimm Ceq n, r1 :: nil, v1 :: nil => make_cmp_case3 n r1 v1 - | Ccompuimm Cne n, r1 :: nil, v1 :: nil => make_cmp_case4 n r1 v1 - | c, args, vl => make_cmp_default c args vl - end. - -Definition make_cmp (c: condition) (args: list reg) (vl: list aval) := - match make_cmp_match c args vl with - | make_cmp_case1 n r1 v1 => (* Ccompimm Ceq n, r1 :: nil, v1 :: nil *) - make_cmp_imm_eq c args vl n r1 v1 - | make_cmp_case2 n r1 v1 => (* Ccompimm Cne n, r1 :: nil, v1 :: nil *) - make_cmp_imm_ne c args vl n r1 v1 - | make_cmp_case3 n r1 v1 => (* Ccompuimm Ceq n, r1 :: nil, v1 :: nil *) - make_cmp_imm_eq c args vl n r1 v1 - | make_cmp_case4 n r1 v1 => (* Ccompuimm Cne n, r1 :: nil, v1 :: nil *) - make_cmp_imm_ne c args vl n r1 v1 - | make_cmp_default c args vl => - make_cmp_base c args vl - end. - - -Definition make_addimm (n: int) (r: reg) := - if Int.eq n Int.zero - then (Omove, r :: nil) - else (Oaddimm n, r :: nil). - -Definition make_shlimm (n: int) (r1 r2: reg) := - if Int.eq n Int.zero then (Omove, r1 :: nil) - else if Int.ltu n Int.iwordsize then (Oshlimm n, r1 :: nil) - else (Oshl, r1 :: r2 :: nil). - -Definition make_shrimm (n: int) (r1 r2: reg) := - if Int.eq n Int.zero then (Omove, r1 :: nil) - else if Int.ltu n Int.iwordsize then (Oshrimm n, r1 :: nil) - else (Oshr, r1 :: r2 :: nil). - -Definition make_shruimm (n: int) (r1 r2: reg) := - if Int.eq n Int.zero then (Omove, r1 :: nil) - else if Int.ltu n Int.iwordsize then (Oshruimm n, r1 :: nil) - else (Oshru, r1 :: r2 :: nil). - -Definition make_mulimm (n: int) (r1 r2: reg) := - if Int.eq n Int.zero then - (Ointconst Int.zero, nil) - else if Int.eq n Int.one then - (Omove, r1 :: nil) - else - match Int.is_power2 n with - | Some l => (Oshlimm l, r1 :: nil) - | None => (Omul, r1 :: r2 :: nil) - end. - -Definition make_andimm (n: int) (r: reg) (a: aval) := - if Int.eq n Int.zero then (Ointconst Int.zero, nil) - else if Int.eq n Int.mone then (Omove, r :: nil) - else if match a with Uns _ m => Int.eq (Int.zero_ext m (Int.not n)) Int.zero - | _ => false end - then (Omove, r :: nil) - else (Oandimm n, r :: nil). - -Definition make_orimm (n: int) (r: reg) := - if Int.eq n Int.zero then (Omove, r :: nil) - else if Int.eq n Int.mone then (Ointconst Int.mone, nil) - else (Oorimm n, r :: nil). - -Definition make_xorimm (n: int) (r: reg) := - if Int.eq n Int.zero then (Omove, r :: nil) - else (Oxorimm n, r :: nil). - -Definition make_divimm n (r1 r2: reg) := - if Int.eq n Int.one then - (Omove, r1 :: nil) - else - match Int.is_power2 n with - | Some l => if Int.ltu l (Int.repr 31) - then (Oshrximm l, r1 :: nil) - else (Odiv, r1 :: r2 :: nil) - | None => (Odiv, r1 :: r2 :: nil) - end. - -Definition make_divuimm n (r1 r2: reg) := - if Int.eq n Int.one then - (Omove, r1 :: nil) - else - match Int.is_power2 n with - | Some l => (Oshruimm l, r1 :: nil) - | None => (Odivu, r1 :: r2 :: nil) - end. - -Definition make_moduimm n (r1 r2: reg) := - match Int.is_power2 n with - | Some l => (Oandimm (Int.sub n Int.one), r1 :: nil) - | None => (Omodu, r1 :: r2 :: nil) - end. - -Definition make_addlimm (n: int64) (r: reg) := - if Int64.eq n Int64.zero - then (Omove, r :: nil) - else (Oaddlimm n, r :: nil). - -Definition make_shllimm (n: int) (r1 r2: reg) := - if Int.eq n Int.zero then (Omove, r1 :: nil) - else if Int.ltu n Int64.iwordsize' then (Oshllimm n, r1 :: nil) - else (Oshll, r1 :: r2 :: nil). - -Definition make_shrlimm (n: int) (r1 r2: reg) := - if Int.eq n Int.zero then (Omove, r1 :: nil) - else if Int.ltu n Int64.iwordsize' then (Oshrlimm n, r1 :: nil) - else (Oshrl, r1 :: r2 :: nil). - -Definition make_shrluimm (n: int) (r1 r2: reg) := - if Int.eq n Int.zero then (Omove, r1 :: nil) - else if Int.ltu n Int64.iwordsize' then (Oshrluimm n, r1 :: nil) - else (Oshrlu, r1 :: r2 :: nil). - -Definition make_mullimm (n: int64) (r1 r2: reg) := - if Int64.eq n Int64.zero then - (Olongconst Int64.zero, nil) - else if Int64.eq n Int64.one then - (Omove, r1 :: nil) - else - match Int64.is_power2' n with - | Some l => (Oshllimm l, r1 :: nil) - | None => (Omull, r1 :: r2 :: nil) - end. - -Definition make_andlimm (n: int64) (r: reg) (a: aval) := - if Int64.eq n Int64.zero then (Olongconst Int64.zero, nil) - else if Int64.eq n Int64.mone then (Omove, r :: nil) - else (Oandlimm n, r :: nil). - -Definition make_orlimm (n: int64) (r: reg) := - if Int64.eq n Int64.zero then (Omove, r :: nil) - else if Int64.eq n Int64.mone then (Olongconst Int64.mone, nil) - else (Oorlimm n, r :: nil). - -Definition make_xorlimm (n: int64) (r: reg) := - if Int64.eq n Int64.zero then (Omove, r :: nil) - else (Oxorlimm n, r :: nil). - -Definition make_divlimm n (r1 r2: reg) := - match Int64.is_power2' n with - | Some l => if Int.ltu l (Int.repr 63) - then (Oshrxlimm l, r1 :: nil) - else (Odivl, r1 :: r2 :: nil) - | None => (Odivl, r1 :: r2 :: nil) - end. - -Definition make_divluimm n (r1 r2: reg) := - match Int64.is_power2' n with - | Some l => (Oshrluimm l, r1 :: nil) - | None => (Odivlu, r1 :: r2 :: nil) - end. - -Definition make_modluimm n (r1 r2: reg) := - match Int64.is_power2 n with - | Some l => (Oandlimm (Int64.sub n Int64.one), r1 :: nil) - | None => (Omodlu, r1 :: r2 :: nil) - end. - -Definition make_mulfimm (n: float) (r r1 r2: reg) := - if Float.eq_dec n (Float.of_int (Int.repr 2)) - then (Oaddf, r :: r :: nil) - else (Omulf, r1 :: r2 :: nil). - -Definition make_mulfsimm (n: float32) (r r1 r2: reg) := - if Float32.eq_dec n (Float32.of_int (Int.repr 2)) - then (Oaddfs, r :: r :: nil) - else (Omulfs, r1 :: r2 :: nil). - -Definition make_cast8signed (r: reg) (a: aval) := - if vincl a (Sgn Ptop 8) then (Omove, r :: nil) else (Ocast8signed, r :: nil). -Definition make_cast16signed (r: reg) (a: aval) := - if vincl a (Sgn Ptop 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil). - -(** Original definition: -<< -Nondetfunction op_strength_reduction - (op: operation) (args: list reg) (vl: list aval) := - match op, args, vl with - | Ocast8signed, r1 :: nil, v1 :: nil => make_cast8signed r1 v1 - | Ocast16signed, r1 :: nil, v1 :: nil => make_cast16signed r1 v1 - | Oadd, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_addimm n1 r2 - | Oadd, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm n2 r1 - | Osub, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm (Int.neg n2) r1 - | Omul, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_mulimm n1 r2 r1 - | Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_mulimm n2 r1 r2 - | Odiv, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_divimm n2 r1 r2 - | Odivu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_divuimm n2 r1 r2 - | Omodu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_moduimm n2 r1 r2 - | Oand, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_andimm n1 r2 v2 - | Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm n2 r1 v1 - | Oandimm n, r1 :: nil, v1 :: nil => make_andimm n r1 v1 - | Oor, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_orimm n1 r2 - | Oor, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_orimm n2 r1 - | Oxor, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_xorimm n1 r2 - | Oxor, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_xorimm n2 r1 - | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shlimm n2 r1 r2 - | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1 r2 - | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 r2 - | Oaddl, r1 :: r2 :: nil, L n1 :: v2 :: nil => make_addlimm n1 r2 - | Oaddl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_addlimm n2 r1 - | Osubl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_addlimm (Int64.neg n2) r1 - | Omull, r1 :: r2 :: nil, L n1 :: v2 :: nil => make_mullimm n1 r2 r1 - | Omull, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_mullimm n2 r1 r2 - | Odivl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_divlimm n2 r1 r2 - | Odivlu, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_divluimm n2 r1 r2 - | Omodlu, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_modluimm n2 r1 r2 - | Oandl, r1 :: r2 :: nil, L n1 :: v2 :: nil => make_andlimm n1 r2 v2 - | Oandl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_andlimm n2 r1 v1 - | Oandlimm n, r1 :: nil, v1 :: nil => make_andlimm n r1 v1 - | Oorl, r1 :: r2 :: nil, L n1 :: v2 :: nil => make_orlimm n1 r2 - | Oorl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_orlimm n2 r1 - | Oxorl, r1 :: r2 :: nil, L n1 :: v2 :: nil => make_xorlimm n1 r2 - | Oxorl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_xorlimm n2 r1 - | Oshll, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shllimm n2 r1 r2 - | Oshrl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrlimm n2 r1 r2 - | Oshrlu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrluimm n2 r1 r2 - | Ocmp c, args, vl => make_cmp c args vl - | Omulf, r1 :: r2 :: nil, v1 :: F n2 :: nil => make_mulfimm n2 r1 r1 r2 - | Omulf, r1 :: r2 :: nil, F n1 :: v2 :: nil => make_mulfimm n1 r2 r1 r2 - | Omulfs, r1 :: r2 :: nil, v1 :: FS n2 :: nil => make_mulfsimm n2 r1 r1 r2 - | Omulfs, r1 :: r2 :: nil, FS n1 :: v2 :: nil => make_mulfsimm n1 r2 r1 r2 - | _, _, _ => (op, args) - end. ->> -*) - -Inductive op_strength_reduction_cases: forall (op: operation) (args: list reg) (vl: list aval), Type := - | op_strength_reduction_case1: forall r1 v1, op_strength_reduction_cases (Ocast8signed) (r1 :: nil) (v1 :: nil) - | op_strength_reduction_case2: forall r1 v1, op_strength_reduction_cases (Ocast16signed) (r1 :: nil) (v1 :: nil) - | op_strength_reduction_case3: forall r1 r2 n1 v2, op_strength_reduction_cases (Oadd) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | op_strength_reduction_case4: forall r1 r2 v1 n2, op_strength_reduction_cases (Oadd) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case5: forall r1 r2 v1 n2, op_strength_reduction_cases (Osub) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case6: forall r1 r2 n1 v2, op_strength_reduction_cases (Omul) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | op_strength_reduction_case7: forall r1 r2 v1 n2, op_strength_reduction_cases (Omul) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case8: forall r1 r2 v1 n2, op_strength_reduction_cases (Odiv) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case9: forall r1 r2 v1 n2, op_strength_reduction_cases (Odivu) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case10: forall r1 r2 v1 n2, op_strength_reduction_cases (Omodu) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case11: forall r1 r2 n1 v2, op_strength_reduction_cases (Oand) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | op_strength_reduction_case12: forall r1 r2 v1 n2, op_strength_reduction_cases (Oand) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case13: forall n r1 v1, op_strength_reduction_cases (Oandimm n) (r1 :: nil) (v1 :: nil) - | op_strength_reduction_case14: forall r1 r2 n1 v2, op_strength_reduction_cases (Oor) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | op_strength_reduction_case15: forall r1 r2 v1 n2, op_strength_reduction_cases (Oor) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case16: forall r1 r2 n1 v2, op_strength_reduction_cases (Oxor) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | op_strength_reduction_case17: forall r1 r2 v1 n2, op_strength_reduction_cases (Oxor) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case18: forall r1 r2 v1 n2, op_strength_reduction_cases (Oshl) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case19: forall r1 r2 v1 n2, op_strength_reduction_cases (Oshr) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case20: forall r1 r2 v1 n2, op_strength_reduction_cases (Oshru) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case21: forall r1 r2 n1 v2, op_strength_reduction_cases (Oaddl) (r1 :: r2 :: nil) (L n1 :: v2 :: nil) - | op_strength_reduction_case22: forall r1 r2 v1 n2, op_strength_reduction_cases (Oaddl) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | op_strength_reduction_case23: forall r1 r2 v1 n2, op_strength_reduction_cases (Osubl) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | op_strength_reduction_case24: forall r1 r2 n1 v2, op_strength_reduction_cases (Omull) (r1 :: r2 :: nil) (L n1 :: v2 :: nil) - | op_strength_reduction_case25: forall r1 r2 v1 n2, op_strength_reduction_cases (Omull) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | op_strength_reduction_case26: forall r1 r2 v1 n2, op_strength_reduction_cases (Odivl) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | op_strength_reduction_case27: forall r1 r2 v1 n2, op_strength_reduction_cases (Odivlu) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | op_strength_reduction_case28: forall r1 r2 v1 n2, op_strength_reduction_cases (Omodlu) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | op_strength_reduction_case29: forall r1 r2 n1 v2, op_strength_reduction_cases (Oandl) (r1 :: r2 :: nil) (L n1 :: v2 :: nil) - | op_strength_reduction_case30: forall r1 r2 v1 n2, op_strength_reduction_cases (Oandl) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | op_strength_reduction_case31: forall n r1 v1, op_strength_reduction_cases (Oandlimm n) (r1 :: nil) (v1 :: nil) - | op_strength_reduction_case32: forall r1 r2 n1 v2, op_strength_reduction_cases (Oorl) (r1 :: r2 :: nil) (L n1 :: v2 :: nil) - | op_strength_reduction_case33: forall r1 r2 v1 n2, op_strength_reduction_cases (Oorl) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | op_strength_reduction_case34: forall r1 r2 n1 v2, op_strength_reduction_cases (Oxorl) (r1 :: r2 :: nil) (L n1 :: v2 :: nil) - | op_strength_reduction_case35: forall r1 r2 v1 n2, op_strength_reduction_cases (Oxorl) (r1 :: r2 :: nil) (v1 :: L n2 :: nil) - | op_strength_reduction_case36: forall r1 r2 v1 n2, op_strength_reduction_cases (Oshll) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case37: forall r1 r2 v1 n2, op_strength_reduction_cases (Oshrl) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case38: forall r1 r2 v1 n2, op_strength_reduction_cases (Oshrlu) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case39: forall c args vl, op_strength_reduction_cases (Ocmp c) (args) (vl) - | op_strength_reduction_case40: forall r1 r2 v1 n2, op_strength_reduction_cases (Omulf) (r1 :: r2 :: nil) (v1 :: F n2 :: nil) - | op_strength_reduction_case41: forall r1 r2 n1 v2, op_strength_reduction_cases (Omulf) (r1 :: r2 :: nil) (F n1 :: v2 :: nil) - | op_strength_reduction_case42: forall r1 r2 v1 n2, op_strength_reduction_cases (Omulfs) (r1 :: r2 :: nil) (v1 :: FS n2 :: nil) - | op_strength_reduction_case43: forall r1 r2 n1 v2, op_strength_reduction_cases (Omulfs) (r1 :: r2 :: nil) (FS n1 :: v2 :: nil) - | op_strength_reduction_default: forall (op: operation) (args: list reg) (vl: list aval), op_strength_reduction_cases op args vl. - -Definition op_strength_reduction_match (op: operation) (args: list reg) (vl: list aval) := - match op as zz1, args as zz2, vl as zz3 return op_strength_reduction_cases zz1 zz2 zz3 with - | Ocast8signed, r1 :: nil, v1 :: nil => op_strength_reduction_case1 r1 v1 - | Ocast16signed, r1 :: nil, v1 :: nil => op_strength_reduction_case2 r1 v1 - | Oadd, r1 :: r2 :: nil, I n1 :: v2 :: nil => op_strength_reduction_case3 r1 r2 n1 v2 - | Oadd, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case4 r1 r2 v1 n2 - | Osub, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case5 r1 r2 v1 n2 - | Omul, r1 :: r2 :: nil, I n1 :: v2 :: nil => op_strength_reduction_case6 r1 r2 n1 v2 - | Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case7 r1 r2 v1 n2 - | Odiv, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case8 r1 r2 v1 n2 - | Odivu, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case9 r1 r2 v1 n2 - | Omodu, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case10 r1 r2 v1 n2 - | Oand, r1 :: r2 :: nil, I n1 :: v2 :: nil => op_strength_reduction_case11 r1 r2 n1 v2 - | Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case12 r1 r2 v1 n2 - | Oandimm n, r1 :: nil, v1 :: nil => op_strength_reduction_case13 n r1 v1 - | Oor, r1 :: r2 :: nil, I n1 :: v2 :: nil => op_strength_reduction_case14 r1 r2 n1 v2 - | Oor, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case15 r1 r2 v1 n2 - | Oxor, r1 :: r2 :: nil, I n1 :: v2 :: nil => op_strength_reduction_case16 r1 r2 n1 v2 - | Oxor, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case17 r1 r2 v1 n2 - | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case18 r1 r2 v1 n2 - | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case19 r1 r2 v1 n2 - | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case20 r1 r2 v1 n2 - | Oaddl, r1 :: r2 :: nil, L n1 :: v2 :: nil => op_strength_reduction_case21 r1 r2 n1 v2 - | Oaddl, r1 :: r2 :: nil, v1 :: L n2 :: nil => op_strength_reduction_case22 r1 r2 v1 n2 - | Osubl, r1 :: r2 :: nil, v1 :: L n2 :: nil => op_strength_reduction_case23 r1 r2 v1 n2 - | Omull, r1 :: r2 :: nil, L n1 :: v2 :: nil => op_strength_reduction_case24 r1 r2 n1 v2 - | Omull, r1 :: r2 :: nil, v1 :: L n2 :: nil => op_strength_reduction_case25 r1 r2 v1 n2 - | Odivl, r1 :: r2 :: nil, v1 :: L n2 :: nil => op_strength_reduction_case26 r1 r2 v1 n2 - | Odivlu, r1 :: r2 :: nil, v1 :: L n2 :: nil => op_strength_reduction_case27 r1 r2 v1 n2 - | Omodlu, r1 :: r2 :: nil, v1 :: L n2 :: nil => op_strength_reduction_case28 r1 r2 v1 n2 - | Oandl, r1 :: r2 :: nil, L n1 :: v2 :: nil => op_strength_reduction_case29 r1 r2 n1 v2 - | Oandl, r1 :: r2 :: nil, v1 :: L n2 :: nil => op_strength_reduction_case30 r1 r2 v1 n2 - | Oandlimm n, r1 :: nil, v1 :: nil => op_strength_reduction_case31 n r1 v1 - | Oorl, r1 :: r2 :: nil, L n1 :: v2 :: nil => op_strength_reduction_case32 r1 r2 n1 v2 - | Oorl, r1 :: r2 :: nil, v1 :: L n2 :: nil => op_strength_reduction_case33 r1 r2 v1 n2 - | Oxorl, r1 :: r2 :: nil, L n1 :: v2 :: nil => op_strength_reduction_case34 r1 r2 n1 v2 - | Oxorl, r1 :: r2 :: nil, v1 :: L n2 :: nil => op_strength_reduction_case35 r1 r2 v1 n2 - | Oshll, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case36 r1 r2 v1 n2 - | Oshrl, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case37 r1 r2 v1 n2 - | Oshrlu, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case38 r1 r2 v1 n2 - | Ocmp c, args, vl => op_strength_reduction_case39 c args vl - | Omulf, r1 :: r2 :: nil, v1 :: F n2 :: nil => op_strength_reduction_case40 r1 r2 v1 n2 - | Omulf, r1 :: r2 :: nil, F n1 :: v2 :: nil => op_strength_reduction_case41 r1 r2 n1 v2 - | Omulfs, r1 :: r2 :: nil, v1 :: FS n2 :: nil => op_strength_reduction_case42 r1 r2 v1 n2 - | Omulfs, r1 :: r2 :: nil, FS n1 :: v2 :: nil => op_strength_reduction_case43 r1 r2 n1 v2 - | op, args, vl => op_strength_reduction_default op args vl - end. - -Definition op_strength_reduction (op: operation) (args: list reg) (vl: list aval) := - match op_strength_reduction_match op args vl with - | op_strength_reduction_case1 r1 v1 => (* Ocast8signed, r1 :: nil, v1 :: nil *) - make_cast8signed r1 v1 - | op_strength_reduction_case2 r1 v1 => (* Ocast16signed, r1 :: nil, v1 :: nil *) - make_cast16signed r1 v1 - | op_strength_reduction_case3 r1 r2 n1 v2 => (* Oadd, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - make_addimm n1 r2 - | op_strength_reduction_case4 r1 r2 v1 n2 => (* Oadd, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_addimm n2 r1 - | op_strength_reduction_case5 r1 r2 v1 n2 => (* Osub, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_addimm (Int.neg n2) r1 - | op_strength_reduction_case6 r1 r2 n1 v2 => (* Omul, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - make_mulimm n1 r2 r1 - | op_strength_reduction_case7 r1 r2 v1 n2 => (* Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_mulimm n2 r1 r2 - | op_strength_reduction_case8 r1 r2 v1 n2 => (* Odiv, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_divimm n2 r1 r2 - | op_strength_reduction_case9 r1 r2 v1 n2 => (* Odivu, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_divuimm n2 r1 r2 - | op_strength_reduction_case10 r1 r2 v1 n2 => (* Omodu, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_moduimm n2 r1 r2 - | op_strength_reduction_case11 r1 r2 n1 v2 => (* Oand, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - make_andimm n1 r2 v2 - | op_strength_reduction_case12 r1 r2 v1 n2 => (* Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_andimm n2 r1 v1 - | op_strength_reduction_case13 n r1 v1 => (* Oandimm n, r1 :: nil, v1 :: nil *) - make_andimm n r1 v1 - | op_strength_reduction_case14 r1 r2 n1 v2 => (* Oor, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - make_orimm n1 r2 - | op_strength_reduction_case15 r1 r2 v1 n2 => (* Oor, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_orimm n2 r1 - | op_strength_reduction_case16 r1 r2 n1 v2 => (* Oxor, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - make_xorimm n1 r2 - | op_strength_reduction_case17 r1 r2 v1 n2 => (* Oxor, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_xorimm n2 r1 - | op_strength_reduction_case18 r1 r2 v1 n2 => (* Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_shlimm n2 r1 r2 - | op_strength_reduction_case19 r1 r2 v1 n2 => (* Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_shrimm n2 r1 r2 - | op_strength_reduction_case20 r1 r2 v1 n2 => (* Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_shruimm n2 r1 r2 - | op_strength_reduction_case21 r1 r2 n1 v2 => (* Oaddl, r1 :: r2 :: nil, L n1 :: v2 :: nil *) - make_addlimm n1 r2 - | op_strength_reduction_case22 r1 r2 v1 n2 => (* Oaddl, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - make_addlimm n2 r1 - | op_strength_reduction_case23 r1 r2 v1 n2 => (* Osubl, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - make_addlimm (Int64.neg n2) r1 - | op_strength_reduction_case24 r1 r2 n1 v2 => (* Omull, r1 :: r2 :: nil, L n1 :: v2 :: nil *) - make_mullimm n1 r2 r1 - | op_strength_reduction_case25 r1 r2 v1 n2 => (* Omull, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - make_mullimm n2 r1 r2 - | op_strength_reduction_case26 r1 r2 v1 n2 => (* Odivl, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - make_divlimm n2 r1 r2 - | op_strength_reduction_case27 r1 r2 v1 n2 => (* Odivlu, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - make_divluimm n2 r1 r2 - | op_strength_reduction_case28 r1 r2 v1 n2 => (* Omodlu, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - make_modluimm n2 r1 r2 - | op_strength_reduction_case29 r1 r2 n1 v2 => (* Oandl, r1 :: r2 :: nil, L n1 :: v2 :: nil *) - make_andlimm n1 r2 v2 - | op_strength_reduction_case30 r1 r2 v1 n2 => (* Oandl, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - make_andlimm n2 r1 v1 - | op_strength_reduction_case31 n r1 v1 => (* Oandlimm n, r1 :: nil, v1 :: nil *) - make_andlimm n r1 v1 - | op_strength_reduction_case32 r1 r2 n1 v2 => (* Oorl, r1 :: r2 :: nil, L n1 :: v2 :: nil *) - make_orlimm n1 r2 - | op_strength_reduction_case33 r1 r2 v1 n2 => (* Oorl, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - make_orlimm n2 r1 - | op_strength_reduction_case34 r1 r2 n1 v2 => (* Oxorl, r1 :: r2 :: nil, L n1 :: v2 :: nil *) - make_xorlimm n1 r2 - | op_strength_reduction_case35 r1 r2 v1 n2 => (* Oxorl, r1 :: r2 :: nil, v1 :: L n2 :: nil *) - make_xorlimm n2 r1 - | op_strength_reduction_case36 r1 r2 v1 n2 => (* Oshll, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_shllimm n2 r1 r2 - | op_strength_reduction_case37 r1 r2 v1 n2 => (* Oshrl, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_shrlimm n2 r1 r2 - | op_strength_reduction_case38 r1 r2 v1 n2 => (* Oshrlu, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_shrluimm n2 r1 r2 - | op_strength_reduction_case39 c args vl => (* Ocmp c, args, vl *) - make_cmp c args vl - | op_strength_reduction_case40 r1 r2 v1 n2 => (* Omulf, r1 :: r2 :: nil, v1 :: F n2 :: nil *) - make_mulfimm n2 r1 r1 r2 - | op_strength_reduction_case41 r1 r2 n1 v2 => (* Omulf, r1 :: r2 :: nil, F n1 :: v2 :: nil *) - make_mulfimm n1 r2 r1 r2 - | op_strength_reduction_case42 r1 r2 v1 n2 => (* Omulfs, r1 :: r2 :: nil, v1 :: FS n2 :: nil *) - make_mulfsimm n2 r1 r1 r2 - | op_strength_reduction_case43 r1 r2 n1 v2 => (* Omulfs, r1 :: r2 :: nil, FS n1 :: v2 :: nil *) - make_mulfsimm n1 r2 r1 r2 - | op_strength_reduction_default op args vl => - (op, args) - end. - - -(** Original definition: -<< -Nondetfunction addr_strength_reduction - (addr: addressing) (args: list reg) (vl: list aval) := - match addr, args, vl with - | Aindexed n, r1 :: nil, Ptr(Gl symb n1) :: nil => - if Archi.pic_code tt - then (addr, args) - else (Aglobal symb (Ptrofs.add n1 n), nil) - | Aindexed n, r1 :: nil, Ptr(Stk n1) :: nil => - (Ainstack (Ptrofs.add n1 n), nil) - | _, _, _ => - (addr, args) - end. ->> -*) - -Inductive addr_strength_reduction_cases: forall (addr: addressing) (args: list reg) (vl: list aval), Type := - | addr_strength_reduction_case1: forall n r1 symb n1, addr_strength_reduction_cases (Aindexed n) (r1 :: nil) (Ptr(Gl symb n1) :: nil) - | addr_strength_reduction_case2: forall n r1 n1, addr_strength_reduction_cases (Aindexed n) (r1 :: nil) (Ptr(Stk n1) :: nil) - | addr_strength_reduction_default: forall (addr: addressing) (args: list reg) (vl: list aval), addr_strength_reduction_cases addr args vl. - -Definition addr_strength_reduction_match (addr: addressing) (args: list reg) (vl: list aval) := - match addr as zz1, args as zz2, vl as zz3 return addr_strength_reduction_cases zz1 zz2 zz3 with - | Aindexed n, r1 :: nil, Ptr(Gl symb n1) :: nil => addr_strength_reduction_case1 n r1 symb n1 - | Aindexed n, r1 :: nil, Ptr(Stk n1) :: nil => addr_strength_reduction_case2 n r1 n1 - | addr, args, vl => addr_strength_reduction_default addr args vl - end. - -Definition addr_strength_reduction (addr: addressing) (args: list reg) (vl: list aval) := - match addr_strength_reduction_match addr args vl with - | addr_strength_reduction_case1 n r1 symb n1 => (* Aindexed n, r1 :: nil, Ptr(Gl symb n1) :: nil *) - if Archi.pic_code tt then (addr, args) else (Aglobal symb (Ptrofs.add n1 n), nil) - | addr_strength_reduction_case2 n r1 n1 => (* Aindexed n, r1 :: nil, Ptr(Stk n1) :: nil *) - (Ainstack (Ptrofs.add n1 n), nil) - | addr_strength_reduction_default addr args vl => - (addr, args) - end. - - diff --git a/mppa_k1c/Machregsaux.ml b/mppa_k1c/Machregsaux.ml index 473e0602..9c4175ed 100644 --- a/mppa_k1c/Machregsaux.ml +++ b/mppa_k1c/Machregsaux.ml @@ -31,3 +31,8 @@ let register_by_name s = Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s) let can_reserve_register r = Conventions1.is_callee_save r + +let class_of_type = function + | AST.Tint | AST.Tlong + | AST.Tfloat | AST.Tsingle -> 0 + | AST.Tany32 | AST.Tany64 -> assert false diff --git a/mppa_k1c/Machregsaux.mli b/mppa_k1c/Machregsaux.mli index 9404568d..d7117c21 100644 --- a/mppa_k1c/Machregsaux.mli +++ b/mppa_k1c/Machregsaux.mli @@ -16,3 +16,5 @@ val name_of_register: Machregs.mreg -> string option val register_by_name: string -> Machregs.mreg option val is_scratch_register: string -> bool val can_reserve_register: Machregs.mreg -> bool + +val class_of_type: AST.typ -> int diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 2c39e342..56b00c7e 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -222,7 +222,6 @@ let basic_rec i = | Pnop -> { inst = "nop"; write_locs = []; read_locs = []; imm = None ; is_control = false} let expand_rec = function - | Pdiv | Pdivu -> { inst = "Pdiv"; write_locs = [Reg (IR GPR0)]; read_locs = [Reg (IR GPR0); Reg (IR GPR1)]; imm = None; is_control = true } | Pbuiltin _ -> raise OpaqueInstruction let ctl_flow_rec = function diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index 3a17ab17..0c3618d7 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -21,6 +21,7 @@ Require Import Coqlib. Require Import Compopts. Require Import AST Integers Floats. Require Import Op CminorSel. +Require Import OpHelpers. Require Import SelectOp SplitLong. Local Open Scope cminorsel_scope. diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 4723278a..79187338 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -21,6 +21,7 @@ Require Import String Coqlib Maps Integers Floats Errors. Require Archi. Require Import AST Values Memory Globalenvs Events. Require Import Cminor Op CminorSel. +Require Import OpHelpers OpHelpersproof. Require Import SelectOp SelectOpproof SplitLong SplitLongproof. Require Import SelectLong. diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 19712d2f..f6605c11 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -50,6 +50,7 @@ Require Import Integers. Require Import Floats. Require Import Op. Require Import CminorSel. +Require Import OpHelpers. Local Open Scope cminorsel_scope. @@ -57,44 +58,6 @@ 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. -Definition sig_ff_f := mksignature (Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default. -Definition sig_ss_s := mksignature (Tsingle :: Tsingle :: nil) (Some Tsingle) 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 *) - f64_div: ident; (**float division*) - f32_div: ident; (**float division*) -}. Context {hf: helper_functions}. diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index a4a5f72b..89af39ee 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -30,76 +30,13 @@ Require Import Op. Require Import CminorSel. Require Import SelectOp. Require Import Events. +Require Import OpHelpers. +Require Import OpHelpersproof. 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.divs x y = Some z -> external_implements "__compcert_i32_sdiv" sig_ii_i (x::y::nil) z) - /\ (forall x y z, Val.divu x y = Some z -> external_implements "__compcert_i32_udiv" sig_ii_i (x::y::nil) z) - /\ (forall x y z, Val.mods x y = Some z -> external_implements "__compcert_i32_smod" sig_ii_i (x::y::nil) z) - /\ (forall x y z, Val.modu x y = Some z -> external_implements "__compcert_i32_umod" sig_ii_i (x::y::nil) z) - /\ (forall x y z, Val.divfs x y = z -> external_implements "__compcert_f32_div" sig_ss_s (x::y::nil) z) - /\ (forall x y z, Val.divf x y = z -> external_implements "__compcert_f64_div" sig_ff_f (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 - /\ helper_declared p f32_div "__compcert_f32_div" sig_ss_s - /\ helper_declared p f64_div "__compcert_f64_div" sig_ff_f -. - (** * Useful lemmas and tactics *) (** The following are trivial lemmas and custom tactics that help @@ -158,7 +95,7 @@ Variable m: mem. (* Helper lemmas - from SplitLongproof.v *) -Ltac UseHelper := decompose [Logic.and] i64_helpers_correct; eauto. +Ltac UseHelper := decompose [Logic.and] arith_helpers_correct; eauto. Ltac DeclHelper := red in HELPERS; decompose [Logic.and] HELPERS; eauto. Lemma eval_helper: diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index d4e2afc9..69824852 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -258,10 +258,6 @@ module Target (*: TARGET*) = fprintf oc " goto %a\n" symbol s | Pigoto(rs) -> fprintf oc " igoto %a\n" ireg rs - | Pdiv -> - fprintf oc " call __divdi3\n" - | Pdivu -> - fprintf oc " call __udivdi3\n" | Pj_l(s) -> fprintf oc " goto %a\n" print_label s | Pcb (bt, r, lbl) | Pcbu (bt, r, lbl) -> diff --git a/powerpc/Machregsaux.ml b/powerpc/Machregsaux.ml index 664f71a0..0b0d4548 100644 --- a/powerpc/Machregsaux.ml +++ b/powerpc/Machregsaux.ml @@ -33,3 +33,8 @@ let register_by_name s = let can_reserve_register r = List.mem r Conventions1.int_callee_save_regs || List.mem r Conventions1.float_callee_save_regs + +let class_of_type = function + | AST.Tint | AST.Tlong -> 0 + | AST.Tfloat | AST.Tsingle -> 1 + | AST.Tany32 | AST.Tany64 -> assert false diff --git a/powerpc/Machregsaux.mli b/powerpc/Machregsaux.mli index 9404568d..d7117c21 100644 --- a/powerpc/Machregsaux.mli +++ b/powerpc/Machregsaux.mli @@ -16,3 +16,5 @@ val name_of_register: Machregs.mreg -> string option val register_by_name: string -> Machregs.mreg option val is_scratch_register: string -> bool val can_reserve_register: Machregs.mreg -> bool + +val class_of_type: AST.typ -> int diff --git a/powerpc/SelectLong.vp b/powerpc/SelectLong.vp index 5f13774b..e4274ba5 100644 --- a/powerpc/SelectLong.vp +++ b/powerpc/SelectLong.vp @@ -16,7 +16,7 @@ Require Import Coqlib. Require Import Compopts. Require Import AST Integers Floats. Require Import Op CminorSel. -Require Import SelectOp SplitLong. +Require Import OpHelpers SelectOp SplitLong. Local Open Scope cminorsel_scope. Local Open Scope string_scope. diff --git a/powerpc/SelectLongproof.v b/powerpc/SelectLongproof.v index a214d131..b4e48596 100644 --- a/powerpc/SelectLongproof.v +++ b/powerpc/SelectLongproof.v @@ -16,6 +16,7 @@ Require Import String Coqlib Maps Integers Floats Errors. Require Archi. Require Import AST Values Memory Globalenvs Events. Require Import Cminor Op CminorSel. +Require Import OpHelpers OpHelpersproof. Require Import SelectOp SelectOpproof SplitLong SplitLongproof. Require Import SelectLong. diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index d2ca408a..478ce251 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -43,6 +43,7 @@ Require Import Integers. Require Import Floats. Require Import Op. Require Import CminorSel. +Require Import OpHelpers. Local Open Scope cminorsel_scope. @@ -552,3 +553,10 @@ Nondetfunction builtin_arg (e: expr) := | Eop Oadd (e1:::e2:::Enil) => BA_addptr (BA e1) (BA e2) | _ => BA e end. + +(* floats *) +Definition divf_base (e1: expr) (e2: expr) := + Eop Odivf (e1 ::: e2 ::: Enil). + +Definition divfs_base (e1: expr) (e2: expr) := + Eop Odivfs (e1 ::: e2 ::: Enil). diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 5f87d9b9..00b91e70 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -25,6 +25,8 @@ Require Import Cminor. Require Import Op. Require Import CminorSel. Require Import SelectOp. +Require Import OpHelpers. +Require Import OpHelpersproof. Local Open Scope cminorsel_scope. Local Transparent Archi.ptr64. @@ -77,8 +79,10 @@ Ltac TrivialExists := (** * Correctness of the smart constructors *) Section CMCONSTR. - -Variable ge: genv. +Variable prog: program. +Variable hf: helper_functions. +Hypothesis HELPERS: helper_functions_declared prog hf. +Let ge := Genv.globalenv prog. Variable sp: val. Variable e: env. Variable m: mem. @@ -1044,4 +1048,24 @@ Proof. - constructor; auto. Qed. +(* floating-point division without HELPERS *) +Theorem eval_divf_base: + forall le a b x y, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + exists v, eval_expr ge sp e m le (divf_base a b) v /\ Val.lessdef (Val.divf x y) v. +Proof. + intros; unfold divf_base. + TrivialExists. +Qed. + +Theorem eval_divfs_base: + forall le a b x y, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + exists v, eval_expr ge sp e m le (divfs_base a b) v /\ Val.lessdef (Val.divfs x y) v. +Proof. + intros; unfold divfs_base. + TrivialExists. +Qed. End CMCONSTR. diff --git a/riscV/Machregsaux.ml b/riscV/Machregsaux.ml index 473e0602..07097eaf 100644 --- a/riscV/Machregsaux.ml +++ b/riscV/Machregsaux.ml @@ -31,3 +31,8 @@ let register_by_name s = Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s) let can_reserve_register r = Conventions1.is_callee_save r + +let class_of_type = function + | AST.Tint | AST.Tlong -> 0 + | AST.Tfloat | AST.Tsingle -> 1 + | AST.Tany32 | AST.Tany64 -> assert false diff --git a/riscV/Machregsaux.mli b/riscV/Machregsaux.mli index 9404568d..d7117c21 100644 --- a/riscV/Machregsaux.mli +++ b/riscV/Machregsaux.mli @@ -16,3 +16,5 @@ val name_of_register: Machregs.mreg -> string option val register_by_name: string -> Machregs.mreg option val is_scratch_register: string -> bool val can_reserve_register: Machregs.mreg -> bool + +val class_of_type: AST.typ -> int diff --git a/riscV/SelectLong.vp b/riscV/SelectLong.vp index b3e07bf5..0ccc4725 100644 --- a/riscV/SelectLong.vp +++ b/riscV/SelectLong.vp @@ -21,7 +21,7 @@ Require Import Coqlib. Require Import Compopts. Require Import AST Integers Floats. Require Import Op CminorSel. -Require Import SelectOp SplitLong. +Require Import OpHelpers SelectOp SplitLong. Local Open Scope cminorsel_scope. Local Open Scope string_scope. diff --git a/riscV/SelectLongproof.v b/riscV/SelectLongproof.v index 78a1935d..d47b6d64 100644 --- a/riscV/SelectLongproof.v +++ b/riscV/SelectLongproof.v @@ -21,6 +21,7 @@ Require Import String Coqlib Maps Integers Floats Errors. Require Archi. Require Import AST Values Memory Globalenvs Events. Require Import Cminor Op CminorSel. +Require Import OpHelpers OpHelpersproof. Require Import SelectOp SelectOpproof SplitLong SplitLongproof. Require Import SelectLong. diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp index bb8af2ed..181b9d05 100644 --- a/riscV/SelectOp.vp +++ b/riscV/SelectOp.vp @@ -448,3 +448,10 @@ Nondetfunction builtin_arg (e: expr) := if Archi.ptr64 then BA_addptr (BA e1) (BA_long n) else BA e | _ => BA e end. + +(* floats *) +Definition divf_base (e1: expr) (e2: expr) := + Eop Odivf (e1 ::: e2 ::: Enil). + +Definition divfs_base (e1: expr) (e2: expr) := + Eop Odivfs (e1 ::: e2 ::: Enil). diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v index 90f077db..9966305c 100644 --- a/riscV/SelectOpproof.v +++ b/riscV/SelectOpproof.v @@ -29,6 +29,8 @@ Require Import Cminor. Require Import Op. Require Import CminorSel. Require Import SelectOp. +Require Import OpHelpers. +Require Import OpHelpersproof. Local Open Scope cminorsel_scope. @@ -80,8 +82,10 @@ Ltac TrivialExists := (** * Correctness of the smart constructors *) Section CMCONSTR. - -Variable ge: genv. +Variable prog: program. +Variable hf: helper_functions. +Hypothesis HELPERS: helper_functions_declared prog hf. +Let ge := Genv.globalenv prog. Variable sp: val. Variable e: env. Variable m: mem. @@ -922,4 +926,25 @@ Proof. - constructor; auto. Qed. + +(* floating-point division without HELPERS *) +Theorem eval_divf_base: + forall le a b x y, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + exists v, eval_expr ge sp e m le (divf_base a b) v /\ Val.lessdef (Val.divf x y) v. +Proof. + intros; unfold divf_base. + TrivialExists. +Qed. + +Theorem eval_divfs_base: + forall le a b x y, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + exists v, eval_expr ge sp e m le (divfs_base a b) v /\ Val.lessdef (Val.divfs x y) v. +Proof. + intros; unfold divfs_base. + TrivialExists. +Qed. End CMCONSTR. diff --git a/test/monniaux/mbedtls/mbedtls_Kalray.patch b/test/monniaux/mbedtls/mbedtls_Kalray.patch index 25cd5922..594ee7fa 100644 --- a/test/monniaux/mbedtls/mbedtls_Kalray.patch +++ b/test/monniaux/mbedtls/mbedtls_Kalray.patch @@ -39,56 +39,6 @@ index f89bf9604..9f8a4faeb 100644 /** * \def MBEDTLS_VERSION_C -diff --git a/library/bignum.c b/library/bignum.c -index 87015af0c..a2bad7b84 100644 ---- a/library/bignum.c -+++ b/library/bignum.c -@@ -1696,6 +1696,8 @@ cleanup: - return( ret ); - } - -+#define INT_DIV(x,y) ((x) / (y)) -+ - /* - * Modulo: r = A mod b - */ -@@ -1734,12 +1736,12 @@ int mbedtls_mpi_mod_int( mbedtls_mpi_uint *r, const mbedtls_mpi *A, mbedtls_mpi_ - { - x = A->p[i - 1]; - y = ( y << biH ) | ( x >> biH ); -- z = y / b; -+ z = INT_DIV(y, b); - y -= z * b; - - x <<= biH; - y = ( y << biH ) | ( x >> biH ); -- z = y / b; -+ z = INT_DIV(y, b); - y -= z * b; - } - -diff --git a/library/ssl_tls.c b/library/ssl_tls.c -index 8710a5076..e47c859fe 100644 ---- a/library/ssl_tls.c -+++ b/library/ssl_tls.c -@@ -2482,6 +2482,8 @@ static int ssl_decompress_buf( mbedtls_ssl_context *ssl ) - } - #endif /* MBEDTLS_ZLIB_SUPPORT */ - -+#define INT_DIV(x, y) (((long)(x))/(y)) -+ - #if defined(MBEDTLS_SSL_SRV_C) && defined(MBEDTLS_SSL_RENEGOTIATION) - static int ssl_write_hello_request( mbedtls_ssl_context *ssl ); - -@@ -2492,7 +2494,7 @@ static int ssl_resend_hello_request( mbedtls_ssl_context *ssl ) - * timeout if we were using the usual handshake doubling scheme */ - if( ssl->conf->renego_max_records < 0 ) - { -- uint32_t ratio = ssl->conf->hs_timeout_max / ssl->conf->hs_timeout_min + 1; -+ uint32_t ratio = INT_DIV(ssl->conf->hs_timeout_max, ssl->conf->hs_timeout_min + 1); - unsigned char doublings = 1; - - while( ratio != 0 ) diff --git a/tests/suites/helpers.function b/tests/suites/helpers.function index 1255ff4be..103abe9a8 100644 --- a/tests/suites/helpers.function @@ -105,3 +55,16 @@ index 1255ff4be..103abe9a8 100644 #endif /* Type for Hex parameters */ +diff --git a/tests/scripts/run-test-suites.pl b/tests/scripts/run-test-suites.pl +index d0d4046..00cff26 100755 +--- a/tests/scripts/run-test-suites.pl ++++ b/tests/scripts/run-test-suites.pl +@@ -59,7 +59,7 @@ for my $suite (@suites) + if( $verbose ) { + $command .= ' -v'; + } +- my $result = `$command`; ++ my $result = `k1-cluster -- $command`; + + $suite_cases_passed = () = $result =~ /.. PASS/g; + $suite_cases_failed = () = $result =~ /.. FAILED/g; diff --git a/test/mppa/instr/andd.c b/test/mppa/instr/andd.c deleted file mode 100644 index e3221bd7..00000000 --- a/test/mppa/instr/andd.c +++ /dev/null @@ -1,5 +0,0 @@ -#include "framework.h" - -BEGIN_TEST(long long) - c = a&b; -END_TEST64() diff --git a/test/mppa/instr/addw.c b/test/mppa/instr/div32.c index e22024cf..83c3a0e3 100644 --- a/test/mppa/instr/addw.c +++ b/test/mppa/instr/div32.c @@ -1,5 +1,5 @@ #include "framework.h" BEGIN_TEST(int) - c = a+b; + c = a/b; END_TEST32() diff --git a/test/mppa/instr/faddw.c b/test/mppa/instr/divf32.c index e0e635ae..513a3293 100644 --- a/test/mppa/instr/faddw.c +++ b/test/mppa/instr/divf32.c @@ -1,5 +1,5 @@ #include "framework.h" BEGIN_TEST(float) - c = ((float)a + (float)b); + c = a / b; END_TESTF32() diff --git a/test/mppa/instr/faddd.c b/test/mppa/instr/divf64.c index 35b7fc92..0dd23826 100644 --- a/test/mppa/instr/faddd.c +++ b/test/mppa/instr/divf64.c @@ -1,5 +1,5 @@ #include "framework.h" BEGIN_TEST(double) - c = ((double)a + (double)b); + c = a / b; END_TESTF64() diff --git a/test/mppa/instr/cast_U32_S64.c b/test/mppa/instr/divu32.c index 6f9cd059..1fe196c4 100644 --- a/test/mppa/instr/cast_U32_S64.c +++ b/test/mppa/instr/divu32.c @@ -2,6 +2,6 @@ BEGIN_TEST(unsigned int) { - c = (long long) a; + c = a/b; } END_TEST32() diff --git a/test/mppa/instr/f32.c b/test/mppa/instr/f32.c new file mode 100644 index 00000000..7e304aeb --- /dev/null +++ b/test/mppa/instr/f32.c @@ -0,0 +1,8 @@ +#include "framework.h" + +BEGIN_TEST(float) + c = ((float)a + (float)b); + c += ((float)a * (float)b); + c += (-(float)a); + c += ((float)a - (float)b); +END_TESTF32() diff --git a/test/mppa/instr/f64.c b/test/mppa/instr/f64.c new file mode 100644 index 00000000..be8094c9 --- /dev/null +++ b/test/mppa/instr/f64.c @@ -0,0 +1,8 @@ +#include "framework.h" + +BEGIN_TEST(double) + c = ((double)a + (double)b); + c += ((double)a * (double)b); + c += (-(double)a); + c += ((double)a - (double)b); +END_TESTF64() diff --git a/test/mppa/instr/i32.c b/test/mppa/instr/i32.c new file mode 100644 index 00000000..c48531b1 --- /dev/null +++ b/test/mppa/instr/i32.c @@ -0,0 +1,87 @@ +#include "framework.h" + +int sum(int a, int b){ + return a+b; +} + +int make(int a){ + return a; +} + +int tailsum(int a, int b){ + return make(a+b); +} + +float int2float(int v){ + return v; +} + +BEGIN_TEST(int) + c = a+b; + c += a&b; + + if ((a & 0x1) == 1) + c += 1; + else + c += 2; + + if (a & 0x1 == 0) + c += 4; + else + c += 8; + + b = !(a & 0x01); + if (!b) + c += 16; + else + c += 32; + + c += sum(make(a), make(b)); + c += (long long) a; + + if (0 > (a & 0x1) - 1) + c += 64; + else + c += 128; + + if (0 >= (a & 0x1)) + c += 256; + else + c += 512; + + if ((a & 0x1) > 0) + c += 1024; + else + c += 2048; + + if ((a & 0x1) - 1 >= 0) + c += 4096; + else + c += 8192; + + c += ((a & 0x1) == (b & 0x1)); + c += (a > b); + c += (a <= b); + c += (a < b); + c += (a + b) / 2; + c += (int) int2float(a) + (int) int2float(b) + (int) int2float(42.3); + + int j; + for (j = 0 ; j < 10 ; j++) + c += a; + int k; + for (k = 0 ; k < (b & 0x8) ; k++) + c += a; + + char s[] = "Tome and Cherry at the playa\n"; + c += s[(a & (sizeof(s)-1))]; + + unsigned char s2[] = "Tim is sorry at the playa\n"; + c += s2[a & (sizeof(s) - 1)]; + + c += a*b; + c += a-b; + c += a << (b & 0x8); + + c += sum(a, b); +END_TEST32() diff --git a/test/mppa/instr/i64.c b/test/mppa/instr/i64.c new file mode 100644 index 00000000..00eb159d --- /dev/null +++ b/test/mppa/instr/i64.c @@ -0,0 +1,107 @@ +#include "framework.h" + +long long sum(long long a, long long b){ + return a+b; +} + +long long diff(long long a, long long b){ + return a-b; +} + +long long mul(long long a, long long b){ + return a*b; +} + +long long make(long long a){ + return a; +} + +long long random_op(long long a, long long b){ + long long d = 3; + long long (*op)(long long, long long); + + if (a % d == 0) + op = sum; + else if (a % d == 1) + op = diff; + else + op = mul; + + return op(a, b); +} + +double long2double(long v){ + return v; +} + +BEGIN_TEST(long long) + c = a&b; + c += a*b; + c += -a; + c += a | b; + c += a-b; + c += a >> (b & 0x8LL); + c += a >> (b & 0x8ULL); + c += a % b; + + long long d = 3; + long long (*op)(long long, long long); + + if (a % d == 0) + op = sum; + else if (a % d == 1) + op = diff; + else + op = mul; + + c += op(make(a), make(b)); + c += random_op(a, b); + c += a/b; + c += a^b; + c += (unsigned int) a; + + if (0 != (a & 0x1LL)) + c += 1; + else + c += 2; + + if (0 > (a & 0x1LL)) + c += 4; + else + c += 8; + + if (0 >= (a & 0x1LL) - 1) + c += 16; + else + c += 32; + + if (a & 0x1LL > 0) + c += 64; + else + c += 128; + + if ((a & 0x1LL) - 1 >= 0) + c += 256; + else + c += 512; + + if (0 == (a & 0x1LL)) + c += 1024; + else + c += 2048; + + c += ((a & 0x1LL) == (b & 0x1LL)); + c += (a >= b); + c += (a > b); + c += (a <= b); + c += (a < b); + c += (long) long2double(a) + (long) long2double(b) + (long) long2double(42.3); + + int j; + + for (j = 0 ; j < (b & 0x8LL) ; j++) + c += a; + + c += ((a & 0x1LL) == (b & 0x1LL)); + +END_TEST64() diff --git a/test/mppa/instr/andw.c b/test/mppa/instr/individual/andw.c index 799dc7fb..799dc7fb 100644 --- a/test/mppa/instr/andw.c +++ b/test/mppa/instr/individual/andw.c diff --git a/test/mppa/instr/branch.c b/test/mppa/instr/individual/branch.c index c9937e31..c9937e31 100644 --- a/test/mppa/instr/branch.c +++ b/test/mppa/instr/individual/branch.c diff --git a/test/mppa/instr/branchz.c b/test/mppa/instr/individual/branchz.c index d3e021b5..d3e021b5 100644 --- a/test/mppa/instr/branchz.c +++ b/test/mppa/instr/individual/branchz.c diff --git a/test/mppa/instr/branchzu.c b/test/mppa/instr/individual/branchzu.c index d0169174..d0169174 100644 --- a/test/mppa/instr/branchzu.c +++ b/test/mppa/instr/individual/branchzu.c diff --git a/test/mppa/instr/call.c b/test/mppa/instr/individual/call.c index ba2ec323..ba2ec323 100644 --- a/test/mppa/instr/call.c +++ b/test/mppa/instr/individual/call.c diff --git a/test/mppa/instr/cast_S32_S64.c b/test/mppa/instr/individual/cast_S32_S64.c index 09c97e00..09c97e00 100644 --- a/test/mppa/instr/cast_S32_S64.c +++ b/test/mppa/instr/individual/cast_S32_S64.c diff --git a/test/mppa/instr/cast_S64_U32.c b/test/mppa/instr/individual/cast_S64_U32.c index 2d9dc723..2d9dc723 100644 --- a/test/mppa/instr/cast_S64_U32.c +++ b/test/mppa/instr/individual/cast_S64_U32.c diff --git a/test/mppa/instr/cb.deqz.c b/test/mppa/instr/individual/cb.deqz.c index 6da2ab07..6da2ab07 100644 --- a/test/mppa/instr/cb.deqz.c +++ b/test/mppa/instr/individual/cb.deqz.c diff --git a/test/mppa/instr/cb.dgez.c b/test/mppa/instr/individual/cb.dgez.c index 7bef25ad..7bef25ad 100644 --- a/test/mppa/instr/cb.dgez.c +++ b/test/mppa/instr/individual/cb.dgez.c diff --git a/test/mppa/instr/cb.dgtz.c b/test/mppa/instr/individual/cb.dgtz.c index 1a43fb1f..1a43fb1f 100644 --- a/test/mppa/instr/cb.dgtz.c +++ b/test/mppa/instr/individual/cb.dgtz.c diff --git a/test/mppa/instr/cb.dlez.c b/test/mppa/instr/individual/cb.dlez.c index 2fb97939..2fb97939 100644 --- a/test/mppa/instr/cb.dlez.c +++ b/test/mppa/instr/individual/cb.dlez.c diff --git a/test/mppa/instr/cb.dltz.c b/test/mppa/instr/individual/cb.dltz.c index a431d5d0..a431d5d0 100644 --- a/test/mppa/instr/cb.dltz.c +++ b/test/mppa/instr/individual/cb.dltz.c diff --git a/test/mppa/instr/cb.dnez.c b/test/mppa/instr/individual/cb.dnez.c index 44516cbe..44516cbe 100644 --- a/test/mppa/instr/cb.dnez.c +++ b/test/mppa/instr/individual/cb.dnez.c diff --git a/test/mppa/instr/cb.wgez.c b/test/mppa/instr/individual/cb.wgez.c index 5779ad92..5779ad92 100644 --- a/test/mppa/instr/cb.wgez.c +++ b/test/mppa/instr/individual/cb.wgez.c diff --git a/test/mppa/instr/cb.wgtz.c b/test/mppa/instr/individual/cb.wgtz.c index abb695bd..abb695bd 100644 --- a/test/mppa/instr/cb.wgtz.c +++ b/test/mppa/instr/individual/cb.wgtz.c diff --git a/test/mppa/instr/cb.wlez.c b/test/mppa/instr/individual/cb.wlez.c index 3a2e08c1..3a2e08c1 100644 --- a/test/mppa/instr/cb.wlez.c +++ b/test/mppa/instr/individual/cb.wlez.c diff --git a/test/mppa/instr/cb.wltz.c b/test/mppa/instr/individual/cb.wltz.c index 5d52c72a..5d52c72a 100644 --- a/test/mppa/instr/cb.wltz.c +++ b/test/mppa/instr/individual/cb.wltz.c diff --git a/test/mppa/instr/compd.eq.c b/test/mppa/instr/individual/compd.eq.c index 4fe8de2a..4fe8de2a 100644 --- a/test/mppa/instr/compd.eq.c +++ b/test/mppa/instr/individual/compd.eq.c diff --git a/test/mppa/instr/compd.geu.c b/test/mppa/instr/individual/compd.geu.c index fccf0804..fccf0804 100644 --- a/test/mppa/instr/compd.geu.c +++ b/test/mppa/instr/individual/compd.geu.c diff --git a/test/mppa/instr/compd.gt.c b/test/mppa/instr/individual/compd.gt.c index b9901436..b9901436 100644 --- a/test/mppa/instr/compd.gt.c +++ b/test/mppa/instr/individual/compd.gt.c diff --git a/test/mppa/instr/compd.le.c b/test/mppa/instr/individual/compd.le.c index 6fa0f103..6fa0f103 100644 --- a/test/mppa/instr/compd.le.c +++ b/test/mppa/instr/individual/compd.le.c diff --git a/test/mppa/instr/compd.leu.c b/test/mppa/instr/individual/compd.leu.c index 1ad18281..1ad18281 100644 --- a/test/mppa/instr/compd.leu.c +++ b/test/mppa/instr/individual/compd.leu.c diff --git a/test/mppa/instr/compd.lt.c b/test/mppa/instr/individual/compd.lt.c index c42cda56..c42cda56 100644 --- a/test/mppa/instr/compd.lt.c +++ b/test/mppa/instr/individual/compd.lt.c diff --git a/test/mppa/instr/compd.ltu.c b/test/mppa/instr/individual/compd.ltu.c index b03d4d53..b03d4d53 100644 --- a/test/mppa/instr/compd.ltu.c +++ b/test/mppa/instr/individual/compd.ltu.c diff --git a/test/mppa/instr/compd.ne.c b/test/mppa/instr/individual/compd.ne.c index fd9d0b28..fd9d0b28 100644 --- a/test/mppa/instr/compd.ne.c +++ b/test/mppa/instr/individual/compd.ne.c diff --git a/test/mppa/instr/compw.eq.c b/test/mppa/instr/individual/compw.eq.c index cd93f365..cd93f365 100644 --- a/test/mppa/instr/compw.eq.c +++ b/test/mppa/instr/individual/compw.eq.c diff --git a/test/mppa/instr/compw.geu.c b/test/mppa/instr/individual/compw.geu.c index b8fb1adf..b8fb1adf 100644 --- a/test/mppa/instr/compw.geu.c +++ b/test/mppa/instr/individual/compw.geu.c diff --git a/test/mppa/instr/compw.gt.c b/test/mppa/instr/individual/compw.gt.c index 5f6bc907..5f6bc907 100644 --- a/test/mppa/instr/compw.gt.c +++ b/test/mppa/instr/individual/compw.gt.c diff --git a/test/mppa/instr/compw.gtu.c b/test/mppa/instr/individual/compw.gtu.c index 947f6a14..947f6a14 100644 --- a/test/mppa/instr/compw.gtu.c +++ b/test/mppa/instr/individual/compw.gtu.c diff --git a/test/mppa/instr/compw.le.c b/test/mppa/instr/individual/compw.le.c index 35ec6b7d..35ec6b7d 100644 --- a/test/mppa/instr/compw.le.c +++ b/test/mppa/instr/individual/compw.le.c diff --git a/test/mppa/instr/compw.leu.c b/test/mppa/instr/individual/compw.leu.c index 74ebfb42..74ebfb42 100644 --- a/test/mppa/instr/compw.leu.c +++ b/test/mppa/instr/individual/compw.leu.c diff --git a/test/mppa/instr/compw.lt.c b/test/mppa/instr/individual/compw.lt.c index cb1f30bd..cb1f30bd 100644 --- a/test/mppa/instr/compw.lt.c +++ b/test/mppa/instr/individual/compw.lt.c diff --git a/test/mppa/instr/compw.ltu.c b/test/mppa/instr/individual/compw.ltu.c index 6a0c5af1..6a0c5af1 100644 --- a/test/mppa/instr/compw.ltu.c +++ b/test/mppa/instr/individual/compw.ltu.c diff --git a/test/mppa/instr/compw.ne.c b/test/mppa/instr/individual/compw.ne.c index 7035e2c7..7035e2c7 100644 --- a/test/mppa/instr/compw.ne.c +++ b/test/mppa/instr/individual/compw.ne.c diff --git a/test/mppa/instr/div2.c b/test/mppa/instr/individual/div2.c index b5dfe63a..b5dfe63a 100644 --- a/test/mppa/instr/div2.c +++ b/test/mppa/instr/individual/div2.c diff --git a/test/mppa/instr/doubleconv.c b/test/mppa/instr/individual/doubleconv.c index 55b1ddab..55b1ddab 100644 --- a/test/mppa/instr/doubleconv.c +++ b/test/mppa/instr/individual/doubleconv.c diff --git a/test/mppa/instr/floatconv.c b/test/mppa/instr/individual/floatconv.c index 32b798e1..32b798e1 100644 --- a/test/mppa/instr/floatconv.c +++ b/test/mppa/instr/individual/floatconv.c diff --git a/test/mppa/instr/fmuld.c b/test/mppa/instr/individual/fmuld.c index 03c990fa..03c990fa 100644 --- a/test/mppa/instr/fmuld.c +++ b/test/mppa/instr/individual/fmuld.c diff --git a/test/mppa/instr/fmulw.c b/test/mppa/instr/individual/fmulw.c index f85eba64..f85eba64 100644 --- a/test/mppa/instr/fmulw.c +++ b/test/mppa/instr/individual/fmulw.c diff --git a/test/mppa/instr/fnegd.c b/test/mppa/instr/individual/fnegd.c index 974eb7e8..974eb7e8 100644 --- a/test/mppa/instr/fnegd.c +++ b/test/mppa/instr/individual/fnegd.c diff --git a/test/mppa/instr/fnegw.c b/test/mppa/instr/individual/fnegw.c index fbeaab8e..fbeaab8e 100644 --- a/test/mppa/instr/fnegw.c +++ b/test/mppa/instr/individual/fnegw.c diff --git a/test/mppa/instr/for.c b/test/mppa/instr/individual/for.c index 373ab6bd..373ab6bd 100644 --- a/test/mppa/instr/for.c +++ b/test/mppa/instr/individual/for.c diff --git a/test/mppa/instr/forvar.c b/test/mppa/instr/individual/forvar.c index 9e43c198..9e43c198 100644 --- a/test/mppa/instr/forvar.c +++ b/test/mppa/instr/individual/forvar.c diff --git a/test/mppa/instr/forvarl.c b/test/mppa/instr/individual/forvarl.c index c1fe90fd..c1fe90fd 100644 --- a/test/mppa/instr/forvarl.c +++ b/test/mppa/instr/individual/forvarl.c diff --git a/test/mppa/instr/fsbfd.c b/test/mppa/instr/individual/fsbfd.c index f80c1efe..f80c1efe 100644 --- a/test/mppa/instr/fsbfd.c +++ b/test/mppa/instr/individual/fsbfd.c diff --git a/test/mppa/instr/fsbfw.c b/test/mppa/instr/individual/fsbfw.c index 067c40b5..067c40b5 100644 --- a/test/mppa/instr/fsbfw.c +++ b/test/mppa/instr/individual/fsbfw.c diff --git a/test/mppa/instr/indirect_call.c b/test/mppa/instr/individual/indirect_call.c index f376c00a..f376c00a 100644 --- a/test/mppa/instr/indirect_call.c +++ b/test/mppa/instr/individual/indirect_call.c diff --git a/test/mppa/instr/indirect_tailcall.c b/test/mppa/instr/individual/indirect_tailcall.c index e6c16ea1..e6c16ea1 100644 --- a/test/mppa/instr/indirect_tailcall.c +++ b/test/mppa/instr/individual/indirect_tailcall.c diff --git a/test/mppa/instr/lbs.c b/test/mppa/instr/individual/lbs.c index 22a50632..22a50632 100644 --- a/test/mppa/instr/lbs.c +++ b/test/mppa/instr/individual/lbs.c diff --git a/test/mppa/instr/lbz.c b/test/mppa/instr/individual/lbz.c index 04ba098d..04ba098d 100644 --- a/test/mppa/instr/lbz.c +++ b/test/mppa/instr/individual/lbz.c diff --git a/test/mppa/instr/muld.c b/test/mppa/instr/individual/muld.c index f7e23850..f7e23850 100644 --- a/test/mppa/instr/muld.c +++ b/test/mppa/instr/individual/muld.c diff --git a/test/mppa/instr/mulw.c b/test/mppa/instr/individual/mulw.c index a91d966e..a91d966e 100644 --- a/test/mppa/instr/mulw.c +++ b/test/mppa/instr/individual/mulw.c diff --git a/test/mppa/instr/negd.c b/test/mppa/instr/individual/negd.c index 837b9828..837b9828 100644 --- a/test/mppa/instr/negd.c +++ b/test/mppa/instr/individual/negd.c diff --git a/test/mppa/instr/ord.c b/test/mppa/instr/individual/ord.c index cae1ae8b..cae1ae8b 100644 --- a/test/mppa/instr/ord.c +++ b/test/mppa/instr/individual/ord.c diff --git a/test/mppa/instr/sbfd.c b/test/mppa/instr/individual/sbfd.c index 77c28c77..77c28c77 100644 --- a/test/mppa/instr/sbfd.c +++ b/test/mppa/instr/individual/sbfd.c diff --git a/test/mppa/instr/sbfw.c b/test/mppa/instr/individual/sbfw.c index e38a1fff..e38a1fff 100644 --- a/test/mppa/instr/sbfw.c +++ b/test/mppa/instr/individual/sbfw.c diff --git a/test/mppa/instr/simple.c b/test/mppa/instr/individual/simple.c index 944f09c9..944f09c9 100644 --- a/test/mppa/instr/simple.c +++ b/test/mppa/instr/individual/simple.c diff --git a/test/mppa/instr/sllw.c b/test/mppa/instr/individual/sllw.c index 6dd41a6c..6dd41a6c 100644 --- a/test/mppa/instr/sllw.c +++ b/test/mppa/instr/individual/sllw.c diff --git a/test/mppa/instr/srad.c b/test/mppa/instr/individual/srad.c index 00be9d0c..00be9d0c 100644 --- a/test/mppa/instr/srad.c +++ b/test/mppa/instr/individual/srad.c diff --git a/test/mppa/instr/srld.c b/test/mppa/instr/individual/srld.c index 14970efd..14970efd 100644 --- a/test/mppa/instr/srld.c +++ b/test/mppa/instr/individual/srld.c diff --git a/test/mppa/instr/tailcall.c b/test/mppa/instr/individual/tailcall.c index 6c659a01..6c659a01 100644 --- a/test/mppa/instr/tailcall.c +++ b/test/mppa/instr/individual/tailcall.c diff --git a/test/mppa/instr/udivd.c b/test/mppa/instr/individual/udivd.c index cfb31881..cfb31881 100644 --- a/test/mppa/instr/udivd.c +++ b/test/mppa/instr/individual/udivd.c diff --git a/test/mppa/instr/umodd.c b/test/mppa/instr/individual/umodd.c index a7f25f1c..a7f25f1c 100644 --- a/test/mppa/instr/umodd.c +++ b/test/mppa/instr/individual/umodd.c diff --git a/test/mppa/instr/xord.c b/test/mppa/instr/individual/xord.c index b6a90cb0..b6a90cb0 100644 --- a/test/mppa/instr/xord.c +++ b/test/mppa/instr/individual/xord.c diff --git a/test/mppa/instr/modi32.c b/test/mppa/instr/modi32.c new file mode 100644 index 00000000..958ae920 --- /dev/null +++ b/test/mppa/instr/modi32.c @@ -0,0 +1,5 @@ +#include "framework.h" + +BEGIN_TEST(int) + c = a%b; +END_TEST32() diff --git a/test/mppa/instr/modui32.c b/test/mppa/instr/modui32.c new file mode 100644 index 00000000..a39034a8 --- /dev/null +++ b/test/mppa/instr/modui32.c @@ -0,0 +1,7 @@ +#include "framework.h" + +BEGIN_TEST(unsigned int) +{ + c = a%b; +} +END_TEST32() diff --git a/test/mppa/instr/ui32.c b/test/mppa/instr/ui32.c new file mode 100644 index 00000000..f56a9b95 --- /dev/null +++ b/test/mppa/instr/ui32.c @@ -0,0 +1,12 @@ +#include "framework.h" + +BEGIN_TEST(unsigned int) +{ + c = (long long) a; + c += (a >= b); + c += (a > b); + c += (a <= b); + c += (a < b); + c += ((a & 0x1U) != (b & 0x1U)); +} +END_TEST32() diff --git a/test/mppa/instr/compd.gtu.c b/test/mppa/instr/ui64.c index 7b2b96a6..908dec3c 100644 --- a/test/mppa/instr/compd.gtu.c +++ b/test/mppa/instr/ui64.c @@ -3,5 +3,8 @@ BEGIN_TEST(unsigned long long) { c = (a > b); + c += (a <= b); + c += (a < b); + c += ((a & 0x1ULL) != (b & 0x1ULL)); } END_TEST64() diff --git a/test/mppa/interop/i_manyiargs.c b/test/mppa/interop/i32.c index d674c26f..6bc2705c 100644 --- a/test/mppa/interop/i_manyiargs.c +++ b/test/mppa/interop/i32.c @@ -5,5 +5,9 @@ BEGIN_TEST(int) c = i_manyiargs(a, b, a-b, a+b, a*2, b*2, a*2-b, a+b*2, (a-b)*2, (a+b)*2, -2*a, -2*b, a-b, a+b, a*3, b*3, a*3-b, a+b*3, (a-b)*3, (a+b)*3, -3*a, -3*b, a-b, a+b, a*4, b*4, a*4-b, a+b*4, (a-b)*4, (a+b)*4); -END_TEST() + c += i_multiiargs(a, b, a-b, a+b); + c += i_oneiarg(a); + void_void(); + c += a; +END_TEST32() diff --git a/test/mppa/interop/ll_manyllargs.c b/test/mppa/interop/i64.c index 6e0b3b36..3e7240f7 100644 --- a/test/mppa/interop/ll_manyllargs.c +++ b/test/mppa/interop/i64.c @@ -5,4 +5,10 @@ BEGIN_TEST(long long) c = ll_manyllargs(a, b, a-b, a+b, a*2, b*2, a*2-b, a+b*2, (a-b)*2, (a+b)*2, -2*a, -2*b, a-b, a+b, a*3, b*3, a*3-b, a+b*3, (a-b)*3, (a+b)*3, -3*a, -3*b, a-b, a+b, a*4, b*4, a*4-b, a+b*4, (a-b)*4, (a+b)*4); -END_TEST() + c += ll_multillargs(a, b, a-b, a+b); + c += ll_onellarg(a); + c = ll_void(); + c += a; + void_void(); + c += a; +END_TEST64() diff --git a/test/mppa/interop/i_multiiargs.c b/test/mppa/interop/individual/i_multiiargs.c index 0e8c8936..888742b5 100644 --- a/test/mppa/interop/i_multiiargs.c +++ b/test/mppa/interop/individual/i_multiiargs.c @@ -3,4 +3,4 @@ BEGIN_TEST(int) c = i_multiiargs(a, b, a-b, a+b); -END_TEST() +END_TEST32() diff --git a/test/mppa/interop/i_oneiarg.c b/test/mppa/interop/individual/i_oneiarg.c index 42cd1540..9c969fb8 100644 --- a/test/mppa/interop/i_oneiarg.c +++ b/test/mppa/interop/individual/i_oneiarg.c @@ -3,4 +3,4 @@ BEGIN_TEST(int) c = i_oneiarg(a); -END_TEST() +END_TEST32() diff --git a/test/mppa/interop/ll_multillargs.c b/test/mppa/interop/individual/ll_multillargs.c index edb03b12..34b422eb 100644 --- a/test/mppa/interop/ll_multillargs.c +++ b/test/mppa/interop/individual/ll_multillargs.c @@ -3,5 +3,5 @@ BEGIN_TEST(long long) c = ll_multillargs(a, b, a-b, a+b); -END_TEST() +END_TEST64() diff --git a/test/mppa/interop/ll_onellarg.c b/test/mppa/interop/individual/ll_onellarg.c index 0d182166..a2fbbbe9 100644 --- a/test/mppa/interop/ll_onellarg.c +++ b/test/mppa/interop/individual/ll_onellarg.c @@ -3,5 +3,5 @@ BEGIN_TEST(long long) c = ll_onellarg(a); -END_TEST() +END_TEST64() diff --git a/test/mppa/interop/ll_void.c b/test/mppa/interop/individual/ll_void.c index fa350c9b..da128fdd 100644 --- a/test/mppa/interop/ll_void.c +++ b/test/mppa/interop/individual/ll_void.c @@ -4,4 +4,4 @@ BEGIN_TEST(long long) c = ll_void(); c += a; -END_TEST() +END_TEST64() diff --git a/test/mppa/interop/void_void.c b/test/mppa/interop/individual/void_void.c index e729edb2..976a721b 100644 --- a/test/mppa/interop/void_void.c +++ b/test/mppa/interop/individual/void_void.c @@ -4,4 +4,4 @@ BEGIN_TEST(long long) void_void(); c = a; -END_TEST() +END_TEST64() diff --git a/x86/Conventions1.v b/x86/Conventions1.v index 646c4afb..35d555f9 100644 --- a/x86/Conventions1.v +++ b/x86/Conventions1.v @@ -15,6 +15,7 @@ Require Import Coqlib Decidableplus. Require Import AST Machregs Locations. +Require Import Errors. (** * Classification of machine registers *) @@ -26,7 +27,7 @@ Require Import AST Machregs Locations. We follow the x86-32 and x86-64 application binary interfaces (ABI) in our choice of callee- and caller-save registers. *) - + Definition is_callee_save (r: mreg) : bool := match r with | AX | CX | DX => false diff --git a/x86/Machregsaux.ml b/x86/Machregsaux.ml index 473e0602..80066b00 100644 --- a/x86/Machregsaux.ml +++ b/x86/Machregsaux.ml @@ -14,9 +14,9 @@ open Camlcoq open Machregs - + let register_names : (mreg, string) Hashtbl.t = Hashtbl.create 31 - + let _ = List.iter (fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s)) @@ -31,3 +31,8 @@ let register_by_name s = Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s) let can_reserve_register r = Conventions1.is_callee_save r + +let class_of_type = function + | AST.Tint | AST.Tlong -> 0 + | AST.Tfloat | AST.Tsingle -> 1 + | AST.Tany32 | AST.Tany64 -> assert false diff --git a/x86/Machregsaux.mli b/x86/Machregsaux.mli index 9404568d..d7117c21 100644 --- a/x86/Machregsaux.mli +++ b/x86/Machregsaux.mli @@ -16,3 +16,5 @@ val name_of_register: Machregs.mreg -> string option val register_by_name: string -> Machregs.mreg option val is_scratch_register: string -> bool val can_reserve_register: Machregs.mreg -> bool + +val class_of_type: AST.typ -> int diff --git a/x86/SelectLong.vp b/x86/SelectLong.vp index b213e23f..4f9fb518 100644 --- a/x86/SelectLong.vp +++ b/x86/SelectLong.vp @@ -16,7 +16,7 @@ Require Import Coqlib. Require Import Compopts. Require Import AST Integers Floats. Require Import Op CminorSel. -Require Import SelectOp SplitLong. +Require Import OpHelpers SelectOp SplitLong. Local Open Scope cminorsel_scope. Local Open Scope string_scope. diff --git a/x86/SelectLongproof.v b/x86/SelectLongproof.v index 3bef632d..f008f39e 100644 --- a/x86/SelectLongproof.v +++ b/x86/SelectLongproof.v @@ -16,6 +16,7 @@ Require Import String Coqlib Maps Integers Floats Errors. Require Archi. Require Import AST Values Memory Globalenvs Events. Require Import Cminor Op CminorSel. +Require Import OpHelpers OpHelpersproof. Require Import SelectOp SelectOpproof SplitLong SplitLongproof. Require Import SelectLong. diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp index a1583600..eadda093 100644 --- a/x86/SelectOp.vp +++ b/x86/SelectOp.vp @@ -40,6 +40,7 @@ Require Import Coqlib. Require Import Compopts. Require Import AST Integers Floats. Require Import Op CminorSel. +Require Import OpHelpers. Local Open Scope cminorsel_scope. @@ -540,3 +541,10 @@ Nondetfunction builtin_arg (e: expr) := | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs | _ => BA e end. + +(* floats *) +Definition divf_base (e1: expr) (e2: expr) := + Eop Odivf (e1 ::: e2 ::: Enil). + +Definition divfs_base (e1: expr) (e2: expr) := + Eop Odivfs (e1 ::: e2 ::: Enil). diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v index fdbadaa8..1eeb5906 100644 --- a/x86/SelectOpproof.v +++ b/x86/SelectOpproof.v @@ -23,6 +23,8 @@ Require Import Cminor. Require Import Op. Require Import CminorSel. Require Import SelectOp. +Require Import OpHelpers. +Require Import OpHelpersproof. Local Open Scope cminorsel_scope. @@ -74,8 +76,10 @@ Ltac TrivialExists := (** * Correctness of the smart constructors *) Section CMCONSTR. - -Variable ge: genv. +Variable prog: program. +Variable hf: helper_functions. +Hypothesis HELPERS: helper_functions_declared prog hf. +Let ge := Genv.globalenv prog. Variable sp: val. Variable e: env. Variable m: mem. @@ -984,4 +988,25 @@ Proof. - constructor; auto. Qed. + +(* floating-point division without HELPERS *) +Theorem eval_divf_base: + forall le a b x y, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + exists v, eval_expr ge sp e m le (divf_base a b) v /\ Val.lessdef (Val.divf x y) v. +Proof. + intros; unfold divf_base. + TrivialExists. +Qed. + +Theorem eval_divfs_base: + forall le a b x y, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + exists v, eval_expr ge sp e m le (divfs_base a b) v /\ Val.lessdef (Val.divfs x y) v. +Proof. + intros; unfold divfs_base. + TrivialExists. +Qed. End CMCONSTR. |