diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-12-17 12:36:28 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-12-17 12:36:28 +0000 |
commit | 051b2d07e66a89281fde102e850a4fc386dabdae (patch) | |
tree | 90d8b5f5681fb4dc9ab87e90218b5be4adf9d850 /src/SoftwarePipelining/SPSymbolic_evaluation.ml | |
parent | 520ce1b13a7843efe110d0ae3b9ae16795a92b08 (diff) | |
download | vericert-051b2d07e66a89281fde102e850a4fc386dabdae.tar.gz vericert-051b2d07e66a89281fde102e850a4fc386dabdae.zip |
Fix whitespace
Diffstat (limited to 'src/SoftwarePipelining/SPSymbolic_evaluation.ml')
-rw-r--r-- | src/SoftwarePipelining/SPSymbolic_evaluation.ml | 170 |
1 files changed, 85 insertions, 85 deletions
diff --git a/src/SoftwarePipelining/SPSymbolic_evaluation.ml b/src/SoftwarePipelining/SPSymbolic_evaluation.ml index 450cda7..c99afc8 100644 --- a/src/SoftwarePipelining/SPSymbolic_evaluation.ml +++ b/src/SoftwarePipelining/SPSymbolic_evaluation.ml @@ -20,7 +20,7 @@ type symbolic_value = | Sreg of reg | Sop of operation * symbolic_value list | Sload of memory_chunk * addressing * symbolic_value list * symbolic_mem - + and symbolic_mem = | Smem | Sstore of memory_chunk * addressing * symbolic_value list * symbolic_value * symbolic_mem @@ -36,34 +36,34 @@ let initial_mem = Smem let initial_cons = Cons.empty exception Not_straight - + let find res st = try State.find res st with - | Not_found -> Sreg res + | Not_found -> Sreg res let rec get_args st = function | [] -> [] | 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, [src], dst) :: l -> - symbolic_evaluation (State.add dst (find src st) st) sm cs l + symbolic_evaluation (State.add dst (find src st) st) sm cs l | Iop (op, args, dst) :: l -> - let sym_val = Sop (op,get_args st args) in - symbolic_evaluation (State.add dst sym_val st) sm (Cons.add sym_val cs) l + let sym_val = Sop (op,get_args st args) in + symbolic_evaluation (State.add dst sym_val st) sm (Cons.add sym_val cs) l | Iload (chunk, mode, args, dst) :: l -> - let sym_val = Sload (chunk, mode, get_args st args, sm) in - symbolic_evaluation (State.add dst sym_val st) sm (Cons.add sym_val cs) l + let sym_val = Sload (chunk, mode, get_args st args, sm) in + symbolic_evaluation (State.add dst sym_val st) sm (Cons.add sym_val cs) l | Istore (chunk, mode, args, src) :: l -> - let sym_mem = Sstore (chunk, mode, get_args st args, find src st, sm) in - symbolic_evaluation st sym_mem cs l + let sym_mem = Sstore (chunk, mode, get_args st args, find src st, sm) in + symbolic_evaluation st sym_mem cs l | _ :: l -> raise Not_straight @@ -83,7 +83,7 @@ let string_of_osv = function type ident = int module S = Graph.Persistent.Digraph.Abstract - (struct type t = osv * ident end) + (struct type t = osv * ident end) let name_of_vertex v = let (osv,id) = S.V.label v in @@ -118,76 +118,76 @@ let counter = ref 0 let rec convert_sv_rec sv graph = incr counter; match sv with - | Sreg res -> - let node = S.V.create (Oresource (Reg res), !counter) in - let graph = S.add_vertex graph node in - (graph,node) - - | Sop (op, svl) -> - let node = S.V.create (Oop op, !counter) in - let (graph, node_l) = List.fold_right (fun sv (graph,node_l) -> - let (graph,node) = convert_sv_rec sv graph in - graph, node :: node_l - ) svl (graph,[]) in - let graph = S.add_vertex graph node in - let graph = List.fold_right (fun n graph -> - S.add_edge graph node n - ) node_l graph in - (graph,node) - - - | Sload (mc,addr,svl,sm) -> - let node = S.V.create (Oload (mc, addr), !counter) in - let (graph, node_l) = List.fold_right (fun sv (graph,node_l) -> - let (graph,node) = convert_sv_rec sv graph in - graph, node :: node_l - ) svl (graph,[]) in - let (graph,node_m) = convert_sm_rec sm graph in - let graph = S.add_vertex graph node in - let graph = List.fold_right (fun n graph -> - S.add_edge graph node n - ) node_l graph in - let graph = S.add_edge graph node node_m in - (graph,node) - + | Sreg res -> + let node = S.V.create (Oresource (Reg res), !counter) in + let graph = S.add_vertex graph node in + (graph,node) + + | Sop (op, svl) -> + let node = S.V.create (Oop op, !counter) in + let (graph, node_l) = List.fold_right (fun sv (graph,node_l) -> + let (graph,node) = convert_sv_rec sv graph in + graph, node :: node_l + ) svl (graph,[]) in + let graph = S.add_vertex graph node in + let graph = List.fold_right (fun n graph -> + S.add_edge graph node n + ) node_l graph in + (graph,node) + + + | Sload (mc,addr,svl,sm) -> + let node = S.V.create (Oload (mc, addr), !counter) in + let (graph, node_l) = List.fold_right (fun sv (graph,node_l) -> + let (graph,node) = convert_sv_rec sv graph in + graph, node :: node_l + ) svl (graph,[]) in + let (graph,node_m) = convert_sm_rec sm graph in + let graph = S.add_vertex graph node in + let graph = List.fold_right (fun n graph -> + S.add_edge graph node n + ) node_l graph in + let graph = S.add_edge graph node node_m in + (graph,node) + and convert_sm_rec sm graph = incr counter; match sm with - | Smem -> - let node = S.V.create (Oresource Mem, !counter) in - let graph = S.add_vertex graph node in - (graph,node) - - | Sstore (mc,addr,svl,sv,sm) -> - let node = S.V.create (Ostore (mc, addr), !counter) in - let (graph, node_l) = List.fold_right (fun sv (graph,node_l) -> - let (graph,node) = convert_sv_rec sv graph in - graph, node :: node_l - ) svl (graph,[]) in - let (graph, n) = convert_sv_rec sv graph in - let (graph, node_m) = convert_sm_rec sm graph in - let graph = S.add_vertex graph node in - let graph = List.fold_right (fun n graph -> - S.add_edge graph node n - ) node_l graph in - let graph = S.add_edge graph node n in - let graph = S.add_edge graph node node_m in - (graph,node) - + | Smem -> + let node = S.V.create (Oresource Mem, !counter) in + let graph = S.add_vertex graph node in + (graph,node) + + | Sstore (mc,addr,svl,sv,sm) -> + let node = S.V.create (Ostore (mc, addr), !counter) in + let (graph, node_l) = List.fold_right (fun sv (graph,node_l) -> + let (graph,node) = convert_sv_rec sv graph in + graph, node :: node_l + ) svl (graph,[]) in + let (graph, n) = convert_sv_rec sv graph in + let (graph, node_m) = convert_sm_rec sm graph in + let graph = S.add_vertex graph node in + let graph = List.fold_right (fun n graph -> + S.add_edge graph node n + ) node_l graph in + let graph = S.add_edge graph node n in + let graph = S.add_edge graph node node_m in + (graph,node) + let convert_sv sv = convert_sv_rec sv S.empty let convert_sm sm = convert_sm_rec sm S.empty let convert_sym st sm regs = let graph = State.fold (fun res sv g -> - if (not (List.mem res regs)) then g - else - let (graph,head) = convert_sv sv in - incr counter; - let src = S.V.create (Oresource (Reg res), !counter) in - let graph = S.add_vertex graph src in - let graph = S.add_edge graph src head in - Op.union g graph - ) st S.empty + if (not (List.mem res regs)) then g + else + let (graph,head) = convert_sv sv in + incr counter; + let src = S.V.create (Oresource (Reg res), !counter) in + let graph = S.add_vertex graph src in + let graph = S.add_edge graph src head in + Op.union g graph + ) st S.empty in let graph' = let (graph,head) = convert_sm sm in @@ -198,29 +198,29 @@ let convert_sym st sm regs = graph in Op.union graph graph' - + 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 = SPDebug.name ^ name in dot_output_ss g addr ; ignore (Sys.command ("(dot -Tpng " ^ addr ^ " -o " ^ addr ^ ".png ; rm -f " ^ addr ^ ") & ")) (* & *) - + let symbolic_equivalence (st1,sm1,cs1) (st2,sm2,cs2) regs = Printf.printf "|cs1| = %i - |cs2| = %i \n" (Cons.cardinal cs1) (Cons.cardinal cs2); (List.fold_right (fun res b -> - find res st1 = find res st2 && b - ) regs true - && sm1 = sm2 - && Cons.equal cs1 cs2) + find res st1 = find res st2 && b + ) regs true + && sm1 = sm2 + && Cons.equal cs1 cs2) let symbolic_evaluation = symbolic_evaluation initial_state initial_mem initial_cons let symbolic_condition i l = match i with - | Icond (cond,args) -> - let args = to_caml_list args in - let (st,sm,cs) = symbolic_evaluation l in - (cond,List.map (fun r -> find r st) args) - | _ -> failwith "Not a condition !\n" + | Icond (cond,args) -> + let args = to_caml_list args in + let (st,sm,cs) = symbolic_evaluation l in + (cond,List.map (fun r -> find r st) args) + | _ -> failwith "Not a condition !\n" |