From 82b3cfa677c21e7d1fab907f1824bb101f819291 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 17 Dec 2020 10:03:30 +0000 Subject: Modify software pipelining for build --- src/SoftwarePipelining/SPSymbolic_evaluation.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'src/SoftwarePipelining/SPSymbolic_evaluation.ml') diff --git a/src/SoftwarePipelining/SPSymbolic_evaluation.ml b/src/SoftwarePipelining/SPSymbolic_evaluation.ml index eba5707..450cda7 100644 --- a/src/SoftwarePipelining/SPSymbolic_evaluation.ml +++ b/src/SoftwarePipelining/SPSymbolic_evaluation.ml @@ -13,7 +13,8 @@ open Registers open Op open AST -open Base_types +open SPBase_types +open Camlcoq type symbolic_value = | Sreg of reg @@ -42,14 +43,14 @@ let find res st = | Not_found -> Sreg res let rec get_args st = function - | CList.Coq_nil -> [] - | CList.Coq_cons (arg,args) -> find arg st :: get_args st args + | [] -> [] + | arg::args -> find arg st :: get_args st args let rec symbolic_evaluation st sm cs = function | [] -> (st,sm,cs) | Inop :: l -> symbolic_evaluation st sm cs l - | Iop (Omove, CList.Coq_cons (src,CList.Coq_nil), dst) :: l -> + | Iop (Omove, [src], dst) :: l -> symbolic_evaluation (State.add dst (find src st) st) sm cs l | Iop (op, args, dst) :: l -> @@ -73,7 +74,7 @@ type osv = | Ostore of memory_chunk * addressing let string_of_osv = function - | Oresource (Reg r) -> Printf.sprintf "reg %i" (Int32.to_int (Camlcoq.camlint_of_positive r)) + | Oresource (Reg r) -> Printf.sprintf "reg %i" (P.to_int r) | Oresource Mem -> "mem" | Oop op -> string_of_op op | Oload (mc,addr) -> "load" @@ -201,7 +202,7 @@ let convert_sym st sm regs = let display_st name l regs = let (st,sm,_) = symbolic_evaluation initial_state initial_mem initial_cons l in let g = convert_sym st sm regs in - let addr = Debug.name ^ name in + let addr = SPDebug.name ^ name in dot_output_ss g addr ; ignore (Sys.command ("(dot -Tpng " ^ addr ^ " -o " ^ addr ^ ".png ; rm -f " ^ addr ^ ") & ")) (* & *) -- cgit