From 6e2259a57b6ca00c068b176b9d5087ed632598c2 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 30 Oct 2021 21:42:52 +0100 Subject: Fix compilation issues with new types --- src/extraction/Extraction.v | 6 ++++-- src/hls/PrintRTLBlockInstr.ml | 11 +++++++---- src/hls/RTLPargen.v | 40 ++++++++++++---------------------------- src/hls/Schedule.ml | 26 ++++++++++++++------------ 4 files changed, 37 insertions(+), 46 deletions(-) (limited to 'src') diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 97f0d2a..3544f9d 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -25,7 +25,9 @@ From vericert Require RTLBlockInstr HTLgen Pipeline - HLSOpts. + HLSOpts + Predicate +. From Coq Require DecidableClass. @@ -192,7 +194,7 @@ Separate Extraction RTLBlockgen.transl_program RTLBlockInstr.successors_instr HTLgen.tbl_to_case_expr Pipeline.pipeline - RTLBlockInstr.sat_pred_simple + Predicate.sat_pred_simple Verilog.stmnt_to_list Compiler.transf_c_program Compiler.transf_cminor_program diff --git a/src/hls/PrintRTLBlockInstr.ml b/src/hls/PrintRTLBlockInstr.ml index 979ca38..8e24575 100644 --- a/src/hls/PrintRTLBlockInstr.ml +++ b/src/hls/PrintRTLBlockInstr.ml @@ -4,6 +4,7 @@ open Datatypes open Maps open AST open RTLBlockInstr +open Predicate open PrintAST let reg pp r = @@ -22,10 +23,11 @@ let ros pp = function | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) let rec print_pred_op pp = function - | Pvar p -> pred pp p - | Pnot p -> fprintf pp "(~ %a)" print_pred_op p + | Plit p -> if fst p then pred pp (snd p) else fprintf pp "~ %a" pred (snd p) | Pand (p1, p2) -> fprintf pp "(%a & %a)" print_pred_op p1 print_pred_op p2 | Por (p1, p2) -> fprintf pp "(%a | %a)" print_pred_op p1 print_pred_op p2 + | Ptrue -> fprintf pp "T" + | Pfalse -> fprintf pp "⟂" let print_pred_option pp = function | Some x -> fprintf pp "(%a)" print_pred_op x @@ -48,8 +50,9 @@ let print_bblock_body pp i = (name_of_chunk chunk) (PrintOp.print_addressing reg) (addr, args) reg src - | RBsetpred (c, args, p) -> - fprintf pp "%a = %a\n" + | RBsetpred (p', c, args, p) -> + fprintf pp "%a %a = %a\n" + print_pred_option p' pred p (PrintOp.print_condition reg) (c, args) diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 13d9480..30a35f3 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -30,10 +30,12 @@ Require Import vericert.common.Vericertlib. Require Import vericert.hls.RTLBlock. Require Import vericert.hls.RTLPar. Require Import vericert.hls.RTLBlockInstr. +Require Import vericert.hls.Predicate. Require Import vericert.hls.Abstr. #[local] Open Scope positive. #[local] Open Scope forest. +#[local] Open Scope pred_op. (*Parameter op_le : Op.operation -> Op.operation -> bool. Parameter chunk_le : AST.memory_chunk -> AST.memory_chunk -> bool. @@ -271,20 +273,11 @@ Definition merge'' x := end. Definition predicated_prod {A B: Type} (p1: predicated A) (p2: predicated B) := - match p1, p2 with - | Psingle a, Psingle b => Psingle (a, b) - | Psingle a, Plist b => Plist (NE.map (fun x => (fst x, (a, snd x))) b) - | Plist b, Psingle a => Plist (NE.map (fun x => (fst x, (snd x, a))) b) - | Plist a, Plist b => - Plist (NE.map (fun x => match x with ((a, b), (c, d)) => (Pand a c, (b, d)) end) - (NE.non_empty_prod a b)) - end. + NE.map (fun x => match x with ((a, b), (c, d)) => (Pand a c, (b, d)) end) + (NE.non_empty_prod p1 p2). Definition predicated_map {A B: Type} (f: A -> B) (p: predicated A): predicated B := - match p with - | Psingle a => Psingle (f a) - | Plist b => Plist (NE.map (fun x => (fst x, f (snd x))) b) - end. + NE.map (fun x => (fst x, f (snd x))) p. (*map (fun x => (fst x, Econs (snd x) Enil)) pel*) Definition merge' (pel: pred_expr) (tpel: predicated expression_list) := @@ -292,7 +285,7 @@ Definition merge' (pel: pred_expr) (tpel: predicated expression_list) := Fixpoint merge (pel: list pred_expr): predicated expression_list := match pel with - | nil => Psingle Enil + | nil => NE.singleton (T, Enil) | a :: b => merge' a (merge b) end. @@ -305,29 +298,20 @@ Definition map_predicated {A B} (pf: predicated (A -> B)) (pa: predicated A): pr predicated_map (fun x => (fst x) (snd x)) (predicated_prod pf pa). Definition predicated_apply1 {A B} (pf: predicated (A -> B)) (pa: A): predicated B := - match pf with - | Psingle f => Psingle (f pa) - | Plist pf' => Plist (NE.map (fun x => (fst x, (snd x) pa)) pf') - end. + NE.map (fun x => (fst x, (snd x) pa)) pf. Definition predicated_apply2 {A B C} (pf: predicated (A -> B -> C)) (pa: A) (pb: B): predicated C := - match pf with - | Psingle f => Psingle (f pa pb) - | Plist pf' => Plist (NE.map (fun x => (fst x, (snd x) pa pb)) pf') - end. + NE.map (fun x => (fst x, (snd x) pa pb)) pf. Definition predicated_apply3 {A B C D} (pf: predicated (A -> B -> C -> D)) (pa: A) (pb: B) (pc: C): predicated D := - match pf with - | Psingle f => Psingle (f pa pb pc) - | Plist pf' => Plist (NE.map (fun x => (fst x, (snd x) pa pb pc)) pf') - end. + NE.map (fun x => (fst x, (snd x) pa pb pc)) pf. (*Compute merge (((Some (Pvar 2), Ebase (Reg 4))::nil)::((Some (Pvar 3), Ebase (Reg 3))::(Some (Pvar 1), Ebase (Reg 3))::nil)::nil).*) Definition predicated_from_opt {A: Type} (p: option pred_op) (a: A) := match p with - | None => Psingle a - | Some x => Plist (NE.singleton (x, a)) + | Some p' => NE.singleton (p', a) + | None => NE.singleton (T, a) end. Definition update (f : forest) (i : instr) : forest := @@ -347,7 +331,7 @@ Definition update (f : forest) (i : instr) : forest := (map_predicated (predicated_apply2 (map_predicated (predicated_from_opt p Estore) (f # (Reg r))) chunk addr) (merge (list_translation rl f))) (f # Mem)) - | RBsetpred c addr p => f + | RBsetpred p' c addr p => f end. (*| diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml index 2389369..dd3e39f 100644 --- a/src/hls/Schedule.ml +++ b/src/hls/Schedule.ml @@ -26,6 +26,7 @@ open AST open Kildall open Op open RTLBlockInstr +open Predicate open RTLBlock open HTL open Verilog @@ -105,7 +106,7 @@ let print_instr = function | RBnop -> "" | RBload (_, _, _, _, r) -> sprintf "load(%s)" (reg r) | RBstore (_, _, _, _, r) -> sprintf "store(%s)" (reg r) - | RBsetpred (_, _, p) -> sprintf "setpred(%s)" (print_pred p) + | RBsetpred (_, _, _, p) -> sprintf "setpred(%s)" (print_pred p) | RBop (_, op, args, d) -> (match op, args with | Omove, _ -> "mov" @@ -354,7 +355,7 @@ let rec find_all_next_dst_read i dst i' curr = | RBload (_, _, _, rs, _) :: curr' -> check_dst rs curr' | RBstore (_, _, _, rs, src) :: curr' -> check_dst (src :: rs) curr' | RBnop :: curr' -> find_all_next_dst_read i dst (i' + 1) curr' - | RBsetpred (_, rs, _) :: curr' -> check_dst rs curr' + | RBsetpred (_, _, rs, _) :: curr' -> check_dst rs curr' let drop i lst = let rec drop' i' lst' = @@ -413,10 +414,11 @@ let accumulate_WAW_mem_deps instrs dfg curri = let rec in_predicate p p' = match p' with - | Pvar p'' -> P.to_int p = P.to_int p'' - | Pnot p'' -> in_predicate p p'' + | Plit p'' -> P.to_int p = P.to_int (snd p'') | Pand (p1, p2) -> in_predicate p p1 || in_predicate p p2 | Por (p1, p2) -> in_predicate p p1 || in_predicate p p2 + | Ptrue -> false + | Pfalse -> false let get_predicate = function | RBop (p, _, _, _) -> p @@ -426,7 +428,7 @@ let get_predicate = function let rec next_setpred p i = function | [] -> None - | RBsetpred (_, _, p') :: rst -> + | RBsetpred (_, _, _, p') :: rst -> if in_predicate p' p then Some i else @@ -459,7 +461,7 @@ let accumulate_RAW_pred_deps instrs dfg curri = let accumulate_WAR_pred_deps instrs dfg curri = let i, curr = curri in match curr with - | RBsetpred (_, _, p) -> ( + | RBsetpred (_, _, _, p) -> ( match next_preduse p 0 (take i instrs |> List.rev) with | None -> dfg | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) @@ -468,8 +470,8 @@ let accumulate_WAR_pred_deps instrs dfg curri = let accumulate_WAW_pred_deps instrs dfg curri = let i, curr = curri in match curr with - | RBsetpred (_, _, p) -> ( - match next_setpred (Pvar p) 0 (take i instrs |> List.rev) with + | RBsetpred (_, _, _, p) -> ( + match next_setpred (Plit (true, p)) 0 (take i instrs |> List.rev) with | None -> dfg | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) | _ -> dfg @@ -512,18 +514,18 @@ let assigned_vars vars = function | RBop (_, _, _, dst) -> dst :: vars | RBload (_, _, _, _, dst) -> dst :: vars | RBstore (_, _, _, _, _) -> vars - | RBsetpred (_, _, _) -> vars + | RBsetpred (_, _, _, _) -> vars let get_pred = function | RBnop -> None | RBop (op, _, _, _) -> op | RBload (op, _, _, _, _) -> op | RBstore (op, _, _, _, _) -> op - | RBsetpred (_, _, _) -> None + | RBsetpred (_, _, _, _) -> None let independant_pred p p' = - match sat_pred_simple (Nat.of_int 100000) (Pand (p, p')) with - | Some None -> true + match sat_pred_simple (Pand (p, p')) with + | None -> true | _ -> false let check_dependent op1 op2 = -- cgit