From 34c136fcd0ffcfe61e3cec5c72a90a1d3bcdc941 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 22 Jul 2019 18:38:49 +0200 Subject: (#137) [BROKEN] - Finer latencies for the oracle. Some debugging to do --- mppa_k1c/PostpassSchedulingOracle.ml | 133 ++++++++++++++++++++++++----------- 1 file changed, 93 insertions(+), 40 deletions(-) diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 895f9f40..b9fc3c18 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -38,6 +38,8 @@ type ab_inst_rec = { inst: real_instruction; write_locs : location list; read_locs : location list; + read_at_id : location list; (* Must be contained in read_locs *) + read_at_e1 : location list; (* idem *) imm : immediate option; is_control : bool; } @@ -232,25 +234,40 @@ let jl_real = Goto let cb_real = Cb let cbu_real = Cb -let arith_rri32_rec i rd rs imm32 = { inst = arith_rri32_real i; write_locs = [Reg rd]; read_locs = [Reg rs]; imm = imm32; is_control = false } +let arith_rri32_rec i rd rs imm32 = { inst = arith_rri32_real i; write_locs = [Reg rd]; read_locs = [Reg rs]; imm = imm32; is_control = false; + read_at_id = []; read_at_e1 = [] } -let arith_rri64_rec i rd rs imm64 = { inst = arith_rri64_real i; write_locs = [Reg rd]; read_locs = [Reg rs]; imm = imm64; is_control = false } +let arith_rri64_rec i rd rs imm64 = { inst = arith_rri64_real i; write_locs = [Reg rd]; read_locs = [Reg rs]; imm = imm64; is_control = false; + read_at_id = []; read_at_e1 = [] } -let arith_rrr_rec i rd rs1 rs2 = { inst = arith_rrr_real i; write_locs = [Reg rd]; read_locs = [Reg rs1; Reg rs2]; imm = None; is_control = false} +let arith_rrr_rec i rd rs1 rs2 = { inst = arith_rrr_real i; write_locs = [Reg rd]; read_locs = [Reg rs1; Reg rs2]; imm = None; is_control = false; + read_at_id = []; read_at_e1 = [] } -let arith_arri32_rec i rd rs imm32 = { inst = arith_arri32_real i; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs]; imm = imm32; is_control = false } +let arith_arri32_rec i rd rs imm32 = + let rae1 = match i with Pmaddiw -> [Reg rd] | _ -> [] + in { inst = arith_arri32_real i; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs]; imm = imm32; is_control = false; + read_at_id = [] ; read_at_e1 = rae1 } -let arith_arri64_rec i rd rs imm64 = { inst = arith_arri64_real i; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs]; imm = imm64; is_control = false } +let arith_arri64_rec i rd rs imm64 = + let rae1 = match i with Pmaddil -> [Reg rd] | _ -> [] + in { inst = arith_arri64_real i; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs]; imm = imm64; is_control = false; + read_at_id = []; read_at_e1 = rae1 } -let arith_arr_rec i rd rs = { inst = arith_arr_real i; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs]; imm = None; is_control = false} +let arith_arr_rec i rd rs = { inst = arith_arr_real i; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs]; imm = None; is_control = false; + read_at_id = []; read_at_e1 = [] } -let arith_arrr_rec i rd rs1 rs2 = { inst = arith_arrr_real i; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs1; Reg rs2]; imm = None; is_control = false} +let arith_arrr_rec i rd rs1 rs2 = + let rae1 = match i with Pmaddl | Pmaddw | Pmsubl | Pmsubw -> [Reg rd] | _ -> [] + in { inst = arith_arrr_real i; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs1; Reg rs2]; imm = None; is_control = false; + read_at_id = []; read_at_e1 = rae1 } -let arith_rr_rec i rd rs = { inst = arith_rr_real i; write_locs = [Reg rd]; read_locs = [Reg rs]; imm = None; is_control = false} +let arith_rr_rec i rd rs = { inst = arith_rr_real i; write_locs = [Reg rd]; read_locs = [Reg rs]; imm = None; is_control = false; + read_at_id = []; read_at_e1 = [] } let arith_r_rec i rd = match i with (* For Ploadsymbol, writing the highest integer since we do not know how many bits does a symbol have *) - | Ploadsymbol (id, ofs) -> { inst = loadsymbol_real; write_locs = [Reg rd]; read_locs = []; imm = Some (I64 Integers.Int64.max_signed); is_control = false} + | Ploadsymbol (id, ofs) -> { inst = loadsymbol_real; write_locs = [Reg rd]; read_locs = []; imm = Some (I64 Integers.Int64.max_signed); + is_control = false; read_at_id = []; read_at_e1 = [] } let arith_rec i = match i with @@ -262,45 +279,54 @@ let arith_rec i = | PArithARRI32 (i, rd, rs, imm32) -> arith_arri32_rec i (IR rd) (IR rs) (Some (I32 imm32)) | PArithARRI64 (i, rd, rs, imm64) -> arith_arri64_rec i (IR rd) (IR rs) (Some (I64 imm64)) | PArithARRR (i, rd, rs1, rs2) -> arith_arrr_rec i (IR rd) (IR rs1) (IR rs2) - | PArithRI32 (rd, imm32) -> { inst = arith_ri32_real; write_locs = [Reg (IR rd)]; read_locs = []; imm = (Some (I32 imm32)) ; is_control = false} - | PArithRI64 (rd, imm64) -> { inst = arith_ri64_real; write_locs = [Reg (IR rd)]; read_locs = []; imm = (Some (I64 imm64)) ; is_control = false} + | PArithRI32 (rd, imm32) -> { inst = arith_ri32_real; write_locs = [Reg (IR rd)]; read_locs = []; imm = (Some (I32 imm32)) ; is_control = false; + read_at_id = []; read_at_e1 = [] } + | PArithRI64 (rd, imm64) -> { inst = arith_ri64_real; write_locs = [Reg (IR rd)]; read_locs = []; imm = (Some (I64 imm64)) ; is_control = false; + read_at_id = []; read_at_e1 = [] } | PArithRF32 (rd, f) -> { inst = arith_rf32_real; write_locs = [Reg (IR rd)]; read_locs = []; - imm = (Some (I32 (Floats.Float32.to_bits f))); is_control = false} + imm = (Some (I32 (Floats.Float32.to_bits f))); is_control = false; read_at_id = []; read_at_e1 = []} | PArithRF64 (rd, f) -> { inst = arith_rf64_real; write_locs = [Reg (IR rd)]; read_locs = []; - imm = (Some (I64 (Floats.Float.to_bits f))); is_control = false} + imm = (Some (I64 (Floats.Float.to_bits f))); is_control = false; read_at_id = []; read_at_e1 = []} | PArithRR (i, rd, rs) -> arith_rr_rec i (IR rd) (IR rs) | PArithR (i, rd) -> arith_r_rec i (IR rd) let load_rec i = match i with | PLoadRRO (i, rs1, rs2, imm) -> - { inst = load_real i; write_locs = [Reg (IR rs1)]; read_locs = [Mem; Reg (IR rs2)]; imm = (Some (Off imm)) ; is_control = false} + { inst = load_real i; write_locs = [Reg (IR rs1)]; read_locs = [Mem; Reg (IR rs2)]; imm = (Some (Off imm)) ; is_control = false; + read_at_id = []; read_at_e1 = [] } | PLoadQRRO(rs, ra, imm) -> let (rs0, rs1) = gpreg_q_expand rs in - { inst = loadqrro_real; write_locs = [Reg (IR rs0); Reg (IR rs1)]; read_locs = [Mem; Reg (IR ra)]; imm = (Some (Off imm)) ; is_control = false} + { inst = loadqrro_real; write_locs = [Reg (IR rs0); Reg (IR rs1)]; read_locs = [Mem; Reg (IR ra)]; imm = (Some (Off imm)) ; is_control = false; + read_at_id = []; read_at_e1 = [] } | PLoadORRO(rs, ra, imm) -> let (((rs0, rs1), rs2), rs3) = gpreg_o_expand rs in - { inst = loadorro_real; write_locs = [Reg (IR rs0); Reg (IR rs1); Reg (IR rs2); Reg (IR rs3)]; read_locs = [Mem; Reg (IR ra)]; imm = (Some (Off imm)) ; is_control = false} + { inst = loadorro_real; write_locs = [Reg (IR rs0); Reg (IR rs1); Reg (IR rs2); Reg (IR rs3)]; read_locs = [Mem; Reg (IR ra)]; + imm = (Some (Off imm)) ; is_control = false; read_at_id = []; read_at_e1 = []} | PLoadRRR (i, rs1, rs2, rs3) | PLoadRRRXS (i, rs1, rs2, rs3) -> - { inst = load_real i; write_locs = [Reg (IR rs1)]; read_locs = [Mem; Reg (IR rs2); Reg (IR rs3)]; imm = None ; is_control = false} + { inst = load_real i; write_locs = [Reg (IR rs1)]; read_locs = [Mem; Reg (IR rs2); Reg (IR rs3)]; imm = None ; is_control = false; + read_at_id = []; read_at_e1 = [] } let store_rec i = match i with - | PStoreRRO (i, rs1, rs2, imm) -> - { inst = store_real i; write_locs = [Mem]; read_locs = [Reg (IR rs1); Reg (IR rs2)]; imm = (Some (Off imm)) - ; is_control = false} + | PStoreRRO (i, rs, ra, imm) -> + { inst = store_real i; write_locs = [Mem]; read_locs = [Reg (IR rs); Reg (IR ra)]; imm = (Some (Off imm)); + read_at_id = []; read_at_e1 = [Reg (IR rs)] ; is_control = false} | PStoreQRRO (rs, ra, imm) -> let (rs0, rs1) = gpreg_q_expand rs in - { inst = storeqrro_real; write_locs = [Mem]; read_locs = [Reg (IR rs0); Reg (IR rs1); Reg (IR ra)]; imm = (Some (Off imm)) - ; is_control = false} + { inst = storeqrro_real; write_locs = [Mem]; read_locs = [Reg (IR rs0); Reg (IR rs1); Reg (IR ra)]; imm = (Some (Off imm)); + read_at_id = []; read_at_e1 = [Reg (IR rs0); Reg (IR rs1)] ; is_control = false} | PStoreORRO (rs, ra, imm) -> let (((rs0, rs1), rs2), rs3) = gpreg_o_expand rs in - { inst = storeorro_real; write_locs = [Mem]; read_locs = [Reg (IR rs0); Reg (IR rs1); Reg (IR rs2); Reg (IR rs3); Reg (IR ra)]; imm = (Some (Off imm)) - ; is_control = false} - | PStoreRRR (i, rs1, rs2, rs3) | PStoreRRRXS (i, rs1, rs2, rs3) -> { inst = store_real i; write_locs = [Mem]; read_locs = [Reg (IR rs1); Reg (IR rs2); Reg (IR rs3)]; imm = None - ; is_control = false} + { inst = storeorro_real; write_locs = [Mem]; read_locs = [Reg (IR rs0); Reg (IR rs1); Reg (IR rs2); Reg (IR rs3); Reg (IR ra)]; + imm = (Some (Off imm)); read_at_id = []; read_at_e1 = [Reg (IR rs0); Reg (IR rs1); Reg (IR rs2); Reg (IR rs3)]; is_control = false} + | PStoreRRR (i, rs, ra1, ra2) | PStoreRRRXS (i, rs, ra1, ra2) -> + { inst = store_real i; write_locs = [Mem]; read_locs = [Reg (IR rs); Reg (IR ra1); Reg (IR ra2)]; imm = None; + read_at_id = []; read_at_e1 = [Reg (IR rs)]; is_control = false} -let get_rec (rd:gpreg) rs = { inst = get_real; write_locs = [Reg (IR rd)]; read_locs = [Reg rs]; imm = None; is_control = false } +let get_rec (rd:gpreg) rs = { inst = get_real; write_locs = [Reg (IR rd)]; read_locs = [Reg rs]; imm = None; is_control = false; + read_at_id = []; read_at_e1 = [] } -let set_rec rd (rs:gpreg) = { inst = set_real; write_locs = [Reg rd]; read_locs = [Reg (IR rs)]; imm = None; is_control = false } +let set_rec rd (rs:gpreg) = { inst = set_real; write_locs = [Reg rd]; read_locs = [Reg (IR rs)]; imm = None; is_control = false; + read_at_id = [Reg (IR rs)]; read_at_e1 = [] } let basic_rec i = match i with @@ -311,20 +337,24 @@ let basic_rec i = | Pfreeframe (_, _) -> raise OpaqueInstruction | Pget (rd, rs) -> get_rec rd rs | Pset (rd, rs) -> set_rec rd rs - | Pnop -> { inst = nop_real; write_locs = []; read_locs = []; imm = None ; is_control = false} + | Pnop -> { inst = nop_real; write_locs = []; read_locs = []; imm = None ; is_control = false; read_at_id = []; read_at_e1 = []} let expand_rec = function | Pbuiltin _ -> raise OpaqueInstruction let ctl_flow_rec = function - | Pret -> { inst = ret_real; write_locs = []; read_locs = [Reg RA]; imm = None ; is_control = true} - | Pcall lbl -> { inst = call_real; write_locs = [Reg RA]; read_locs = []; imm = None ; is_control = true} - | Picall r -> { inst = icall_real; write_locs = [Reg RA]; read_locs = [Reg (IR r)]; imm = None; is_control = true} - | Pgoto lbl -> { inst = goto_real; write_locs = []; read_locs = []; imm = None ; is_control = true} - | Pigoto r -> { inst = igoto_real; write_locs = []; read_locs = [Reg (IR r)]; imm = None ; is_control = true} - | Pj_l lbl -> { inst = goto_real; write_locs = []; read_locs = []; imm = None ; is_control = true} - | Pcb (bt, rs, lbl) -> { inst = cb_real; write_locs = []; read_locs = [Reg (IR rs)]; imm = None ; is_control = true} - | Pcbu (bt, rs, lbl) -> { inst = cbu_real; write_locs = []; read_locs = [Reg (IR rs)]; imm = None ; is_control = true} + | Pret -> { inst = ret_real; write_locs = []; read_locs = [Reg RA]; imm = None ; is_control = true; read_at_id = [Reg RA]; read_at_e1 = []} + | Pcall lbl -> { inst = call_real; write_locs = [Reg RA]; read_locs = []; imm = None ; is_control = true; read_at_id = []; read_at_e1 = []} + | Picall r -> { inst = icall_real; write_locs = [Reg RA]; read_locs = [Reg (IR r)]; imm = None; is_control = true; + read_at_id = [Reg (IR r)]; read_at_e1 = [] } + | Pgoto lbl -> { inst = goto_real; write_locs = []; read_locs = []; imm = None ; is_control = true; read_at_id = []; read_at_e1 = []} + | Pigoto r -> { inst = igoto_real; write_locs = []; read_locs = [Reg (IR r)]; imm = None ; is_control = true; + read_at_id = [Reg (IR r)]; read_at_e1 = [] } + | Pj_l lbl -> { inst = goto_real; write_locs = []; read_locs = []; imm = None ; is_control = true; read_at_id = []; read_at_e1 = []} + | Pcb (bt, rs, lbl) -> { inst = cb_real; write_locs = []; read_locs = [Reg (IR rs)]; imm = None ; is_control = true; + read_at_id = [Reg (IR rs)]; read_at_e1 = [] } + | Pcbu (bt, rs, lbl) -> { inst = cbu_real; write_locs = []; read_locs = [Reg (IR rs)]; imm = None ; is_control = true; + read_at_id = [Reg (IR rs)]; read_at_e1 = [] } | Pjumptable (r, _) -> raise OpaqueInstruction (* { inst = "Pjumptable"; write_locs = [Reg (IR GPR62); Reg (IR GPR63)]; read_locs = [Reg (IR r)]; imm = None ; is_control = true} *) let control_rec i = @@ -350,6 +380,8 @@ let instruction_recs bb = (basic_recs bb.body) @ (exit_rec bb.exit) type inst_info = { write_locs : location list; read_locs : location list; + reads_at_id : bool; + reads_at_e1 : bool; is_control : bool; usage: int array; (* resources consumed by the instruction *) latency: int; @@ -582,6 +614,16 @@ let rec_to_usage r = | Fnarrowdw -> alu_full | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw -> mau +let inst_info_to_dlatency i = + begin + assert (not (i.reads_at_id && i.reads_at_e1)); + match i.reads_at_id with + | true -> +1 + | false -> (match i.reads_at_e1 with + | true -> -1 + | false -> 0) + end + let real_inst_to_latency = function | Nop -> 0 (* Only goes through ID *) | Addw | Andw | Compw | Orw | Sbfw | Sbfxw | Sraw | Srsw | Srlw | Sllw | Xorw @@ -601,10 +643,17 @@ let real_inst_to_latency = function | Fnegd | Fnegw | Fabsd | Fabsw | Fwidenlwd | Fnarrowdw -> 1 | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw -> 4 +let rec empty_inter la = function + | [] -> true + | b::lb -> if (List.mem b la) then false else empty_inter la lb + let rec_to_info r : inst_info = let usage = rec_to_usage r and latency = real_inst_to_latency r.inst - in { write_locs = r.write_locs; read_locs = r.read_locs; usage=usage; latency=latency; is_control=r.is_control } + and reads_at_id = not (empty_inter r.read_locs r.read_at_id) + and reads_at_e1 = not (empty_inter r.read_locs r.read_at_e1) + in { write_locs = r.write_locs; read_locs = r.read_locs; usage=usage; latency=latency; is_control=r.is_control; + reads_at_id = reads_at_id; reads_at_e1 = reads_at_e1 } let instruction_infos bb = List.map rec_to_info (instruction_recs bb) @@ -651,6 +700,8 @@ let rec get_accesses hashloc (ll: location list) = match ll with | [] -> [] | loc :: llocs -> (find_in_hash hashloc loc) @ (get_accesses hashloc llocs) +let compute_latency (ifrom: inst_info) (ito: inst_info) = ifrom.latency + (inst_info_to_dlatency ito) + let latency_constraints bb = let written = LocHash.create 70 and read = LocHash.create 70 @@ -662,8 +713,10 @@ let latency_constraints bb = and waw = get_accesses written i.write_locs and war = get_accesses read i.write_locs in begin - List.iter (fun i -> constraints := {instr_from = i; instr_to = !count; latency = (List.nth instr_infos i).latency} :: !constraints) raw; - List.iter (fun i -> constraints := {instr_from = i; instr_to = !count; latency = (List.nth instr_infos i).latency} :: !constraints) waw; + List.iter (fun i -> constraints := {instr_from = i; instr_to = !count; + latency = compute_latency (List.nth instr_infos i) (List.nth instr_infos !count)} :: !constraints) raw; + List.iter (fun i -> constraints := {instr_from = i; instr_to = !count; + latency = compute_latency (List.nth instr_infos i) (List.nth instr_infos !count)} :: !constraints) waw; List.iter (fun i -> constraints := {instr_from = i; instr_to = !count; latency = 0} :: !constraints) war; if i.is_control then List.iter (fun n -> constraints := {instr_from = n; instr_to = !count; latency = 0} :: !constraints) (intlist !count); (* Updating "read" and "written" hashmaps *) -- cgit From 4c1209c5c1e0e667f20f13bc02662fdc7e4868ac Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 23 Jul 2019 10:42:47 +0200 Subject: (#137) Possible fix --- mppa_k1c/PostpassSchedulingOracle.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index b9fc3c18..fd03a80c 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -700,7 +700,10 @@ let rec get_accesses hashloc (ll: location list) = match ll with | [] -> [] | loc :: llocs -> (find_in_hash hashloc loc) @ (get_accesses hashloc llocs) -let compute_latency (ifrom: inst_info) (ito: inst_info) = ifrom.latency + (inst_info_to_dlatency ito) +let compute_latency (ifrom: inst_info) (ito: inst_info) = + let dlat = inst_info_to_dlatency ito + in let lat = ifrom.latency + dlat + in assert (lat >= 0); if (lat == 0) then 1 else lat let latency_constraints bb = let written = LocHash.create 70 -- cgit From 7da1af080217eef5626480ac30feda45ff8ca002 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 24 Jul 2019 11:01:37 +0200 Subject: (#144) Fixing on RTL dumps --- mppa_k1c/Op.v | 20 ++++++++--------- mppa_k1c/PrintOp.ml | 63 ++++++++++++++++++++++++++++++++++------------------- 2 files changed, 50 insertions(+), 33 deletions(-) diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 35fbb596..815d3958 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -100,23 +100,23 @@ Inductive operation : Type := | Onandimm (n: int) (**r [rd = ~(r1 & n)] *) | Oor (**r [rd = r1 | r2] *) | Oorimm (n: int) (**r [rd = r1 | n] *) - | Onor (**r [rd = r1 | r2] *) - | Onorimm (n: int) (**r [rd = r1 | n] *) + | Onor (**r [rd = ~(r1 | r2)] *) + | Onorimm (n: int) (**r [rd = ~(r1 | n)] *) | Oxor (**r [rd = r1 ^ r2] *) | Oxorimm (n: int) (**r [rd = r1 ^ n] *) | Onxor (**r [rd = ~(r1 ^ r2)] *) | Onxorimm (n: int) (**r [rd = ~(r1 ^ n)] *) | Onot (**r [rd = ~r1] *) - | Oandn (**r [rd = (~r1) ^ r2] *) - | Oandnimm (n: int) (**r [rd = (~r1) ^ n] *) + | Oandn (**r [rd = (~r1) & r2] *) + | Oandnimm (n: int) (**r [rd = (~r1) & n] *) | Oorn (**r [rd = (~r1) | r2] *) | Oornimm (n: int) (**r [rd = (~r1) | n] *) | Oshl (**r [rd = r1 << r2] *) | Oshlimm (n: int) (**r [rd = r1 << n] *) - | Oshr (**r [rd = r1 >> r2] (signed) *) - | Oshrimm (n: int) (**r [rd = r1 >> n] (signed) *) - | Oshru (**r [rd = r1 >> r2] (unsigned) *) - | Oshruimm (n: int) (**r [rd = r1 >> n] (unsigned) *) + | Oshr (**r [rd = r1 >>s r2] (signed) *) + | Oshrimm (n: int) (**r [rd = r1 >>s n] (signed) *) + | Oshru (**r [rd = r1 >>u r2] (unsigned) *) + | Oshruimm (n: int) (**r [rd = r1 >>x n] (unsigned) *) | Oshrximm (n: int) (**r [rd = r1 / 2^n] (signed) *) | Ororimm (n: int) (**r rotate right immediate *) | Omadd (**r [rd = rd + r1 * r2] *) @@ -158,8 +158,8 @@ Inductive operation : Type := | Onxorl (**r [rd = ~(r1 ^ r2)] *) | Onxorlimm (n: int64) (**r [rd = ~(r1 ^ n)] *) | Onotl (**r [rd = ~r1] *) - | Oandnl (**r [rd = (~r1) ^ r2] *) - | Oandnlimm (n: int64) (**r [rd = (~r1) ^ n] *) + | Oandnl (**r [rd = (~r1) & r2] *) + | Oandnlimm (n: int64) (**r [rd = (~r1) & n] *) | Oornl (**r [rd = (~r1) | r2] *) | Oornlimm (n: int64) (**r [rd = (~r1) | n] *) | Oshll (**r [rd = r1 << r2] *) diff --git a/mppa_k1c/PrintOp.ml b/mppa_k1c/PrintOp.ml index 575fa94f..7c408cdf 100644 --- a/mppa_k1c/PrintOp.ml +++ b/mppa_k1c/PrintOp.ml @@ -72,7 +72,7 @@ let int_of_s14 = function | SHIFT3 -> 3 | SHIFT4 -> 4 -let print_operation reg pp = function +let print_operation reg pp op = match op with | Omove, [r1] -> reg pp r1 | Ointconst n, [] -> fprintf pp "%ld" (camlint_of_coqint n) | Olongconst n, [] -> fprintf pp "%LdL" (camlint64_of_coqint n) @@ -86,9 +86,15 @@ let print_operation reg pp = function | Ocast16signed, [r1] -> fprintf pp "int16signed(%a)" reg r1 | Oadd, [r1;r2] -> fprintf pp "%a + %a" reg r1 reg r2 | Oaddimm n, [r1] -> fprintf pp "%a + %ld" reg r1 (camlint_of_coqint n) + | Oaddx(s14), [r1; r2] -> fprintf pp "(%a << %d) + %a" reg r1 (int_of_s14 s14) reg r2 + | Oaddximm(s14, imm), [r1] -> fprintf pp "(%a << %d) + %ld" reg r1 (int_of_s14 s14) (camlint_of_coqint imm) | Oneg, [r1] -> fprintf pp "-(%a)" reg r1 | Osub, [r1;r2] -> fprintf pp "%a - %a" reg r1 reg r2 + | Orevsubimm(imm), [r1] -> fprintf pp "%ld - %a" (camlint_of_coqint imm) reg r1 + | Orevsubx(s14), [r1; r2] -> fprintf pp "%a - (%a << %d)" reg r2 reg r1 (int_of_s14 s14) + | Orevsubximm(s14, imm), [r1] -> fprintf pp "%ld - (%a << %d)" (camlint_of_coqint imm) reg r1 (int_of_s14 s14) | Omul, [r1;r2] -> fprintf pp "%a * %a" reg r1 reg r2 + | Omulimm(imm), [r1] -> fprintf pp "%a * %ld" reg r1 (camlint_of_coqint imm) | Omulhs, [r1;r2] -> fprintf pp "%a *hs %a" reg r1 reg r2 | Omulhu, [r1;r2] -> fprintf pp "%a *hu %a" reg r1 reg r2 | Odiv, [r1;r2] -> fprintf pp "%a /s %a" reg r1 reg r2 @@ -101,6 +107,13 @@ let print_operation reg pp = function | Oorimm n, [r1] -> fprintf pp "%a | %ld" reg r1 (camlint_of_coqint n) | Oxor, [r1;r2] -> fprintf pp "%a ^ %a" reg r1 reg r2 | Oxorimm n, [r1] -> fprintf pp "%a ^ %ld" reg r1 (camlint_of_coqint n) + | Onxor, [r1;r2] -> fprintf pp "~(%a ^ %a)" reg r1 reg r2 + | Onxorimm n, [r1] -> fprintf pp "~(%a ^ %ld)" reg r1 (camlint_of_coqint n) + | Onot, [r1] -> fprintf pp "~%a" reg r1 + | Oandn, [r1; r2] -> fprintf pp "(~%a) & %a" reg r1 reg r2 + | Oandnimm n, [r1] -> fprintf pp "(~%a) & %ld" reg r1 (camlint_of_coqint n) + | Oorn, [r1;r2] -> fprintf pp "(~%a) | %a" reg r1 reg r2 + | Oornimm n, [r1] -> fprintf pp "(~%a) | %ld" reg r1 (camlint_of_coqint n) | Oshl, [r1;r2] -> fprintf pp "%a << %a" reg r1 reg r2 | Oshlimm n, [r1] -> fprintf pp "%a << %ld" reg r1 (camlint_of_coqint n) | Oshr, [r1;r2] -> fprintf pp "%a >>s %a" reg r1 reg r2 @@ -108,6 +121,10 @@ let print_operation reg pp = function | Oshru, [r1;r2] -> fprintf pp "%a >>u %a" reg r1 reg r2 | Oshruimm n, [r1] -> fprintf pp "%a >>u %ld" reg r1 (camlint_of_coqint n) | Oshrximm n, [r1] -> fprintf pp "%a >>x %ld" reg r1 (camlint_of_coqint n) + | Ororimm n, [r1] -> fprintf pp "(%a ror %ld)" reg r1 (camlint_of_coqint n) + | Omadd, [r1; r2; r3] -> fprintf pp "%a + %a * %a" reg r1 reg r2 reg r3 + | Omaddimm imm, [r1; r2] -> fprintf pp "%a + %a * %ld" reg r1 reg r2 (camlint_of_coqint imm) + | Omsub, [r1; r2; r3] -> fprintf pp "%a - %a * %a" reg r1 reg r2 reg r3 | Omakelong, [r1;r2] -> fprintf pp "makelong(%a,%a)" reg r1 reg r2 | Olowlong, [r1] -> fprintf pp "lowlong(%a)" reg r1 @@ -116,9 +133,15 @@ let print_operation reg pp = function | Ocast32unsigned, [r1] -> fprintf pp "long32unsigned(%a)" reg r1 | Oaddl, [r1;r2] -> fprintf pp "%a +l %a" reg r1 reg r2 | Oaddlimm n, [r1] -> fprintf pp "%a +l %Ld" reg r1 (camlint64_of_coqint n) + | Oaddxl(s14), [r1; r2] -> fprintf pp "(%a < fprintf pp "(%a < fprintf pp "%Ld -l %a" (camlint64_of_coqint imm) reg r1 + | Orevsubxl(s14), [r1; r2] -> fprintf pp "%a -l (%a < fprintf pp "%Ld -l (%a < fprintf pp "-l (%a)" reg r1 | Osubl, [r1;r2] -> fprintf pp "%a -l %a" reg r1 reg r2 | Omull, [r1;r2] -> fprintf pp "%a *l %a" reg r1 reg r2 + | Omullimm(imm), [r1] -> fprintf pp "%a *l %Ld" reg r1 (camlint64_of_coqint imm) | Omullhs, [r1;r2] -> fprintf pp "%a *lhs %a" reg r1 reg r2 | Omullhu, [r1;r2] -> fprintf pp "%a *lhu %a" reg r1 reg r2 | Odivl, [r1;r2] -> fprintf pp "%a /ls %a" reg r1 reg r2 @@ -129,8 +152,17 @@ let print_operation reg pp = function | Oandlimm n, [r1] -> fprintf pp "%a &l %Ld" reg r1 (camlint64_of_coqint n) | Oorl, [r1;r2] -> fprintf pp "%a |l %a" reg r1 reg r2 | Oorlimm n, [r1] -> fprintf pp "%a |l %Ld" reg r1 (camlint64_of_coqint n) + | Onorl, [r1; r2] -> fprintf pp "~(%a |l %a)" reg r1 reg r2 + | Onorlimm n, [r1] -> fprintf pp "~(%a |l %Ld)" reg r1 (camlint64_of_coqint n) | Oxorl, [r1;r2] -> fprintf pp "%a ^l %a" reg r1 reg r2 | Oxorlimm n, [r1] -> fprintf pp "%a ^l %Ld" reg r1 (camlint64_of_coqint n) + | Onxorl, [r1;r2] -> fprintf pp "~(%a ^l %a)" reg r1 reg r2 + | Onxorlimm n, [r1] -> fprintf pp "~(%a ^l %Ld)" reg r1 (camlint64_of_coqint n) + | Onotl, [r1] -> fprintf pp "~%a" reg r1 + | Oandnl, [r1;r2] -> fprintf pp "(~%a) &l %a" reg r1 reg r2 + | Oandnlimm n, [r1] -> fprintf pp "(~%a) &l %Ld" reg r1 (camlint64_of_coqint n) + | Oornl, [r1;r2] -> fprintf pp "(~%a) |l %a" reg r1 reg r2 + | Oornlimm n, [r1;r2] -> fprintf pp "(~%a) |l %Ld" reg r1 (camlint64_of_coqint n) | Oshll, [r1;r2] -> fprintf pp "%a < fprintf pp "%a < fprintf pp "%a >>ls %a" reg r1 reg r2 @@ -138,6 +170,9 @@ let print_operation reg pp = function | Oshrlu, [r1;r2] -> fprintf pp "%a >>lu %a" reg r1 reg r2 | Oshrluimm n, [r1] -> fprintf pp "%a >>lu %ld" reg r1 (camlint_of_coqint n) | Oshrxlimm n, [r1] -> fprintf pp "%a >>lx %ld" reg r1 (camlint_of_coqint n) + | Omaddl, [r1; r2; r3] -> fprintf pp "%a +l %a *l %a" reg r1 reg r2 reg r3 + | Omaddlimm imm, [r1; r2] -> fprintf pp "%a +l %a *l %Ld" reg r1 reg r2 (camlint64_of_coqint imm) + | Omsubl, [r1; r2; r3] -> fprintf pp "%a -l %a *l %a" reg r1 reg r2 reg r3 | Onegf, [r1] -> fprintf pp "negf(%a)" reg r1 | Oabsf, [r1] -> fprintf pp "absf(%a)" reg r1 @@ -155,14 +190,14 @@ let print_operation reg pp = function | Ofloatofsingle, [r1] -> fprintf pp "floatofsingle(%a)" reg r1 | Ointoffloat, [r1] -> fprintf pp "intoffloat(%a)" reg r1 | Ointuoffloat, [r1] -> fprintf pp "intuoffloat(%a)" reg r1 - | Olongoffloat, [r1] -> fprintf pp "longoffloat(%a)" reg r1 - | Olonguoffloat, [r1] -> fprintf pp "longuoffloat(%a)" reg r1 - | Ofloatoflong, [r1] -> fprintf pp "floatoflong(%a)" reg r1 - | Ofloatoflongu, [r1] -> fprintf pp "floatoflongu(%a)" reg r1 | Ointofsingle, [r1] -> fprintf pp "intofsingle(%a)" reg r1 | Ointuofsingle, [r1] -> fprintf pp "intuofsingle(%a)" reg r1 | Osingleofint, [r1] -> fprintf pp "singleofint(%a)" reg r1 | Osingleofintu, [r1] -> fprintf pp "singleofintu(%a)" reg r1 + | Olongoffloat, [r1] -> fprintf pp "longoffloat(%a)" reg r1 + | Olonguoffloat, [r1] -> fprintf pp "longuoffloat(%a)" reg r1 + | Ofloatoflong, [r1] -> fprintf pp "floatoflong(%a)" reg r1 + | Ofloatoflongu, [r1] -> fprintf pp "floatoflongu(%a)" reg r1 | Olongofsingle, [r1] -> fprintf pp "longofsingle(%a)" reg r1 | Olonguofsingle, [r1] -> fprintf pp "longuofsingle(%a)" reg r1 | Osingleoflong, [r1] -> fprintf pp "singleoflong(%a)" reg r1 @@ -184,24 +219,6 @@ let print_operation reg pp = function | Osellimm(cond0, imm), [r1; rc] -> print_condition0 reg pp cond0 rc; fprintf pp " ? %a :l %Ld" reg r1 (camlint64_of_coqint imm) - | Oaddx(s14), [r1; r2] -> fprintf pp "(%a << %d) + %a" reg r1 (int_of_s14 s14) reg r2 - | Oaddximm(s14, imm), [r1] -> fprintf pp "(%a << %d) + %ld" reg r1 (int_of_s14 s14) (camlint_of_coqint imm) - | Oaddxl(s14), [r1; r2] -> fprintf pp "(%a < fprintf pp "(%a < fprintf pp "%ld - %a" (camlint_of_coqint imm) reg r1 - | Orevsubximm(s14, imm), [r1] -> fprintf pp "%ld - (%a << %d)" (camlint_of_coqint imm) reg r1 (int_of_s14 s14) - | Orevsublimm(imm), [r1] -> fprintf pp "%Ld -l %a" (camlint64_of_coqint imm) reg r1 - | Orevsubxlimm(s14, imm), [r1] -> fprintf pp "%Ld -l (%a < fprintf pp "%a - (%a << %d)" reg r2 reg r1 (int_of_s14 s14) - | Orevsubxl(s14), [r1; r2] -> fprintf pp "%a -l (%a < fprintf pp "%a * %ld" reg r1 (camlint_of_coqint imm) - | Omullimm(imm), [r1] -> fprintf pp "%a *l %Ld" reg r1 (camlint64_of_coqint imm) - | Omadd, [r1; r2; r3] -> fprintf pp "%a + %a * %a" reg r1 reg r2 reg r3 - | Omaddl, [r1; r2; r3] -> fprintf pp "%a +l %a *l %a" reg r1 reg r2 reg r3 - | (Omaddimm imm), [r1; r2] -> fprintf pp "%a + %a * %ld" reg r1 reg r2 (camlint_of_coqint imm) - | (Omaddlimm imm), [r1; r2] -> fprintf pp "%a +l %a *l %Ld" reg r1 reg r2 (camlint64_of_coqint imm) - | Omsub, [r1; r2; r3] -> fprintf pp "%a - %a * %a" reg r1 reg r2 reg r3 - | Omsubl, [r1; r2; r3] -> fprintf pp "%a -l %a *l %a" reg r1 reg r2 reg r3 | _, _ -> fprintf pp "" let print_addressing reg pp = function -- cgit From a11f3b87e0535b6c7953c74d00d91fb7d7fbb21b Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 24 Jul 2019 11:05:56 +0200 Subject: (#145) Fix on RTL dumps --- mppa_k1c/PrintOp.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/mppa_k1c/PrintOp.ml b/mppa_k1c/PrintOp.ml index 7c408cdf..67f87000 100644 --- a/mppa_k1c/PrintOp.ml +++ b/mppa_k1c/PrintOp.ml @@ -222,8 +222,9 @@ let print_operation reg pp op = match op with | _, _ -> fprintf pp "" let print_addressing reg pp = function - | Aindexed n, [r1] -> fprintf pp "%a + %Ld" reg r1 (camlint64_of_ptrofs n) + | Aindexed2XS scale, [r1;r2] -> fprintf pp "%a + (%a << %ld)" reg r1 reg r2 (camlint_of_coqint scale) | Aindexed2, [r1;r2] -> fprintf pp "%a + %a" reg r1 reg r2 + | Aindexed n, [r1] -> fprintf pp "%a + %Ld" reg r1 (camlint64_of_ptrofs n) | Aglobal(id, ofs), [] -> fprintf pp "\"%s\" + %Ld" (extern_atom id) (camlint64_of_ptrofs ofs) | Ainstack ofs, [] -> fprintf pp "stack(%Ld)" (camlint64_of_ptrofs ofs) -- cgit From 4ee5d47c502e05deed69eb8ddf183384a86ffd05 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 24 Jul 2019 17:01:41 +0200 Subject: Minor fix for the measurements macros --- test/monniaux/cycles.h | 2 +- test/monniaux/rules.mk | 7 ++++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/test/monniaux/cycles.h b/test/monniaux/cycles.h index 8012a013..21541145 100644 --- a/test/monniaux/cycles.h +++ b/test/monniaux/cycles.h @@ -46,5 +46,5 @@ static inline cycle_t get_cycle(void) { return 0; } #ifdef MAX_MEASURES #define TIMEINIT(i) {_last_stop[i] = get_cycle();} #define TIMESTOP(i) {cycle_t cur = get_cycle(); _total_cycles[i] += cur - _last_stop[i]; _last_stop[i] = cur;} - #define TIMEPRINT(n) { for (int i = 0; i <= n; i++) printf("(%d) cycles: %" PRIu64 "\n", i, _total_cycles[i]); } + #define TIMEPRINT(n) { for (int i = 0; i <= n; i++) printf("%d cycles: %" PRIu64 "\n", i, _total_cycles[i]); } #endif diff --git a/test/monniaux/rules.mk b/test/monniaux/rules.mk index 4dfeac3b..9d05b4d6 100644 --- a/test/monniaux/rules.mk +++ b/test/monniaux/rules.mk @@ -12,6 +12,7 @@ CLOCK=../clock # Maximum amount of time measures (see cycles.h) MAX_MEASURES=10 +MEASURES?=time # Flags common to both compilers, then to gcc, then to ccomp ALL_CFLAGS+=-Wall -D__K1C_COS__ -DMAX_MEASURES=$(MAX_MEASURES) @@ -28,12 +29,12 @@ EXECUTE_CYCLES?=k1-cluster --syscall=libstd_scalls.so --cycle-based -- # You can define up to GCC4FLAGS and CCOMP4FLAGS GCC0FLAGS?= -GCC1FLAGS?=$(ALL_GCCFLAGS) -O1 +GCC1FLAGS?=$(ALL_GCCFLAGS) -O1 -g GCC2FLAGS?=$(ALL_GCCFLAGS) -O2 GCC3FLAGS?=$(ALL_GCCFLAGS) -O3 GCC4FLAGS?= CCOMP0FLAGS?= -CCOMP1FLAGS?=$(ALL_CCOMPFLAGS) -O1 +CCOMP1FLAGS?=$(ALL_CCOMPFLAGS) -O1 -g CCOMP2FLAGS?=$(ALL_CCOMPFLAGS) CCOMP3FLAGS?= CCOMP4FLAGS?= @@ -131,7 +132,7 @@ endif measures.csv: $(OUTFILES) @echo $(FIRSTLINE) > $@ - @for i in "$(MEASURES)"; do\ + @for i in $(MEASURES); do\ first=$$(grep "$$i cycles" $(firstword $(OUTFILES)));\ if test ! -z "$$first"; then\ if [ "$$i" != "time" ]; then\ -- cgit From 98c22a6f37c7230faf80b6366aaa1c2476f9e67c Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 25 Jul 2019 14:29:28 +0200 Subject: (#139) - Mise à jour du code Coq, oracle MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- mppa_k1c/PostpassScheduling.v | 55 ++++++++++++++++++++++++++++++------ mppa_k1c/PostpassSchedulingOracle.ml | 14 +++++++-- mppa_k1c/PostpassSchedulingproof.v | 2 +- 3 files changed, 59 insertions(+), 12 deletions(-) diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v index 15cb4c48..76757eba 100644 --- a/mppa_k1c/PostpassScheduling.v +++ b/mppa_k1c/PostpassScheduling.v @@ -19,7 +19,7 @@ Local Open Scope error_monad_scope. (** Oracle taking as input a basic block, returns a schedule expressed as a list of bundles *) -Axiom schedule: bblock -> list bblock. +Axiom schedule: bblock -> (list (list basic)) * option control. Extract Constant schedule => "PostpassSchedulingOracle.schedule". @@ -333,10 +333,49 @@ Proof. apply stick_header_concat_all. assumption. Qed. +Program Definition make_bblock_from_basics lb := + match lb with + | nil => Error (msg "PostpassScheduling.make_bblock_from_basics") + | b :: lb => OK {| header := nil; body := b::lb; exit := None |} + end. + +Fixpoint schedule_to_bblocks_nocontrol llb := + match llb with + | nil => OK nil + | lb :: llb => do bb <- make_bblock_from_basics lb; + do lbb <- schedule_to_bblocks_nocontrol llb; + OK (bb :: lbb) + end. +Program Definition make_bblock_from_basics_and_control lb c := + match c with + | PExpand (Pbuiltin _ _ _) => Error (msg "PostpassScheduling.make_bblock_from_basics_and_control") + | PCtlFlow cf => OK {| header := nil; body := lb; exit := Some (PCtlFlow cf) |} + end. +Next Obligation. + apply wf_bblock_refl. constructor. + - right. discriminate. + - discriminate. +Qed. + +Fixpoint schedule_to_bblocks_wcontrol llb c := + match llb with + | nil => OK ((bblock_single_inst (PControl c)) :: nil) + | lb :: nil => do bb <- make_bblock_from_basics_and_control lb c; OK (bb :: nil) + | lb :: llb => do bb <- make_bblock_from_basics lb; + do lbb <- schedule_to_bblocks_wcontrol llb c; + OK (bb :: lbb) + end. + +Definition schedule_to_bblocks (llb: list (list basic)) (oc: option control) : res (list bblock) := + match oc with + | None => schedule_to_bblocks_nocontrol llb + | Some c => schedule_to_bblocks_wcontrol llb c + end. -Definition do_schedule (bb: bblock) : list bblock := - if (Z.eqb (size bb) 1) then bb::nil else schedule bb. +Definition do_schedule (bb: bblock) : res (list bblock) := + if (Z.eqb (size bb) 1) then OK (bb::nil) + else match (schedule bb) with (llb, oc) => schedule_to_bblocks llb oc end. Definition verify_par_bblock (bb: bblock) : res unit := if (bblock_para_check bb) then OK tt else Error (msg "PostpassScheduling.verify_par_bblock"). @@ -350,7 +389,7 @@ Fixpoint verify_par (lbb: list bblock) := Definition verified_schedule_nob (bb : bblock) : res (list bblock) := let bb' := no_header bb in let bb'' := Peephole.optimize_bblock bb' in - let lbb := do_schedule bb'' in + do lbb <- do_schedule bb''; do tbb <- concat_all lbb; do sizecheck <- verify_size bb lbb; do schedcheck <- verify_schedule bb' tbb; @@ -363,7 +402,7 @@ Lemma verified_schedule_nob_size: Proof. intros. monadInv H. erewrite <- stick_header_code_size; eauto. apply verify_size_size. - destruct x0; try discriminate. assumption. + destruct x1; try discriminate. assumption. Qed. Lemma verified_schedule_nob_no_header_in_middle: @@ -382,7 +421,7 @@ Lemma verified_schedule_nob_header: /\ Forall (fun b => header b = nil) lbb. Proof. intros. split. - - monadInv H. unfold stick_header_code in EQ2. destruct (hd_error _); try discriminate. inv EQ2. + - monadInv H. unfold stick_header_code in EQ3. destruct (hd_error _); try discriminate. inv EQ3. simpl. reflexivity. - apply verified_schedule_nob_no_header_in_middle in H. assumption. Qed. @@ -435,8 +474,8 @@ Proof. exploit stick_header_code_concat_all; eauto. intros (tbb & CONC & STH). exists tbb. split; auto. - rewrite verify_schedule_no_header in EQ0. erewrite stick_header_verify_schedule in EQ0; eauto. - eapply bblock_simub_correct; eauto. unfold verify_schedule in EQ0. + rewrite verify_schedule_no_header in EQ2. erewrite stick_header_verify_schedule in EQ2; eauto. + eapply bblock_simub_correct; eauto. unfold verify_schedule in EQ2. destruct (bblock_simub _ _); auto; try discriminate. Qed. diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index fd03a80c..40f1d9c7 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -961,10 +961,18 @@ let smart_schedule bb = in bundles @ (f lbb) in f lbb -(** Called schedule function from Coq *) - -let schedule bb = +let bblock_to_bundles bb = if debug then (eprintf "###############################\n"; Printf.eprintf "SCHEDULING\n"; print_bb stderr bb); (* print_problem (build_problem bb); *) if Compopts.optim_postpass () then smart_schedule bb else dumb_schedule bb +(** To deal with the Coq Axiom schedule : bblock -> (list (list basic)) * option control *) + +let rec bundles_to_coq_schedule = function + | [] -> ([], None) + | bb :: [] -> ([bb.body], bb.exit) + | bb :: lbb -> let (llb, oc) = bundles_to_coq_schedule lbb in (bb.body :: llb, oc) + +(** Called schedule function from Coq *) + +let schedule bb = let toto = bundles_to_coq_schedule @@ bblock_to_bundles bb in toto diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 5d4fc881..0edaf4e2 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -798,7 +798,7 @@ Lemma verified_schedule_nob_checks_alls_bundles bb lb bundle: List.In bundle lb -> verify_par_bblock bundle = OK tt. Proof. unfold verified_schedule_nob. intros H; - monadInv H. destruct x3. + monadInv H. destruct x4. intros; eapply verified_par_checks_alls_bundles; eauto. Qed. -- cgit From 211382d21013c038c3c716454fcfa5a375dba8ba Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 30 Jul 2019 11:15:15 +0200 Subject: (#139) - Predicate is_concat --- mppa_k1c/PostpassScheduling.v | 15 ++++++++------- mppa_k1c/PostpassSchedulingproof.v | 2 +- 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v index 76757eba..8b6de1e2 100644 --- a/mppa_k1c/PostpassScheduling.v +++ b/mppa_k1c/PostpassScheduling.v @@ -208,7 +208,8 @@ Proof. + apply IHlbb in EQ. assumption. Qed. - +Inductive is_concat : bblock -> list bblock -> Prop := + | mk_is_concat: forall tbb lbb, concat_all lbb = OK tbb -> is_concat tbb lbb. Definition verify_schedule (bb bb' : bblock) : res unit := match bblock_simub bb bb' with @@ -466,14 +467,14 @@ Qed. Lemma verified_schedule_nob_correct: forall ge f bb lbb, verified_schedule_nob bb = OK lbb -> - exists tbb, - concat_all lbb = OK tbb + exists tbb, + is_concat tbb lbb /\ bblock_simu ge f bb tbb. Proof. intros. monadInv H. exploit stick_header_code_concat_all; eauto. intros (tbb & CONC & STH). - exists tbb. split; auto. + exists tbb. split; auto. constructor; auto. rewrite verify_schedule_no_header in EQ2. erewrite stick_header_verify_schedule in EQ2; eauto. eapply bblock_simub_correct; eauto. unfold verify_schedule in EQ2. destruct (bblock_simub _ _); auto; try discriminate. @@ -482,13 +483,13 @@ Qed. Theorem verified_schedule_correct: forall ge f bb lbb, verified_schedule bb = OK lbb -> - exists tbb, - concat_all lbb = OK tbb + exists tbb, + is_concat tbb lbb /\ bblock_simu ge f bb tbb. Proof. intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i. all: try (eapply verified_schedule_nob_correct; eauto; fail). - inv H. eexists. split; simpl; auto. constructor; auto. + inv H. eexists. split; simpl; auto. constructor; auto. simpl; auto. constructor; auto. Qed. Lemma verified_schedule_builtin_idem: diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 0edaf4e2..2207a2fa 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -736,7 +736,7 @@ Proof. induction 1; intros; inv MS. - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF. exploit transf_find_bblock; eauto. intros (lbb & VES & c & TAIL). - exploit verified_schedule_correct; eauto. intros (tbb & CONC & BBEQ). + exploit verified_schedule_correct; eauto. intros (tbb & CONC & BBEQ). inv CONC. rename H3 into CONC. assert (NOOV: size_blocks x.(fn_blocks) <= Ptrofs.max_unsigned). eapply transf_function_no_overflow; eauto. -- cgit From 5b4560bd853cbcf1ef195da1b625f37609ec00ec Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 30 Jul 2019 11:33:51 +0200 Subject: (#139) - Quelques renommages --- mppa_k1c/Asmblock.v | 2 +- mppa_k1c/Asmblockdeps.v | 10 +++++----- mppa_k1c/Asmvliw.v | 8 ++++---- mppa_k1c/PostpassSchedulingproof.v | 4 ++-- 4 files changed, 12 insertions(+), 12 deletions(-) diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index ddb7ce7d..0a25e81a 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -286,7 +286,7 @@ Definition exec_store_regxs (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: (** * basic instructions *) -Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome := parexec_basic_instr ge bi rs rs m m. +Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome := bstep ge bi rs rs m m. Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome := match body with diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 9855afa2..a7fa5cff 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -846,7 +846,7 @@ Theorem bisimu_par_wio_basic ge fn rsr rsw mr mw sr sw bi: Ge = Genv ge fn -> match_states (State rsr mr) sr -> match_states (State rsw mw) sw -> - match_outcome (parexec_basic_instr ge bi rsr rsw mr mw) (inst_prun Ge (trans_basic bi) sw sr sr). + match_outcome (bstep ge bi rsr rsw mr mw) (inst_prun Ge (trans_basic bi) sw sr sr). Proof. (* a little tactic to automate reasoning on preg_eq *) @@ -1004,7 +1004,7 @@ Proof. induction bdy as [|i bdy]; simpl; eauto. intros. exploit (bisimu_par_wio_basic ge fn rsr rsw mr mw sr sw i); eauto. - destruct (parexec_basic_instr _ _ _ _ _ _); simpl. + destruct (bstep _ _ _ _ _ _); simpl. - intros (s' & X1 & X2). rewrite X1; simpl; eauto. - intros X; rewrite X; simpl; auto. Qed. @@ -1015,7 +1015,7 @@ Theorem bisimu_par_control ex sz aux ge fn rsr rsw mr mw sr sw: match_states (State rsw mw) sw -> match_outcome (parexec_control ge fn ex (incrPC (Ptrofs.repr sz) rsr) (rsw#PC <- aux) mw) (inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr). Proof. - intros GENV MSR MSW; unfold parexec_exit. + intros GENV MSR MSW; unfold estep. simpl in *. inv MSR. inv MSW. destruct ex. - destruct c; destruct i; try discriminate; simpl. @@ -1071,9 +1071,9 @@ Theorem bisimu_par_exit ex sz ge fn rsr rsw mr mw sr sw: Ge = Genv ge fn -> match_states (State rsr mr) sr -> match_states (State rsw mw) sw -> - match_outcome (parexec_exit ge fn ex (Ptrofs.repr sz) rsr rsw mw) (inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr). + match_outcome (estep ge fn ex (Ptrofs.repr sz) rsr rsw mw) (inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr). Proof. - intros; unfold parexec_exit. + intros; unfold estep. exploit (bisimu_par_control ex sz rsw#PC ge fn rsr rsw mr mw sr sw); eauto. cutrewrite (rsw # PC <- (rsw PC) = rsw); auto. apply extensionality. intros; destruct x; simpl; auto. diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index c5b7db45..c6dd85f4 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -1355,7 +1355,7 @@ Definition store_chunk n := (** * basic instructions *) -Definition parexec_basic_instr (bi: basic) (rsr rsw: regset) (mr mw: mem) := +Definition bstep (bi: basic) (rsr rsw: regset) (mr mw: mem) := match bi with | PArith ai => Next (parexec_arith_instr ai rsr rsw) mw @@ -1414,7 +1414,7 @@ Fixpoint parexec_wio_body (body: list basic) (rsr rsw: regset) (mr mw: mem) := match body with | nil => Next rsw mw | bi::body' => - match parexec_basic_instr bi rsr rsw mr mw with + match bstep bi rsr rsw mr mw with | Next rsw mw => parexec_wio_body body' rsr rsw mr mw | Stuck => Stuck end @@ -1550,12 +1550,12 @@ Definition incrPC size_b (rs: regset) := rs#PC <- (Val.offset_ptr rs#PC size_b). (** parallel execution of the exit instruction of a bundle *) -Definition parexec_exit (f: function) ext size_b (rsr rsw: regset) (mw: mem) +Definition estep (f: function) ext size_b (rsr rsw: regset) (mw: mem) := parexec_control f ext (incrPC size_b rsr) rsw mw. Definition parexec_wio f bdy ext size_b (rs: regset) (m: mem): outcome := match parexec_wio_body bdy rs rs m m with - | Next rsw mw => parexec_exit f ext size_b rs rsw mw + | Next rsw mw => estep f ext size_b rs rsw mw | Stuck => Stuck end. diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 2207a2fa..21af276b 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -240,7 +240,7 @@ Lemma exec_basic_instr_pc_var: exec_basic_instr ge i rs m = Next rs' m' -> exec_basic_instr ge i (rs # PC <- v) m = Next (rs' # PC <- v) m'. Proof. - intros. unfold exec_basic_instr in *. unfold parexec_basic_instr in *. destruct i. + intros. unfold exec_basic_instr in *. unfold bstep in *. destruct i. - unfold exec_arith_instr in *. destruct i; destruct i. all: try (exploreInst; inv H; apply next_eq; auto; apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate). @@ -681,7 +681,7 @@ Lemma transf_exec_basic_instr: forall i rs m, exec_basic_instr ge i rs m = exec_basic_instr tge i rs m. Proof. intros. pose symbol_address_preserved. - unfold exec_basic_instr. unfold parexec_basic_instr. exploreInst; simpl; auto; try congruence. + unfold exec_basic_instr. unfold bstep. exploreInst; simpl; auto; try congruence. unfold parexec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence. Qed. -- cgit From ce33586e40bf7be637b932d363275b9d5761a3a0 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 30 Jul 2019 16:46:16 +0200 Subject: (#156) - Un peu de cleaning et de doc --- mppa_k1c/Archi.v | 3 +- mppa_k1c/Asm.v | 50 ++------- mppa_k1c/Asmaux.v | 2 +- mppa_k1c/Asmblock.v | 33 +----- mppa_k1c/Asmblockdeps.v | 35 +++--- mppa_k1c/Asmblockgen.v | 66 ++---------- mppa_k1c/Asmblockgenproof0.v | 86 ++------------- mppa_k1c/Asmblockgenproof1.v | 246 +------------------------------------------ mppa_k1c/Asmgenproof.v | 4 +- mppa_k1c/Asmvliw.v | 25 +---- 10 files changed, 53 insertions(+), 497 deletions(-) diff --git a/mppa_k1c/Archi.v b/mppa_k1c/Archi.v index 113f5d51..96571841 100644 --- a/mppa_k1c/Archi.v +++ b/mppa_k1c/Archi.v @@ -14,10 +14,9 @@ (* *) (* *********************************************************************) -(** Architecture-dependent parameters for RISC-V *) +(** Architecture-dependent parameters for MPPA K1c. Mostly copied from the Risc-V backend *) Require Import ZArith. -(*From Flocq*) Require Import Binary Bits. Definition ptr64 := true. diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 620aa91e..1964e5f8 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -15,7 +15,13 @@ (* *) (* *********************************************************************) -(** Abstract syntax and semantics for K1c assembly language. *) +(** * Abstract syntax for K1c textual assembly language. + + Each emittable instruction is defined here. ';;' is also defined as an instruction. + The goal of this representation is to stay compatible with the rest of the generic backend of CompCert + We define [unfold : list bblock -> list instruction] + An Asm function is then defined as : [fn_sig], [fn_blocks], [fn_code], and a proof of [unfold fn_blocks = fn_code] + [fn_code] has no semantic. Instead, the semantic of Asm is given by using the AsmVLIW semantic on [fn_blocks] *) Require Import Coqlib. Require Import Maps. @@ -57,10 +63,6 @@ Inductive instruction : Type := | Psemi (**r semi colon separating bundles *) | Pnop (**r instruction that does nothing *) - (** builtins *) - | Pclzll (rd rs: ireg) - | Pstsud (rd rs1 rs2: ireg) - (** Control flow instructions *) | Pget (rd: ireg) (rs: preg) (**r get system register *) | Pset (rd: preg) (rs: ireg) (**r set system register *) @@ -101,6 +103,8 @@ Inductive instruction : Type := | Pafaddw (addr: ireg) (incr_res: ireg) | Palclrd (dst: ireg) (addr: ireg) | Palclrw (dst: ireg) (addr: ireg) + | Pclzll (rd rs: ireg) + | Pstsud (rd rs1 rs2: ireg) (** Loads **) | Plb (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte *) @@ -571,12 +575,6 @@ Definition genv := Genv.t fundef unit. Definition function_proj (f: function) := Asmvliw.mkfunction (fn_sig f) (fn_blocks f). -(* -Definition fundef_proj (fu: fundef) : Asmblock.fundef := transf_fundef function_proj fu. - -Definition program_proj (p: program) : Asmblock.program := transform_program fundef_proj p. - *) - Definition fundef_proj (fu: fundef) : Asmvliw.fundef := match fu with | Internal f => Internal (function_proj f) @@ -650,35 +648,6 @@ Proof. rewrite transf_function_proj. auto. Qed. -(* Definition transf_globdef (gd: globdef Asmblock.fundef unit) : globdef fundef unit := - match gd with - | Gfun f => Gfun (transf_fundef f) - | Gvar gu => Gvar gu - end. - -Lemma transf_globdef_proj: forall gd, globdef_proj (transf_globdef gd) = gd. -Proof. - intros gd. destruct gd as [f|v]; simpl; auto. - rewrite transf_fundef_proj; auto. -Qed. - -Fixpoint transf_prog_defs (l: list (ident * globdef Asmblock.fundef unit)) - : list (ident * globdef fundef unit) := - match l with - | nil => nil - | (i, gd) :: l => (i, transf_globdef gd) :: transf_prog_defs l - end. - -Lemma transf_prog_proj: forall p, prog_defs p = prog_defs_proj (transf_prog_defs (prog_defs p)). -Proof. - intros p. destruct p as [defs pub main]. simpl. - induction defs; simpl; auto. - destruct a as [i gd]. simpl. - rewrite transf_globdef_proj. - congruence. -Qed. - *) - Definition transf_program : Asmvliw.program -> program := transform_program transf_fundef. Lemma program_equals {A B: Type} : forall (p1 p2: AST.program A B), @@ -716,7 +685,6 @@ Proof. intros. congruence. Qed. -(* I think it is a special case of Asmblock -> Asm. Very handy to have *) Lemma match_program_transf: forall p tp, match_prog p tp -> transf_program p = tp. Proof. diff --git a/mppa_k1c/Asmaux.v b/mppa_k1c/Asmaux.v index 85359658..94b39f4e 100644 --- a/mppa_k1c/Asmaux.v +++ b/mppa_k1c/Asmaux.v @@ -1,5 +1,5 @@ Require Import Asm. Require Import AST. -(* Constant only needed by Asmexpandaux.ml *) +(** Constant only needed by Asmexpandaux.ml *) Program Definition dummy_function := {| fn_code := nil; fn_sig := signature_main; fn_blocks := nil |}. diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 0a25e81a..9b4489c5 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -15,7 +15,7 @@ (* *) (* *********************************************************************) -(** Abstract syntax and semantics for K1c assembly language. *) +(** Sequential block semantics for K1c assembly. The syntax is given in AsmVLIW *) Require Import Coqlib. Require Import Maps. @@ -172,7 +172,6 @@ Proof. Qed. Ltac bblock_auto_correct := (apply non_empty_bblock_refl; try discriminate; try (left; discriminate); try (right; discriminate)). -(* Local Obligation Tactic := bblock_auto_correct. *) Lemma Istrue_proof_irrelevant (b: bool): forall (p1 p2:Is_true b), p1=p2. Proof. @@ -250,9 +249,6 @@ Proof. intros. destruct bb as [hd bdy ex COR]. simpl. unfold no_header; unfold stick_header; simpl. reflexivity. Qed. - - - (** * Sequential Semantics of basic blocks *) Section RELSEM. @@ -302,29 +298,8 @@ Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome := Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome := par_goto_label f lbl rs rs m. -(** Evaluating a branch - -Warning: in m PC is assumed to be already pointing on the next instruction ! - -*) Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: option bool) : outcome := par_eval_branch f l rs rs m res. -(** Execution of a single control-flow instruction [i] in initial state [rs] and - [m]. Return updated state. - - As above: PC is assumed to be incremented on the next block before the control-flow instruction - - For instructions that correspond tobuiltin - actual RISC-V instructions, the cases are straightforward - transliterations of the informal descriptions given in the RISC-V - user-mode specification. For pseudo-instructions, refer to the - informal descriptions given above. - - Note that we set to [Vundef] the registers used as temporaries by - the expansions of the pseudo-instructions, so that the RISC-V code - we generate cannot use those registers to hold values that must - survive the execution of the pseudo-instruction. *) - Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) : outcome := parexec_control ge f oc rs rs m. Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcome := @@ -368,16 +343,11 @@ Inductive step: state -> trace -> state -> Prop := step (State rs m) t (State rs' m') . - - End RELSEM. - - Definition semantics (p: program) := Semantics step (initial_state p) final_state (Genv.globalenv p). - Definition data_preg (r: preg) : bool := match r with | RA => false @@ -386,4 +356,3 @@ Definition data_preg (r: preg) : bool := | IR _ => true | PC => false end. - diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index a7fa5cff..2d144bb6 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1,3 +1,10 @@ +(** * Translation from Asmblock to AbstractBB + + We define a specific instance of AbstractBB, named L, translate bblocks from Asmblock into this instance + AbstractBB will then define two semantics for L : a sequential, and a semantic one + We prove a bisimulation between the parallel semantics of L and AsmVLIW + From this, we also deduce a bisimulation between the sequential semantics of L and Asmblock *) + Require Import AST. Require Import Asmblock. Require Import Asmblockgenproof0. @@ -17,6 +24,8 @@ Require Import Chunks. Open Scope impure. +(** Definition of L *) + Module P<: ImpParam. Module R := Pos. @@ -459,18 +468,6 @@ Qed. Hint Resolve op_eq_correct: wlp. Global Opaque op_eq_correct. - -(* QUICK FIX WITH struct_eq *) - -(* Definition op_eq (o1 o2: op): ?? bool := struct_eq o1 o2. - -Theorem op_eq_correct o1 o2: - WHEN op_eq o1 o2 ~> b THEN b=true -> o1 = o2. -Proof. - wlp_simplify. -Qed. -*) - End IMPPARAM. End P. @@ -550,7 +547,7 @@ Proof. - unfold ppos. unfold pmem. discriminate. Qed. -(** Inversion functions, used for debugging *) +(** Inversion functions, used for debug traces *) Definition pos_to_ireg (p: R.t) : option gpreg := match p with @@ -574,9 +571,6 @@ Definition inv_ppos (p: R.t) : option preg := end end. - -(** Traduction Asmblock -> Asmblockdeps *) - Notation "a @ b" := (Econs a b) (at level 102, right associativity). Definition trans_control (ctl: control) : inst := @@ -720,7 +714,7 @@ Proof. intros. congruence. Qed. -(** Parallelizability of a bblock (bundle) *) +(** Parallelizability test of a bblock (bundle), and bisimulation of the Asmblock and L parallel semantics *) Module PChk := ParallelChecks L PosPseudoRegSet. @@ -1162,7 +1156,7 @@ Proof. destruct (prun_iw _ _ _ _); simpl; eauto. Qed. -(* sequential execution *) +(** sequential execution *) Theorem bisimu_basic ge fn bi rs m s: Ge = Genv ge fn -> match_states (State rs m) s -> @@ -1264,7 +1258,6 @@ Qed. End SECT_PAR. - Section SECT_BBLOCK_EQUIV. Variable Ge: genv. @@ -1294,6 +1287,8 @@ Proof. * discriminate. Qed. +(** Used for debug traces *) + Definition gpreg_name (gpr: gpreg) := match gpr with | GPR0 => Str ("GPR0") | GPR1 => Str ("GPR1") | GPR2 => Str ("GPR2") | GPR3 => Str ("GPR3") | GPR4 => Str ("GPR4") @@ -1645,4 +1640,4 @@ Definition bblock_simub: Asmvliw.bblock -> Asmvliw.bblock -> bool := pure_bblock Lemma bblock_simub_correct p1 p2 ge fn: bblock_simub p1 p2 = true -> Asmblockgenproof0.bblock_simu ge fn p1 p2. Proof. eapply (pure_bblock_simu_test_correct true). -Qed. \ No newline at end of file +Qed. diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index e5b9b35a..7e415c2a 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -15,7 +15,8 @@ (* *) (* *********************************************************************) -(** Translation from Machblock to K1c assembly language (Asmblock) *) +(** * Translation from Machblock to K1c assembly language (Asmblock) + Inspired from the Mach->Asm pass of other backends, but adapted to the block structure *) Require Archi. Require Import Coqlib Errors. @@ -41,23 +42,15 @@ Definition ireg_of (r: mreg) : res ireg := Definition freg_of (r: mreg) : res freg := match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgenblock.freg_of") end. -(* -(** Decomposition of 32-bit integer constants. They are split into either - small signed immediates that fit in 12-bits, or, if they do not fit, - into a (20-bit hi, 12-bit lo) pair where lo is sign-extended. *) - -*) Inductive immed32 : Type := | Imm32_single (imm: int). Definition make_immed32 (val: int) := Imm32_single val. -(** Likewise, for 64-bit integer constants. *) Inductive immed64 : Type := | Imm64_single (imm: int64) . -(* For now, let's suppose all instructions of K1c can handle 64-bits immediate *) Definition make_immed64 (val: int64) := Imm64_single val. Notation "a ::g b" := (cons (A:=instruction) a b) (at level 49, right associativity). @@ -66,12 +59,6 @@ Notation "a ::b lb" := ((bblock_single_inst a) :: lb) (at level 49, right associ Notation "a ++g b" := (app (A:=instruction) a b) (at level 49, right associativity). Notation "a @@ b" := (app a b) (at level 49, right associativity). -(** Smart constructors for arithmetic operations involving - a 32-bit or 64-bit integer constant. Depending on whether the - constant fits in 12 bits or not, one or several instructions - are generated as required to perform the operation - and prepended to the given instruction sequence [k]. *) - Definition loadimm32 (r: ireg) (n: int) := match make_immed32 n with | Imm32_single imm => Pmake r imm @@ -92,10 +79,6 @@ Definition orimm32 := opimm32 Porw Poriw. Definition norimm32 := opimm32 Pnorw Pnoriw. Definition xorimm32 := opimm32 Pxorw Pxoriw. Definition nxorimm32 := opimm32 Pnxorw Pnxoriw. -(* -Definition sltimm32 := opimm32 Psltw Psltiw. -Definition sltuimm32 := opimm32 Psltuw Psltiuw. -*) Definition loadimm64 (r: ireg) (n: int64) := match make_immed64 n with @@ -118,11 +101,6 @@ Definition norimm64 := opimm64 Pnorl Pnoril. Definition nandimm64 := opimm64 Pnandl Pnandil. Definition nxorimm64 := opimm64 Pnxorl Pnxoril. -(* -Definition sltimm64 := opimm64 Psltl Psltil. -Definition sltuimm64 := opimm64 Psltul Psltiul. -*) - Definition addptrofs (rd rs: ireg) (n: ptrofs) := if Ptrofs.eq_dec n Ptrofs.zero then Pmv rd rs @@ -170,19 +148,6 @@ Definition transl_opt_compuimm transl_compi c Unsigned r1 n lbl k . -(* Definition transl_opt_compuimm - (n: int) (c: comparison) (r1: ireg) (lbl: label) (k: code) : list instruction := - loadimm32 RTMP n ::g (transl_comp c Unsigned r1 RTMP lbl k). *) - -(* match select_comp n c with - | Some Ceq => Pcbu BTweqz r1 lbl ::g k - | Some Cne => Pcbu BTwnez r1 lbl ::g k - | Some _ => nil (* Never happens *) - | None => loadimm32 RTMP n ::g (transl_comp c Unsigned r1 RTMP lbl k) - end - . - *) - Definition select_compl (n: int64) (c: comparison) : option comparison := if Int64.eq n Int64.zero then match c with @@ -1052,7 +1017,7 @@ Definition make_epilogue (f: Machblock.function) (k: code) := (loadind_ptr SP f.(fn_retaddr_ofs) GPRA) ::g Pset RA GPRA ::g Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::g k. -(** Translation of a Mach instruction. *) +(** Translation of a Machblock instruction. *) Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst) (ep: bool) (k: bcode) := @@ -1096,20 +1061,12 @@ Definition transl_instr_control (f: Machblock.function) (oi: option Machblock.co transl_cbranch cond args lbl nil | MBreturn => OK (make_epilogue f (Pret ::g nil)) - (*OK (make_epilogue f (Pj_r RA f.(Mach.fn_sig) :: k))*) | MBjumptable arg tbl => do r <- ireg_of arg; OK (Pjumptable r tbl ::g nil) end end. -(* TODO - dans l'idée, transl_instr_control renvoie une liste d'instructions sous la forme : - * transl_instr_control _ _ _ = lb ++ (ctl :: nil), où lb est une liste de basics, ctl est un control_inst - - Il faut arriver à exprimer cet aspect là ; extraire le lb, le rajouter dans le body ; et extraire le ctl - qu'on met dans le exit -*) - (** Translation of a code sequence *) Definition fp_is_parent (before: bool) (i: Machblock.basic_inst) : bool := @@ -1120,8 +1077,7 @@ Definition fp_is_parent (before: bool) (i: Machblock.basic_inst) : bool := | _ => false end. -(** This is the naive definition that we no longer use because it - is not tail-recursive. It is kept as specification. *) +(** This is the naive definition, which is not tail-recursive unlike the other backends *) Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) := match il with @@ -1147,20 +1103,11 @@ Definition transl_basic_code' (f: Machblock.function) (il: list Machblock.basic_ transl_basic_rec f il it1p (fun c => OK c). *) (** Translation of a whole function. Note that we must check - that the generated code contains less than [2^32] instructions, + that the generated code contains less than [2^64] instructions, otherwise the offset part of the [PC] code pointer could wrap around, leading to incorrect executions. *) -(* Local Obligation Tactic := bblock_auto_correct. *) - -(* Program Definition gen_bblock_noctl (hd: list label) (c: list basic) := - match c with - | nil => {| header := hd; body := Pnop::nil; exit := None |} - | i::c => {| header := hd; body := i::c; exit := None |} - end. - *) - -(** Can generate two bblocks if the ctl is a PExpand (since the PExpand must be alone in its block) *) +(* gen_bblocks can generate two bblocks if the ctl is a PExpand (since the PExpand must be alone in its block) *) Program Definition gen_bblocks (hd: list label) (c: list basic) (ctl: list instruction) := match (extract_ctl ctl) with | None => @@ -1168,7 +1115,6 @@ Program Definition gen_bblocks (hd: list label) (c: list basic) (ctl: list instr | nil => {| header := hd; body := Pnop::nil; exit := None |} :: nil | i::c => {| header := hd; body := ((i::c) ++ extract_basic ctl); exit := None |} :: nil end -(* gen_bblock_noctl hd (c ++ (extract_basic ctl)) :: nil *) | Some (PExpand (Pbuiltin ef args res)) => match c with | nil => {| header := hd; body := nil; exit := Some (PExpand (Pbuiltin ef args res)) |} :: nil diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v index 89d41017..decc3e2e 100644 --- a/mppa_k1c/Asmblockgenproof0.v +++ b/mppa_k1c/Asmblockgenproof0.v @@ -1,3 +1,9 @@ +(** * "block" version of Asmgenproof0 + + This module is largely adapted from Asmgenproof0.v of the other backends + It needs to stand apart because of the block structure, and the distinction control/basic that there isn't in the other backends + It has similar definitions than Asmgenproof0, but adapted to this new structure *) + Require Import Coqlib. Require Intv. Require Import AST. @@ -31,19 +37,13 @@ Lemma ireg_of_eq: forall r r', ireg_of r = OK r' -> preg_of r = IR r'. Proof. unfold ireg_of; intros. destruct (preg_of r); inv H; auto. -(* destruct b. all: try discriminate. - inv H1. auto. - *)Qed. +Qed. -(* FIXME - Replaced FR by IR for MPPA *) Lemma freg_of_eq: forall r r', freg_of r = OK r' -> preg_of r = IR r'. Proof. unfold freg_of; intros. destruct (preg_of r); inv H; auto. -(* destruct b. all: try discriminate. - inv H1. auto. - *)Qed. - +Qed. Lemma preg_of_injective: forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2. @@ -277,24 +277,6 @@ Proof. exploit preg_of_injective; eauto. congruence. Qed. -(* Lemma agree_undef_regs2: - forall ms sp rl rs rs', - agree (Mach.undef_regs rl ms) sp rs -> - (forall r', data_preg r' = true -> preg_notin r' rl -> rs'#r' = rs#r') -> - agree (Mach.undef_regs rl ms) sp rs'. -Proof. - intros. destruct H. split; auto. - rewrite <- agree_sp0. apply H0; auto. - rewrite preg_notin_charact. intros. apply not_eq_sym. apply preg_of_not_SP. - intros. destruct (In_dec mreg_eq r rl). - rewrite Mach.undef_regs_same; auto. - rewrite H0; auto. - apply preg_of_data. - rewrite preg_notin_charact. intros; red; intros. elim n. - exploit preg_of_injective; eauto. congruence. -Qed. - *) - Lemma agree_set_undef_mreg: forall ms sp rs r v rl rs', agree ms sp rs -> @@ -607,15 +589,13 @@ Hypothesis transf_function_len: forall f tf, transf_function f = OK tf -> size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned. -(* NB: the hypothesis in comment on [b] is not needed in the proof ! *) Lemma return_address_exists: - forall b f (* sg ros *) c, (* b.(MB.exit) = Some (MBcall sg ros) -> *) is_tail (b :: c) f.(MB.fn_code) -> + forall b f c, is_tail (b :: c) f.(MB.fn_code) -> exists ra, return_address_offset f c ra. Proof. intros. destruct (transf_function f) as [tf|] eqn:TF. + exploit transf_function_inv; eauto. intros (tc1 & ep1 & TR1 & TL1). exploit transl_blocks_tail; eauto. intros (tc2 & ep2 & TR2 & TL2). -(* unfold return_address_offset. *) monadInv TR2. assert (TL3: is_tail x0 (fn_blocks tf)). { apply is_tail_trans with tc1; auto. @@ -632,7 +612,7 @@ Qed. End RETADDR_EXISTS. (** [transl_code_at_pc pc fb f c ep tf tc] holds if the code pointer [pc] points - within the Asm code generated by translating Mach function [f], + within the Asmblock code generated by translating Machblock function [f], and [tc] is the tail of the generated code at the position corresponding to the code pointer [pc]. *) @@ -850,18 +830,6 @@ Proof. apply exec_straight_step with rs2 m2; auto. Qed. -(* Theorem exec_straight_bblock: - forall rs1 m1 rs2 m2 rs3 m3 b, - exec_straight (body b) rs1 m1 nil rs2 m2 -> - exec_control_rel (exit b) b rs2 m2 rs3 m3 -> - exec_bblock_rel b rs1 m1 rs3 m3. -Proof. - intros. - econstructor; eauto. unfold exec_bblock. erewrite exec_straight_body; eauto. - inv H0. auto. -Qed. *) - - Lemma exec_straight_two: forall i1 i2 c rs1 m1 rs2 m2 rs3 m3, exec_basic_instr ge i1 rs1 m1 = Next rs2 m2 -> @@ -973,18 +941,6 @@ Proof. - reflexivity. Qed. -(* Lemma exec_straight_pc': - forall c rs1 m1 rs2 m2, - exec_straight c rs1 m1 nil rs2 m2 -> - rs2 PC = rs1 PC. -Proof. - induction c; intros; try (inv H; fail). - inv H. - - erewrite exec_basic_instr_pc; eauto. - - rewrite (IHc rs3 m3 rs2 m2); auto. - erewrite exec_basic_instr_pc; eauto. -Qed. *) - Lemma exec_straight_pc: forall c c' rs1 m1 rs2 m2, exec_straight c rs1 m1 c' rs2 m2 -> @@ -997,25 +953,6 @@ Proof. erewrite exec_basic_instr_pc; eauto. Qed. -(* Lemma exec_straight_through: - forall c i b lb rs1 m1 rs2 m2 rs2' m2', - bblock_basic_ctl c i = b -> - exec_straight c rs1 m1 nil rs2 m2 -> - nextblock b rs2 = rs2' -> m2 = m2' -> - exec_control ge fn i rs2' m2' = Next rs2' m2' -> (* if the control does not jump *) - exec_straight_blocks (b::lb) rs1 m1 lb rs2' m2'. -Proof. - intros. subst. destruct i. - - constructor 1. - + unfold exec_bblock. simpl body. erewrite exec_straight_body; eauto. - + rewrite <- (exec_straight_pc c nil rs1 m1 rs2 m2'); auto. - - destruct c as [|i c]; try (inv H0; fail). - constructor 1. - + unfold exec_bblock. simpl body. erewrite exec_straight_body; eauto. - + rewrite <- (exec_straight_pc (i ::i c) nil rs1 m1 rs2 m2'); auto. -Qed. - *) - Lemma regset_same_assign (rs: regset) r: rs # r <- (rs r) = rs. Proof. @@ -1034,8 +971,6 @@ Proof. simpl; auto. unfold nextblock, incrPC; simpl. Simpl. erewrite exec_straight_pc; eauto. Qed. - - (** The following lemmas show that straight-line executions (predicate [exec_straight_blocks]) correspond to correct Asm executions. *) @@ -1086,7 +1021,6 @@ Qed. End STRAIGHTLINE. - (** * Properties of the Machblock call stack *) Section MATCH_STACK. diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index bc549b4a..e1e2b0b0 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -15,6 +15,8 @@ (* *) (* *********************************************************************) +(** * Proof of correctness for individual instructions *) + Require Import Coqlib Errors Maps. Require Import AST Integers Floats Values Memory Globalenvs. Require Import Op Locations Machblock Conventions. @@ -86,31 +88,6 @@ Section CONSTRUCTORS. Variable ge: genv. Variable fn: function. -(* -(** 32-bit integer constants and arithmetic *) -(* -Lemma load_hilo32_correct: - forall rd hi lo k rs m, - exists rs', - exec_straight ge fn (load_hilo32 rd hi lo k) rs m k rs' m - /\ rs'#rd = Vint (Int.add (Int.shl hi (Int.repr 12)) lo) - /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. -Proof. - unfold load_hilo32; intros. - predSpec Int.eq Int.eq_spec lo Int.zero. -- subst lo. econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. rewrite Int.add_zero. Simpl. - intros; Simpl. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split. Simpl. - intros; Simpl. -Qed. -*) - -*) - Lemma loadimm32_correct: forall rd n k rs m, exists rs', @@ -141,60 +118,6 @@ Proof. intros; Simpl. Qed. -(* -(* -Lemma opimm32_correct: - forall (op: ireg -> ireg0 -> ireg0 -> instruction) - (opi: ireg -> ireg0 -> int -> instruction) - (sem: val -> val -> val) m, - (forall d s1 s2 rs, - exec_instr ge fn (op d s1 s2) rs m = Next (nextinstr (rs#d <- (sem rs##s1 rs##s2))) m) -> - (forall d s n rs, - exec_instr ge fn (opi d s n) rs m = Next (nextinstr (rs#d <- (sem rs##s (Vint n)))) m) -> - forall rd r1 n k rs, - r1 <> RTMP -> - exists rs', - exec_straight ge fn (opimm32 op opi rd r1 n k) rs m k rs' m - /\ rs'#rd = sem rs##r1 (Vint n) - /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r. -Proof. - intros. unfold opimm32. generalize (make_immed32_sound n); intros E. - destruct (make_immed32 n). -- subst imm. econstructor; split. - apply exec_straight_one. rewrite H0. simpl; eauto. auto. - split. Simpl. intros; Simpl. -- destruct (load_hilo32_correct RTMP hi lo (op rd r1 RTMP :: k) rs m) - as (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. apply exec_straight_one. - rewrite H; eauto. auto. - split. Simpl. simpl. rewrite B, C, E. auto. congruence. congruence. - intros; Simpl. -Qed. - -(** 64-bit integer constants and arithmetic *) - -Lemma load_hilo64_correct: - forall rd hi lo k rs m, - exists rs', - exec_straight ge fn (load_hilo64 rd hi lo k) rs m k rs' m - /\ rs'#rd = Vlong (Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo) - /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. -Proof. - unfold load_hilo64; intros. - predSpec Int64.eq Int64.eq_spec lo Int64.zero. -- subst lo. econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. rewrite Int64.add_zero. Simpl. - intros; Simpl. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split. Simpl. - intros; Simpl. -Qed. -*) -*) - Lemma opimm64_correct: forall (op: arith_name_rrr) (opi: arith_name_rri64) @@ -215,18 +138,6 @@ Proof. - subst imm. econstructor; split. apply exec_straight_one. rewrite H0. simpl; eauto. auto. split. Simpl. intros; Simpl. -(* -- destruct (load_hilo64_correct RTMP hi lo (op rd r1 RTMP :: k) rs m) - as (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. apply exec_straight_one. - rewrite H; eauto. auto. - split. Simpl. simpl. rewrite B, C, E. auto. congruence. congruence. - intros; Simpl. -- subst imm. econstructor; split. - eapply exec_straight_two. simpl; eauto. rewrite H. simpl; eauto. auto. auto. - split. Simpl. intros; Simpl. -*) Qed. (** Add offset to pointer *) @@ -252,35 +163,6 @@ Proof. rewrite Ptrofs.of_int64_to_int64 by auto. auto. Qed. -(* -(* -Lemma addptrofs_correct_2: - forall rd r1 n k (rs: regset) m b ofs, - r1 <> RTMP -> rs#r1 = Vptr b of -s -> - exists rs', - exec_straight ge fn (addptrofs rd r1 n k) rs m k rs' m - /\ rs'#rd = Vptr b (Ptrofs.add ofs n) - /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r. -Proof. - intros. exploit (addptrofs_correct rd r1 n); eauto. intros (rs' & A & B & C). - exists rs'; intuition eauto. - rewrite H0 in B. inv B. auto. -Qed. - -(** Translation of conditional branches *) - -Remark branch_on_RTMP: - forall normal lbl (rs: regset) m b, - rs#RTMP = Val.of_bool (eqb normal b) -> - exec_instr ge fn (if normal then Pbnew RTMP X0 lbl else Pbeqw RTMP X0 lbl) rs m = - eval_branch fn lbl rs m (Some b). -Proof. - intros. destruct normal; simpl; rewrite H; simpl; destruct b; reflexivity. -Qed. -*) -*) - Ltac ArgsInv := repeat (match goal with | [ H: Error _ = OK _ |- _ ] => discriminate @@ -1522,99 +1404,6 @@ Proof. exploit transl_cond_nofloat32_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto. Qed. -(* -(* -+ (* cmpf *) - destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR. - fold (Val.cmpf c0 (rs x) (rs x0)). - set (v := Val.cmpf c0 (rs x) (rs x0)). - destruct normal; inv EQ2. -* econstructor; split. - apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto. - split; intros; Simpl. -* econstructor; split. - eapply exec_straight_two. - eapply transl_cond_float_correct with (v := Val.notbool v); eauto. - simpl; reflexivity. - auto. auto. - split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto. -+ (* notcmpf *) - destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR. - rewrite Val.notbool_negb_3. fold (Val.cmpf c0 (rs x) (rs x0)). - set (v := Val.cmpf c0 (rs x) (rs x0)). - destruct normal; inv EQ2. -* econstructor; split. - eapply exec_straight_two. - eapply transl_cond_float_correct with (v := v); eauto. - simpl; reflexivity. - auto. auto. - split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto. -* econstructor; split. - apply exec_straight_one. eapply transl_cond_float_correct with (v := Val.notbool v); eauto. auto. - split; intros; Simpl. -+ (* cmpfs *) - destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR. - fold (Val.cmpfs c0 (rs x) (rs x0)). - set (v := Val.cmpfs c0 (rs x) (rs x0)). - destruct normal; inv EQ2. -* econstructor; split. - apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto. - split; intros; Simpl. -* econstructor; split. - eapply exec_straight_two. - eapply transl_cond_single_correct with (v := Val.notbool v); eauto. - simpl; reflexivity. - auto. auto. - split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto. -+ (* notcmpfs *) - destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR. - rewrite Val.notbool_negb_3. fold (Val.cmpfs c0 (rs x) (rs x0)). - set (v := Val.cmpfs c0 (rs x) (rs x0)). - destruct normal; inv EQ2. -* econstructor; split. - eapply exec_straight_two. - eapply transl_cond_single_correct with (v := v); eauto. - simpl; reflexivity. - auto. auto. - split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto. -* econstructor; split. - apply exec_straight_one. eapply transl_cond_single_correct with (v := Val.notbool v); eauto. auto. - split; intros; Simpl. -*) -*) - -(** Some arithmetic properties. *) - -(* Remark cast32unsigned_from_cast32signed: - forall i, Int64.repr (Int.unsigned i) = Int64.zero_ext 32 (Int64.repr (Int.signed i)). -Proof. - intros. apply Int64.same_bits_eq; intros. - rewrite Int64.bits_zero_ext, !Int64.testbit_repr by tauto. - rewrite Int.bits_signed by tauto. fold (Int.testbit i i0). - change Int.zwordsize with 32. - destruct (zlt i0 32). auto. apply Int.bits_above. auto. -Qed. - -Lemma cast32signed_correct: - forall (d s: ireg) (k: code) (rs: regset) (m: mem), - exists rs': regset, - exec_straight ge (cast32signed d s ::g k) rs m k rs' m - /\ Val.lessdef (Val.longofint (rs s)) (rs' d) - /\ (forall r: preg, r <> PC -> r <> d -> rs' r = rs r). -Proof. - intros. unfold cast32signed. destruct (ireg_eq d s). -- econstructor; split. - + apply exec_straight_one. simpl. eauto with asmgen. - + split. - * rewrite e. Simpl. - * intros. destruct r; Simpl. -- econstructor; split. - + apply exec_straight_one. simpl. eauto with asmgen. - + split. - * Simpl. - * intros. destruct r; Simpl. -Qed. *) - (* Translation of arithmetic operations *) Ltac SimplEval H := @@ -1868,33 +1657,6 @@ Proof. + econstructor; econstructor; econstructor; econstructor; split. apply exec_straight_opt_refl. split; auto. simpl. subst imm. rewrite Ptrofs.of_int64_to_int64 by auto. auto. -(* -+ econstructor; econstructor; econstructor; split. - constructor. eapply exec_straight_two. - simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. destruct (rs base); auto; simpl. rewrite SF. simpl. - rewrite Ptrofs.add_assoc. f_equal. f_equal. - rewrite <- (Ptrofs.of_int64_to_int64 SF ofs). rewrite EQ. - symmetry; auto with ptrofs. -+ econstructor; econstructor; econstructor; split. - constructor. eapply exec_straight_two. - simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold eval_offset. destruct (rs base); auto; simpl. rewrite SF. simpl. - rewrite Ptrofs.add_zero. subst imm. rewrite Ptrofs.of_int64_to_int64 by auto. auto. -(* 32 bits part, irrelevant for us -- generalize (make_immed32_sound (Ptrofs.to_int ofs)); intros EQ. - destruct (make_immed32 (Ptrofs.to_int ofs)). -+ econstructor; econstructor; econstructor; split. - apply exec_straight_opt_refl. - split; auto. simpl. subst imm. rewrite Ptrofs.of_int_to_int by auto. auto. -+ econstructor; econstructor; econstructor; split. - constructor. eapply exec_straight_two. - simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. destruct (rs base); auto; simpl. rewrite SF. simpl. - rewrite Ptrofs.add_assoc. f_equal. f_equal. - rewrite <- (Ptrofs.of_int_to_int SF ofs). rewrite EQ. - symmetry; auto with ptrofs. -*)*) Qed. @@ -2555,8 +2317,8 @@ Proof. { eapply A2. } { apply exec_straight_one. simpl. rewrite (C2 SP) by auto with asmgen. rewrite <- (sp_val _ _ rs1 AG1). simpl; rewrite LP'. - rewrite FREE'. eauto. (* auto. *) } } - * split. (* apply agree_nextinstr. *)apply agree_set_other; auto with asmgen. + rewrite FREE'. eauto. } } + * split. apply agree_set_other; auto with asmgen. apply agree_change_sp with (Vptr stk soff). apply agree_exten with rs; auto. intros; rewrite C2; auto with asmgen. eapply parent_sp_def; eauto. diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index e7e21a18..e0878c7d 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -10,7 +10,7 @@ (* *) (* *********************************************************************) -(** Correctness proof for RISC-V generation: main proof. *) +(** Correctness proof for Asmgen *) Require Import Coqlib Errors. Require Import Integers Floats AST Linking. @@ -89,4 +89,4 @@ Module Asmgenproof0. Definition return_address_offset := return_address_offset. -End Asmgenproof0. \ No newline at end of file +End Asmgenproof0. diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index c6dd85f4..72584d2a 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -17,8 +17,6 @@ (** Abstract syntax and semantics for VLIW semantics of K1c assembly language. *) -(* FIXME: develop/fix the comments in this file *) - Require Import Coqlib. Require Import Maps. Require Import AST. @@ -45,8 +43,7 @@ Require Import Chunks. this view induces our sequential semantics of bundles defined in [Asmblock]. *) -(** General Purpose registers. -*) +(** General Purpose registers. *) Inductive gpreg: Type := | GPR0: gpreg | GPR1: gpreg | GPR2: gpreg | GPR3: gpreg | GPR4: gpreg @@ -152,9 +149,6 @@ Definition gpreg_o_expand (x : gpreg_o) : gpreg * gpreg * gpreg * gpreg := Lemma gpreg_o_eq : forall (x y : gpreg_o), {x=y} + {x<>y}. Proof. decide equality. Defined. -(** We model the following registers of the RISC-V architecture. *) - -(** basic register *) Inductive preg: Type := | IR: gpreg -> preg (**r integer general purpose registers *) | RA: preg @@ -173,7 +167,7 @@ End PregEq. Module Pregmap := EMap(PregEq). -(** Conventional names for stack pointer ([SP]) and return address ([RA]). *) +(** Conventional names for stack pointer ([SP]), return address ([RA]), frame pointer ([FP]) and other temporaries used *) Notation "'SP'" := GPR12 (only parsing) : asm. Notation "'FP'" := GPR17 (only parsing) : asm. @@ -188,9 +182,7 @@ Inductive btest: Type := | BTdgez (**r Double Greater Than or Equal to Zero *) | BTdlez (**r Double Less Than or Equal to Zero *) | BTdgtz (**r Double Greater Than Zero *) -(*| BTodd (**r Odd (LSB Set) *) - | BTeven (**r Even (LSB Clear) *) -*)| BTwnez (**r Word Not Equal to Zero *) + | BTwnez (**r Word Not Equal to Zero *) | BTweqz (**r Word Equal to Zero *) | BTwltz (**r Word Less Than Zero *) | BTwgez (**r Word Greater Than or Equal to Zero *) @@ -251,16 +243,7 @@ Definition offset : Type := ptrofs. Definition label := positive. -(* FIXME - rewrite the comment *) -(** A note on immediates: there are various constraints on immediate - operands to K1c instructions. We do not attempt to capture these - restrictions in the abstract syntax nor in the semantics. The - assembler will emit an error if immediate operands exceed the - representable range. Of course, our K1c generator (file - [Asmgen]) is careful to respect this range. *) - -(** Instructions to be expanded in control-flow -*) +(** Instructions to be expanded in control-flow *) Inductive ex_instruction : Type := (* Pseudo-instructions *) | Pbuiltin: external_function -> list (builtin_arg preg) -- cgit From d9f2d0e8a6420f4f1da8c693960a55c38747d6eb Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 28 Aug 2019 10:45:49 +0200 Subject: Removing submodule test/mppa/asm_coverage from the repository --- .gitmodules | 3 --- test/mppa/asm_coverage | 1 - 2 files changed, 4 deletions(-) delete mode 160000 test/mppa/asm_coverage diff --git a/.gitmodules b/.gitmodules index 955c7fc2..e69de29b 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +0,0 @@ -[submodule "test/mppa/asm_coverage"] - path = test/mppa/asm_coverage - url = git@gricad-gitlab.univ-grenoble-alpes.fr:sixcy/asm-scanner.git diff --git a/test/mppa/asm_coverage b/test/mppa/asm_coverage deleted file mode 160000 index a9c62b61..00000000 --- a/test/mppa/asm_coverage +++ /dev/null @@ -1 +0,0 @@ -Subproject commit a9c62b61552a9e9fd0ebf43df5ee0d5b88bb0944 -- cgit From fcc8418db10cc0f6abe63e78e1fdca948d872c2d Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 29 Aug 2019 17:22:11 +0200 Subject: Updated test/mppa/coverage.sh to check which instruction isn't tested yet --- test/mppa/coverage.sh | 22 +++++++++----- test/mppa/coverage_helper.py | 70 +++++++++++++++++++++++++------------------- 2 files changed, 55 insertions(+), 37 deletions(-) mode change 100644 => 100755 test/mppa/coverage.sh diff --git a/test/mppa/coverage.sh b/test/mppa/coverage.sh old mode 100644 new mode 100755 index 0a057ff9..2b3dafc0 --- a/test/mppa/coverage.sh +++ b/test/mppa/coverage.sh @@ -1,17 +1,25 @@ -asmdir=$1 +#!/bin/bash + +asmdir=instr/asm/ to_cover_raw=/tmp/to_cover_raw to_cover=/tmp/to_cover covered_raw=/tmp/covered_raw covered=/tmp/covered -sed -n "s/^.*fprintf oc \" \(.*\) .*/\1/p" ../../mppa_k1c/TargetPrinter.ml > $to_cover_raw -sed -n "s/^.*fprintf oc \" \(.*\)\\n.*/\1/p" ../../mppa_k1c/TargetPrinter.ml >> $to_cover_raw -python2.7 coverage_helper.py $to_cover_raw > $to_cover +# Stop at any error +set -e +# Pipes do not mask errors +set -o pipefail + +sed -n "s/^.*fprintf oc \" \([^.].*\) .*/\1/p" ../../mppa_k1c/TargetPrinter.ml | sort -u > $to_cover_raw +sed -n "s/^.*fprintf oc \" \([^.].*\)\\n.*/\1/p" ../../mppa_k1c/TargetPrinter.ml | sort -u >> $to_cover_raw +python2.7 coverage_helper.py $to_cover_raw | sort -u > $to_cover rm -f $covered_raw -for asm in $(ls $asmdir/*.s); do - bash asm_coverage/asm-coverage.sh $asm >> $covered_raw +for asm in $(ls $asmdir/*.ccomp.s); do + grep -v ":" $asm | sed -n "s/^\s*\([a-z][a-z0-9.]*\).*/\1/p" | sort -u >> $covered_raw done -python2.7 coverage_helper.py $covered_raw > $covered +python2.7 coverage_helper.py $covered_raw | sort -u > $covered vimdiff $to_cover $covered + diff --git a/test/mppa/coverage_helper.py b/test/mppa/coverage_helper.py index b086aca9..42e0c887 100644 --- a/test/mppa/coverage_helper.py +++ b/test/mppa/coverage_helper.py @@ -1,35 +1,45 @@ import fileinput +import sys -occurs = {} +all_loads_stores = "lbs lbz lhz lo lq ld lhs lws sb sd sh so sq sw".split(" ") + +all_bconds = "wnez weqz wltz wgez wlez wgtz dnez deqz dltz dgez dlez dgtz".split(" ") + +all_iconds = "ne eq lt ge le gt ltu geu leu gtu all nall any none".split(" ") + +all_fconds = "one ueq oeq une olt uge oge ult".split(" ") + +replaces_a = [(["cb."], all_bconds), + (["compd.", "compw."], all_iconds), + (["fcompd.", "fcompw."], all_fconds), + (all_loads_stores, [".xs"])] +replaces_dd = [(["addx", "sbfx"], ["2d", "4d", "8d", "16d"])] +replaces_dw = [(["addx", "sbfx"], ["2w", "4w", "8w", "16w"])] + +macros_binds = {"%a": replaces_a, "%dd": replaces_dd, "%dw": replaces_dw} + +def expand_macro(fullinst, macro, replaceTable): + inst = fullinst.replace(macro, "") + for (searchlist, mods) in replaceTable: + if inst in searchlist: + return [fullinst.replace(macro, mod) for mod in mods] + raise NameError + +insts = [] for line in fileinput.input(): - line_noc = line.replace('\n', '') - if line_noc not in occurs: - occurs[line_noc] = 0 - occurs[line_noc] += 1 - -# HACK: Removing all the instructions with "%a", replacing them with all their variations -# Also removing all instructions starting with '.' -pruned_occurs = dict(occurs) -for inst in occurs: - if inst[0] == '.': - del pruned_occurs[inst] - if "%a" not in inst: - continue - inst_no_a = inst.replace(".%a", "") - if inst_no_a in ("compw", "compd"): - del pruned_occurs[inst] - for mod in ("ne", "eq", "lt", "gt", "le", "ge", "ltu", "leu", "geu", - "gtu", "all", "any", "nall", "none"): - pruned_occurs[inst_no_a + "." + mod] = 1 - elif inst_no_a in ("cb"): - del pruned_occurs[inst] - for mod in ("wnez", "weqz", "wltz", "wgez", "wlez", "wgtz", "deqz", "dnez", - "dltz", "dgez", "dlez", "dgtz"): - pruned_occurs[inst_no_a + "." + mod] = 1 - else: - assert False, "Found instruction with %a: " + inst -occurs = pruned_occurs - -for inst in sorted(occurs): + fullinst = line[:-1] + try: + for macro in macros_binds: + if macro in fullinst: + insts.extend(expand_macro(fullinst, macro, macros_binds[macro])) + break + else: + insts.append(fullinst) + except NameError: + print >> sys.stderr, fullinst + " could not be found any match for macro " + macro + sys.exit(1) + +for inst in insts: print inst +occurs = {} -- cgit From a160967d4ce131c6cad7c1c44b654e3aa5855023 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 30 Aug 2019 10:44:43 +0200 Subject: Fixed the extraction of instructions from TargetPrinter.ml --- test/mppa/coverage.sh | 5 ++--- test/mppa/coverage_helper.py | 4 ++-- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/test/mppa/coverage.sh b/test/mppa/coverage.sh index 2b3dafc0..ec66c94e 100755 --- a/test/mppa/coverage.sh +++ b/test/mppa/coverage.sh @@ -1,5 +1,6 @@ #!/bin/bash +printer=../../mppa_k1c/TargetPrinter.ml asmdir=instr/asm/ to_cover_raw=/tmp/to_cover_raw to_cover=/tmp/to_cover @@ -11,8 +12,7 @@ set -e # Pipes do not mask errors set -o pipefail -sed -n "s/^.*fprintf oc \" \([^.].*\) .*/\1/p" ../../mppa_k1c/TargetPrinter.ml | sort -u > $to_cover_raw -sed -n "s/^.*fprintf oc \" \([^.].*\)\\n.*/\1/p" ../../mppa_k1c/TargetPrinter.ml | sort -u >> $to_cover_raw +sed -n "s/^.*fprintf\s*oc\s*\"\s*\([a-z][^[:space:]]*\)\s.*/\1/p" $printer > $to_cover_raw python2.7 coverage_helper.py $to_cover_raw | sort -u > $to_cover rm -f $covered_raw @@ -22,4 +22,3 @@ done python2.7 coverage_helper.py $covered_raw | sort -u > $covered vimdiff $to_cover $covered - diff --git a/test/mppa/coverage_helper.py b/test/mppa/coverage_helper.py index 42e0c887..cf7a84c9 100644 --- a/test/mppa/coverage_helper.py +++ b/test/mppa/coverage_helper.py @@ -9,10 +9,10 @@ all_iconds = "ne eq lt ge le gt ltu geu leu gtu all nall any none".split(" ") all_fconds = "one ueq oeq une olt uge oge ult".split(" ") -replaces_a = [(["cb."], all_bconds), +replaces_a = [(["cb.", "cmoved."], all_bconds), (["compd.", "compw."], all_iconds), (["fcompd.", "fcompw."], all_fconds), - (all_loads_stores, [".xs"])] + (all_loads_stores, [".xs", ""])] replaces_dd = [(["addx", "sbfx"], ["2d", "4d", "8d", "16d"])] replaces_dw = [(["addx", "sbfx"], ["2w", "4w", "8w", "16w"])] -- cgit From 3a78733f68c8c02f8578fbfa8ca08bbed8ac7988 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 30 Aug 2019 12:08:59 +0200 Subject: Decreasing a bit the number of processes in run_benches --- test/monniaux/run_benches.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/monniaux/run_benches.sh b/test/monniaux/run_benches.sh index a562a117..5f9f22cb 100755 --- a/test/monniaux/run_benches.sh +++ b/test/monniaux/run_benches.sh @@ -6,7 +6,7 @@ for bench in $benches; do echo "(cd $bench && make -j5 run)" >> commands.txt done -cat commands.txt | xargs -n1 -I{} -P5 bash -c '{}' +cat commands.txt | xargs -n1 -I{} -P4 bash -c '{}' ## # Gather all the CSV files -- cgit From 96d03d469015db45828c89a68247f2c70c2bb102 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 30 Aug 2019 12:09:23 +0200 Subject: Adding tests for addx8d addx8w etc.. --- test/mppa/instr/Makefile | 5 +++-- test/mppa/instr/i32.c | 4 ++++ test/mppa/instr/i64.c | 4 ++++ 3 files changed, 11 insertions(+), 2 deletions(-) diff --git a/test/mppa/instr/Makefile b/test/mppa/instr/Makefile index 4129b628..33a265e3 100644 --- a/test/mppa/instr/Makefile +++ b/test/mppa/instr/Makefile @@ -5,6 +5,7 @@ CC ?= gcc CCOMP ?= ccomp OPTIM ?= -O2 CFLAGS ?= $(OPTIM) +CCOMPFLAGS ?= $(CFLAGS) -faddx SIMU ?= k1-mppa TIMEOUT ?= --signal=SIGTERM 120s DIFF ?= python2.7 floatcmp.py -reltol .00001 @@ -111,7 +112,7 @@ $(BINDIR)/%.gcc.bin: $(ASMDIR)/%.gcc.s $(K1LIB) $(K1CCPATH) $(BINDIR)/%.ccomp.bin: $(ASMDIR)/%.ccomp.s $(K1LIB) $(CCOMPPATH) @mkdir -p $(@D) - $(CCOMP) $(CFLAGS) $(filter-out $(CCOMPPATH),$^) -o $@ + $(CCOMP) $(CCOMPFLAGS) $(filter-out $(CCOMPPATH),$^) -o $@ # Source to assembly @@ -125,4 +126,4 @@ $(ASMDIR)/%.gcc.s: $(SRCDIR)/%.c $(K1CCPATH) $(ASMDIR)/%.ccomp.s: $(SRCDIR)/%.c $(CCOMPPATH) @mkdir -p $(@D) - $(CCOMP) $(CFLAGS) -S $< -o $@ + $(CCOMP) $(CCOMPFLAGS) -S $< -o $@ diff --git a/test/mppa/instr/i32.c b/test/mppa/instr/i32.c index c48531b1..c0985031 100644 --- a/test/mppa/instr/i32.c +++ b/test/mppa/instr/i32.c @@ -65,6 +65,10 @@ BEGIN_TEST(int) c += (a < b); c += (a + b) / 2; c += (int) int2float(a) + (int) int2float(b) + (int) int2float(42.3); + c += (a << 4); // addx16w + c += (a << 3); // addx8w + c += (a << 2); // addx4w + c += (a << 1); // addx2w int j; for (j = 0 ; j < 10 ; j++) diff --git a/test/mppa/instr/i64.c b/test/mppa/instr/i64.c index 00eb159d..84828bfb 100644 --- a/test/mppa/instr/i64.c +++ b/test/mppa/instr/i64.c @@ -43,6 +43,10 @@ BEGIN_TEST(long long) c += a >> (b & 0x8LL); c += a >> (b & 0x8ULL); c += a % b; + c += (a << 4); // addx16d + c += (a << 3); // addx8d + c += (a << 2); // addx4d + c += (a << 1); // addx2d long long d = 3; long long (*op)(long long, long long); -- cgit From 436bf1192e129427f6fcc99d2e6b75db08e80cf8 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 30 Aug 2019 15:08:07 +0200 Subject: (#157) Removed AFADDD and AFADDW from the builtins --- mppa_k1c/Asm.v | 4 ++-- mppa_k1c/Asmexpand.ml | 4 ++-- mppa_k1c/CBuiltins.ml | 4 ++-- mppa_k1c/TargetPrinter.ml | 4 ++-- test/mppa/instr/Makefile | 5 ++++- test/mppa/instr/builtin64.c | 10 ++++++++++ 6 files changed, 22 insertions(+), 9 deletions(-) create mode 100644 test/mppa/instr/builtin64.c diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 1964e5f8..a0c5e71c 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -99,8 +99,8 @@ Inductive instruction : Type := | Piinvals (addr: ireg) | Pitouchl (addr: ireg) | Pdzerol (addr: ireg) - | Pafaddd (addr: ireg) (incr_res: ireg) - | Pafaddw (addr: ireg) (incr_res: ireg) +(*| Pafaddd (addr: ireg) (incr_res: ireg) + | Pafaddw (addr: ireg) (incr_res: ireg) *) (* see #157 *) | Palclrd (dst: ireg) (addr: ireg) | Palclrw (dst: ireg) (addr: ireg) | Pclzll (rd rs: ireg) diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml index 65dee6c7..20d27951 100644 --- a/mppa_k1c/Asmexpand.ml +++ b/mppa_k1c/Asmexpand.ml @@ -465,14 +465,14 @@ let expand_builtin_inline name args res = let open Asmvliw in emit (Pitouchl addr) | "__builtin_k1_dzerol", [BA(IR addr)], _ -> emit (Pdzerol addr) - | "__builtin_k1_afaddd", [BA(IR addr); BA (IR incr_res)], BR(IR res) -> +(*| "__builtin_k1_afaddd", [BA(IR addr); BA (IR incr_res)], BR(IR res) -> (if res <> incr_res then (emit (Pmv(res, incr_res)); emit Psemi)); emit (Pafaddd(addr, res)) | "__builtin_k1_afaddw", [BA(IR addr); BA (IR incr_res)], BR(IR res) -> (if res <> incr_res then (emit (Pmv(res, incr_res)); emit Psemi)); - emit (Pafaddw(addr, res)) + emit (Pafaddw(addr, res)) *) (* see #157 *) | "__builtin_alclrd", [BA(IR addr)], BR(IR res) -> emit (Palclrd(res, addr)) | "__builtin_alclrw", [BA(IR addr)], BR(IR res) -> diff --git a/mppa_k1c/CBuiltins.ml b/mppa_k1c/CBuiltins.ml index 2f80c90f..a02da077 100644 --- a/mppa_k1c/CBuiltins.ml +++ b/mppa_k1c/CBuiltins.ml @@ -43,8 +43,8 @@ let builtins = { (* LSU Instructions *) (* acswapd and acswapw done using headers and assembly *) - "__builtin_k1_afaddd", (TInt(IULongLong, []), [TPtr(TVoid [], []); TInt(ILongLong, [])], false); - "__builtin_k1_afaddw", (TInt(IUInt, []), [TPtr(TVoid [], []); TInt(IInt, [])], false); +(* "__builtin_k1_afaddd", (TInt(IULongLong, []), [TPtr(TVoid [], []); TInt(ILongLong, [])], false); + "__builtin_k1_afaddw", (TInt(IUInt, []), [TPtr(TVoid [], []); TInt(IInt, [])], false); *) (* see #157 *) "__builtin_k1_alclrd", (TInt(IULongLong, []), [TPtr(TVoid [], [])], false); (* DONE *) "__builtin_k1_alclrw", (TInt(IUInt, []), [TPtr(TVoid [], [])], false); (* DONE *) "__builtin_k1_dinval", (TVoid [], [], false); (* DONE *) diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 674695d9..2621a43b 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -399,10 +399,10 @@ module Target (*: TARGET*) = fprintf oc " itouchl 0[%a]\n" ireg addr | Pdzerol addr -> fprintf oc " dzerol 0[%a]\n" ireg addr - | Pafaddd(addr, incr_res) -> +(* | Pafaddd(addr, incr_res) -> fprintf oc " afaddd 0[%a] = %a\n" ireg addr ireg incr_res | Pafaddw(addr, incr_res) -> - fprintf oc " afaddw 0[%a] = %a\n" ireg addr ireg incr_res + fprintf oc " afaddw 0[%a] = %a\n" ireg addr ireg incr_res *) (* see #157 *) | Palclrd(res, addr) -> fprintf oc " alclrd %a = 0[%a]\n" ireg res ireg addr | Palclrw(res, addr) -> diff --git a/test/mppa/instr/Makefile b/test/mppa/instr/Makefile index 33a265e3..69446796 100644 --- a/test/mppa/instr/Makefile +++ b/test/mppa/instr/Makefile @@ -46,6 +46,7 @@ all: $(BIN) GREEN=\033[0;32m RED=\033[0;31m +YELLOW=\033[0;33m NC=\033[0m .PHONY: @@ -54,7 +55,9 @@ test: $(X86_GCC_OUT) $(GCC_OUT) for test in $(TESTNAMES); do\ x86out=$(OUTDIR)/$$test.x86-gcc.out;\ gccout=$(OUTDIR)/$$test.gcc.out;\ - if $(DIFF) $$x86out $$gccout > /dev/null; test $${PIPESTATUS[0]} -ne 0; then\ + if grep "__K1C__" -q $$test.c; then\ + printf "$(YELLOW)UNTESTED: $$test.c contains an \`#ifdef __K1C__\`\n";\ + elif $(DIFF) $$x86out $$gccout > /dev/null; test $${PIPESTATUS[0]} -ne 0; then\ >&2 printf "$(RED)ERROR: $$x86out and $$gccout differ$(NC)\n";\ else\ printf "$(GREEN)GOOD: $$x86out and $$gccout concur$(NC)\n";\ diff --git a/test/mppa/instr/builtin64.c b/test/mppa/instr/builtin64.c new file mode 100644 index 00000000..40d53dc7 --- /dev/null +++ b/test/mppa/instr/builtin64.c @@ -0,0 +1,10 @@ +#include "framework.h" + +BEGIN_TEST(long long) + long long *ptr = &c; +#ifdef __K1C__ + /* Removed the AFADDD builtin who was incorrect in CompCert, see #157 */ + // a = __builtin_k1_afaddd(ptr, a); + // a = __builtin_k1_afaddd(ptr, a); +#endif +END_TEST64() -- cgit From 21622a06394e68170a9901f316addcd3fd1841de Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 30 Aug 2019 15:38:14 +0200 Subject: Added more tests --- mppa_k1c/TargetPrinter.ml | 4 ++-- test/mppa/coverage.sh | 2 +- test/mppa/instr/builtin64.c | 4 ++++ test/mppa/instr/i32.c | 38 ++++++++++++++++++++++++-------------- test/mppa/instr/i64.c | 39 +++++++++++++++++++++++++++------------ 5 files changed, 58 insertions(+), 29 deletions(-) diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 2621a43b..c9822e13 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -400,9 +400,9 @@ module Target (*: TARGET*) = | Pdzerol addr -> fprintf oc " dzerol 0[%a]\n" ireg addr (* | Pafaddd(addr, incr_res) -> - fprintf oc " afaddd 0[%a] = %a\n" ireg addr ireg incr_res + fprintfoc " afaddd 0[%a] = %a\n" ireg addr ireg incr_res | Pafaddw(addr, incr_res) -> - fprintf oc " afaddw 0[%a] = %a\n" ireg addr ireg incr_res *) (* see #157 *) + fprintfoc " afaddw 0[%a] = %a\n" ireg addr ireg incr_res *) (* see #157 *) | Palclrd(res, addr) -> fprintf oc " alclrd %a = 0[%a]\n" ireg res ireg addr | Palclrw(res, addr) -> diff --git a/test/mppa/coverage.sh b/test/mppa/coverage.sh index ec66c94e..42ed4182 100755 --- a/test/mppa/coverage.sh +++ b/test/mppa/coverage.sh @@ -12,7 +12,7 @@ set -e # Pipes do not mask errors set -o pipefail -sed -n "s/^.*fprintf\s*oc\s*\"\s*\([a-z][^[:space:]]*\)\s.*/\1/p" $printer > $to_cover_raw +sed -n "s/^.*fprintf\s\+oc\s*\"\s*\([a-z][^[:space:]]*\)\s.*/\1/p" $printer > $to_cover_raw python2.7 coverage_helper.py $to_cover_raw | sort -u > $to_cover rm -f $covered_raw diff --git a/test/mppa/instr/builtin64.c b/test/mppa/instr/builtin64.c index 40d53dc7..d568b7be 100644 --- a/test/mppa/instr/builtin64.c +++ b/test/mppa/instr/builtin64.c @@ -3,6 +3,10 @@ BEGIN_TEST(long long) long long *ptr = &c; #ifdef __K1C__ + long long d = c; + a = __builtin_k1_alclrd(ptr); + c = d; + /* Removed the AFADDD builtin who was incorrect in CompCert, see #157 */ // a = __builtin_k1_afaddd(ptr, a); // a = __builtin_k1_afaddd(ptr, a); diff --git a/test/mppa/instr/i32.c b/test/mppa/instr/i32.c index c0985031..4e389620 100644 --- a/test/mppa/instr/i32.c +++ b/test/mppa/instr/i32.c @@ -12,6 +12,14 @@ int tailsum(int a, int b){ return make(a+b); } +int fact(int a){ + int r = 1; + int i; + for (i = 1; i < a; i++) + r *= i; + return r; +} + float int2float(int v){ return v; } @@ -21,43 +29,43 @@ BEGIN_TEST(int) c += a&b; if ((a & 0x1) == 1) - c += 1; + c += fact(1); else - c += 2; + c += fact(2); if (a & 0x1 == 0) - c += 4; + c += fact(4); else - c += 8; + c += fact(8); b = !(a & 0x01); if (!b) - c += 16; + c += fact(16); else - c += 32; + c += fact(32); c += sum(make(a), make(b)); c += (long long) a; if (0 > (a & 0x1) - 1) - c += 64; + c += fact(64); else - c += 128; + c += fact(128); if (0 >= (a & 0x1)) - c += 256; + c += fact(256); else - c += 512; + c += fact(512); if ((a & 0x1) > 0) - c += 1024; + c += fact(1024); else - c += 2048; + c += fact(2048); if ((a & 0x1) - 1 >= 0) - c += 4096; + c += fact(4096); else - c += 8192; + c += fact(8192); c += ((a & 0x1) == (b & 0x1)); c += (a > b); @@ -70,6 +78,8 @@ BEGIN_TEST(int) c += (a << 2); // addx4w c += (a << 1); // addx2w + c += ~a & b; // andnw + int j; for (j = 0 ; j < 10 ; j++) c += a; diff --git a/test/mppa/instr/i64.c b/test/mppa/instr/i64.c index 84828bfb..dc5fa6ee 100644 --- a/test/mppa/instr/i64.c +++ b/test/mppa/instr/i64.c @@ -30,6 +30,14 @@ long long random_op(long long a, long long b){ return op(a, b); } +long fact(long a){ + long r = 1; + long i; + for (i = 1; i < a; i++) + r *= i; + return r; +} + double long2double(long v){ return v; } @@ -48,6 +56,8 @@ BEGIN_TEST(long long) c += (a << 2); // addx4d c += (a << 1); // addx2d + c += ~a & b; // andnd + long long d = 3; long long (*op)(long long, long long); @@ -65,34 +75,39 @@ BEGIN_TEST(long long) c += (unsigned int) a; if (0 != (a & 0x1LL)) - c += 1; + c += fact(1); else - c += 2; + c += fact(2); if (0 > (a & 0x1LL)) - c += 4; + c += fact(4); else - c += 8; + c += fact(8); if (0 >= (a & 0x1LL) - 1) - c += 16; + c += fact(16); + else + c += fact(32); + + if (a-41414141 > 0) + c += fact(13); else - c += 32; + c += fact(31); if (a & 0x1LL > 0) - c += 64; + c += fact(64); else - c += 128; + c += fact(128); if ((a & 0x1LL) - 1 >= 0) - c += 256; + c += fact(256); else - c += 512; + c += fact(512); if (0 == (a & 0x1LL)) - c += 1024; + c += fact(1024); else - c += 2048; + c += fact(2048); c += ((a & 0x1LL) == (b & 0x1LL)); c += (a >= b); -- cgit From ccd2fa5638e50b5fd8308b4b0c26531f911ff087 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 30 Aug 2019 17:08:07 +0200 Subject: Rajout de clzd dans les tests --- mppa_k1c/CBuiltins.ml | 5 ++--- test/mppa/instr/builtin64.c | 3 +++ 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/mppa_k1c/CBuiltins.ml b/mppa_k1c/CBuiltins.ml index a02da077..5fb69f62 100644 --- a/mppa_k1c/CBuiltins.ml +++ b/mppa_k1c/CBuiltins.ml @@ -63,7 +63,6 @@ let builtins = { "__builtin_k1_lwzu", (TInt(IUInt, []), [TPtr(TVoid [], [])], false); (* ALU Instructions *) - "__builtin_clzll", (TInt(IULongLong, []), [TInt(IULongLong, [])], false); (* "__builtin_k1_addhp", (TInt(IInt, []), [TInt(IInt, []); TInt(IInt, [])], false); *) (* "__builtin_k1_adds", (TInt(IInt, []), [TInt(IInt, []); TInt(IInt, [])], false); *) (* "__builtin_k1_bwlu", (TInt(IUInt, []), @@ -74,8 +73,8 @@ let builtins = { (* "__builtin_k1_cbs", (TInt(IInt, []), [TInt(IUInt, [])], false); *) (* "__builtin_k1_cbsdl", (TInt(ILongLong, []), [TInt(IULongLong, [])], false); *) (* "__builtin_k1_clz", (TInt(IInt, []), [TInt(IUInt, [])], false); *) - "__builtin_k1_clzw", (TInt(IInt, []), [TInt(IUInt, [])], false); - "__builtin_k1_clzd", (TInt(ILongLong, []), [TInt(IULongLong, [])], false); + "__builtin_clzw", (TInt(IInt, []), [TInt(IUInt, [])], false); + "__builtin_clzll", (TInt(ILongLong, []), [TInt(IULongLong, [])], false); (* "__builtin_k1_clzdl", (TInt(ILongLong, []), [TInt(IULongLong, [])], false); *) (* "__builtin_k1_cmove", (TInt(IInt, []), [TInt(IInt, []); TInt(IInt, []); TInt(IInt, [])], false); *) (* "__builtin_k1_ctz", (TInt(IInt, []), [TInt(IUInt, [])], false); *) diff --git a/test/mppa/instr/builtin64.c b/test/mppa/instr/builtin64.c index d568b7be..dbbb1886 100644 --- a/test/mppa/instr/builtin64.c +++ b/test/mppa/instr/builtin64.c @@ -6,6 +6,9 @@ BEGIN_TEST(long long) long long d = c; a = __builtin_k1_alclrd(ptr); c = d; + c += a; + + c += __builtin_clzll(a); /* Removed the AFADDD builtin who was incorrect in CompCert, see #157 */ // a = __builtin_k1_afaddd(ptr, a); -- cgit