From 26a7a6598a80c29a139c533419b38be63c88cd76 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 May 2019 16:24:32 +0200 Subject: indexed2XS begin --- mppa_k1c/Asmblockgen.v | 1 + 1 file changed, 1 insertion(+) (limited to 'mppa_k1c/Asmblockgen.v') diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 6cd31468..c2a0a315 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -888,6 +888,7 @@ Definition transl_load_rrr (chunk: memory_chunk) (addr: addressing) Definition transl_load (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := match addr with + | Aindexed2XS _ => Error (msg "transl_load Aindexed2XS") | Aindexed2 => transl_load_rrr chunk addr args dst k | _ => transl_load_rro chunk addr args dst k end. -- cgit From 667c260620b545c04355dd030fc4430790a3a055 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 May 2019 17:04:34 +0200 Subject: translate load.xs --- mppa_k1c/Asmblockgen.v | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) (limited to 'mppa_k1c/Asmblockgen.v') diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index c2a0a315..7c8a08f6 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -846,6 +846,19 @@ Definition transl_memory_access2 | _, _ => Error (msg "Asmblockgen.transl_memory_access2") end. +Definition transl_memory_access2XS + (chunk: memory_chunk) + (mk_instr: ireg -> ireg -> basic) + (addr: addressing) (args: list mreg) (k: bcode) : res bcode := + match addr, args with + | (Aindexed2XS scale), (a1 :: a2 :: nil) => + assertion (Z.eqb (zscale_of_chunk chunk) scale); + do rs1 <- ireg_of a1; + do rs2 <- ireg_of a2; + OK (mk_instr rs1 rs2 ::i k) + | _, _ => Error (msg "Asmblockgen.transl_memory_access2XS") + end. + Definition transl_memory_access (mk_instr: ireg -> offset -> basic) (addr: addressing) (args: list mreg) (k: bcode) : res bcode := @@ -885,10 +898,15 @@ Definition transl_load_rrr (chunk: memory_chunk) (addr: addressing) do r <- ireg_of dst; transl_memory_access2 (PLoadRRR (chunk2load chunk) r) addr args k. +Definition transl_load_rrrXS (chunk: memory_chunk) (addr: addressing) + (args: list mreg) (dst: mreg) (k: bcode) : res bcode := + do r <- ireg_of dst; + transl_memory_access2XS chunk (PLoadRRR (chunk2load chunk) r) addr args k. + Definition transl_load (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := match addr with - | Aindexed2XS _ => Error (msg "transl_load Aindexed2XS") + | Aindexed2XS _ => transl_load_rrrXS chunk addr args dst k | Aindexed2 => transl_load_rrr chunk addr args dst k | _ => transl_load_rro chunk addr args dst k end. -- cgit From 98be0205d9d29378fb272a9f424144651bd8afec Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 May 2019 19:44:11 +0200 Subject: ça avance MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- mppa_k1c/Asmblockgen.v | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'mppa_k1c/Asmblockgen.v') diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 7c8a08f6..a74aa9f6 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -849,14 +849,14 @@ Definition transl_memory_access2 Definition transl_memory_access2XS (chunk: memory_chunk) (mk_instr: ireg -> ireg -> basic) - (addr: addressing) (args: list mreg) (k: bcode) : res bcode := - match addr, args with - | (Aindexed2XS scale), (a1 :: a2 :: nil) => + scale (args: list mreg) (k: bcode) : res bcode := + match args with + | (a1 :: a2 :: nil) => assertion (Z.eqb (zscale_of_chunk chunk) scale); do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (mk_instr rs1 rs2 ::i k) - | _, _ => Error (msg "Asmblockgen.transl_memory_access2XS") + | _ => Error (msg "Asmblockgen.transl_memory_access2XS") end. Definition transl_memory_access @@ -898,15 +898,15 @@ Definition transl_load_rrr (chunk: memory_chunk) (addr: addressing) do r <- ireg_of dst; transl_memory_access2 (PLoadRRR (chunk2load chunk) r) addr args k. -Definition transl_load_rrrXS (chunk: memory_chunk) (addr: addressing) +Definition transl_load_rrrXS (chunk: memory_chunk) (scale : Z) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := do r <- ireg_of dst; - transl_memory_access2XS chunk (PLoadRRR (chunk2load chunk) r) addr args k. + transl_memory_access2XS chunk (PLoadRRR (chunk2load chunk) r) scale args k. Definition transl_load (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := match addr with - | Aindexed2XS _ => transl_load_rrrXS chunk addr args dst k + | Aindexed2XS scale => transl_load_rrrXS chunk scale args dst k | Aindexed2 => transl_load_rrr chunk addr args dst k | _ => transl_load_rro chunk addr args dst k end. -- cgit From cbe3f094b32077ce8d8569556d4ebc6341b09dd9 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 May 2019 21:54:11 +0200 Subject: it compiles --- mppa_k1c/Asmblockgen.v | 36 +++++++++++++++++++++--------------- 1 file changed, 21 insertions(+), 15 deletions(-) (limited to 'mppa_k1c/Asmblockgen.v') diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index a74aa9f6..ea99c098 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -807,31 +807,31 @@ end. Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode) := match ty, preg_of dst with - | Tint, IR rd => OK (indexed_memory_access (Plw rd) base ofs ::i k) - | Tlong, IR rd => OK (indexed_memory_access (Pld rd) base ofs ::i k) - | Tsingle, IR rd => OK (indexed_memory_access (Pfls rd) base ofs ::i k) - | Tfloat, IR rd => OK (indexed_memory_access (Pfld rd) base ofs ::i k) - | Tany32, IR rd => OK (indexed_memory_access (Plw_a rd) base ofs ::i k) - | Tany64, IR rd => OK (indexed_memory_access (Pld_a rd) base ofs ::i k) + | Tint, IR rd => OK (indexed_memory_access (PLoadRRO Plw rd) base ofs ::i k) + | Tlong, IR rd => OK (indexed_memory_access (PLoadRRO Pld rd) base ofs ::i k) + | Tsingle, IR rd => OK (indexed_memory_access (PLoadRRO Pfls rd) base ofs ::i k) + | Tfloat, IR rd => OK (indexed_memory_access (PLoadRRO Pfld rd) base ofs ::i k) + | Tany32, IR rd => OK (indexed_memory_access (PLoadRRO Plw_a rd) base ofs ::i k) + | Tany64, IR rd => OK (indexed_memory_access (PLoadRRO Pld_a rd) base ofs ::i k) | _, _ => Error (msg "Asmblockgen.loadind") end. Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: bcode) := match ty, preg_of src with - | Tint, IR rd => OK (indexed_memory_access (Psw rd) base ofs ::i k) - | Tlong, IR rd => OK (indexed_memory_access (Psd rd) base ofs ::i k) - | Tsingle, IR rd => OK (indexed_memory_access (Pfss rd) base ofs ::i k) - | Tfloat, IR rd => OK (indexed_memory_access (Pfsd rd) base ofs ::i k) - | Tany32, IR rd => OK (indexed_memory_access (Psw_a rd) base ofs ::i k) - | Tany64, IR rd => OK (indexed_memory_access (Psd_a rd) base ofs ::i k) + | Tint, IR rd => OK (indexed_memory_access (PStoreRRO Psw rd) base ofs ::i k) + | Tlong, IR rd => OK (indexed_memory_access (PStoreRRO Psd rd) base ofs ::i k) + | Tsingle, IR rd => OK (indexed_memory_access (PStoreRRO Pfss rd) base ofs ::i k) + | Tfloat, IR rd => OK (indexed_memory_access (PStoreRRO Pfsd rd) base ofs ::i k) + | Tany32, IR rd => OK (indexed_memory_access (PStoreRRO Psw_a rd) base ofs ::i k) + | Tany64, IR rd => OK (indexed_memory_access (PStoreRRO Psd_a rd) base ofs ::i k) | _, _ => Error (msg "Asmblockgen.storeind") end. Definition loadind_ptr (base: ireg) (ofs: ptrofs) (dst: ireg) := - indexed_memory_access (Pld dst) base ofs. + indexed_memory_access (PLoadRRO Pld dst) base ofs. Definition storeind_ptr (src: ireg) (base: ireg) (ofs: ptrofs) := - indexed_memory_access (Psd src) base ofs. + indexed_memory_access (PStoreRRO Psd src) base ofs. (** Translation of memory accesses: loads, and stores. *) @@ -901,7 +901,7 @@ Definition transl_load_rrr (chunk: memory_chunk) (addr: addressing) Definition transl_load_rrrXS (chunk: memory_chunk) (scale : Z) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := do r <- ireg_of dst; - transl_memory_access2XS chunk (PLoadRRR (chunk2load chunk) r) scale args k. + transl_memory_access2XS chunk (PLoadRRRXS (chunk2load chunk) r) scale args k. Definition transl_load (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := @@ -933,10 +933,16 @@ Definition transl_store_rrr (chunk: memory_chunk) (addr: addressing) do r <- ireg_of src; transl_memory_access2 (PStoreRRR (chunk2store chunk) r) addr args k. +Definition transl_store_rrrxs (chunk: memory_chunk) (scale: Z) + (args: list mreg) (src: mreg) (k: bcode) : res bcode := + do r <- ireg_of src; + transl_memory_access2XS chunk (PStoreRRRXS (chunk2store chunk) r) scale args k. + Definition transl_store (chunk: memory_chunk) (addr: addressing) (args: list mreg) (src: mreg) (k: bcode) : res bcode := match addr with | Aindexed2 => transl_store_rrr chunk addr args src k + | Aindexed2XS scale => transl_store_rrrxs chunk scale args src k | _ => transl_store_rro chunk addr args src k end. -- cgit From 57ddece94f4c4b44e8e3127c6f5f72aaa5962250 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 May 2019 22:20:35 +0200 Subject: does not yet work, arity mismatch --- mppa_k1c/Asmblockgen.v | 1 + 1 file changed, 1 insertion(+) (limited to 'mppa_k1c/Asmblockgen.v') diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index ea99c098..ca7094da 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -22,6 +22,7 @@ Require Import Coqlib Errors. Require Import AST Integers Floats Memdata. Require Import Op Locations Machblock Asmblock. Require ExtValues. +Require Import Chunks. Local Open Scope string_scope. Local Open Scope error_monad_scope. -- cgit