This repository has been archived by the owner on Jun 9, 2019. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 0
/
certifierData.ml
144 lines (133 loc) · 5.86 KB
/
certifierData.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
open MatchTypes
type output_type = HTML | JSON | CSS | PNG
module IntSig = struct
type t = int
let compare: t -> t -> int = compare
let hash (x: t) = x
let equal: int -> int -> bool = (=)
end
module MatchOp = struct
type t = match_operation
let compare: t -> t -> int = compare
let default: t = MatchSimple
end;;
module TraceTree = Graph.Persistent.Digraph.ConcreteBidirectionalLabeled(IntSig)(MatchOp);;
module TraceNodes = Map.Make(IntSig);;
type trace_inner_node_data = {
op1: TraceTypes.rich_operation;
op2: TraceTypes.rich_operation;
stack: match_mode list;
trace_trace: ((match_condition * mismatch) list * match_operation) list
}
type trace_node =
FinalNodeData of trace_inner_node_data
| NodeData of trace_inner_node_data
| EndtraceData of TraceTypes.rich_operation list
| InitTailtraceData of TraceTypes.rich_operation list * match_mode list
| SuccessNode
| BlockedData of int * int * match_mode list
type trace_data = { tree: TraceTree.t; nodes: trace_node TraceNodes.t }
let tree_visitor which fop { tree; nodes } =
let rec find_follower_nodes v =
TraceTree.fold_succ_e (fun e next ->
let v' = TraceTree.E.dst e in
if fop (TraceTree.E.label e) then
v' :: next
else
find_follower_nodes v' @ next)
tree v [] in
let find_ops =
List.fold_left (fun (maybe1, maybe2) v -> match TraceNodes.find v nodes with
| FinalNodeData { op1; op2 } -> (Some op1, Some op2)
| NodeData { op1; op2 } -> (Some op1, Some op2)
| EndtraceData (op1 :: _) -> (Some op1, maybe2)
| InitTailtraceData (op2 :: _, _) -> (maybe1, Some op2)
| _ -> (maybe1, maybe2)) (None, None) in
let rec bfs layer =
match which (find_ops layer) with
| Some op ->
let layer' = List.map find_follower_nodes layer |> List.flatten in
(op, layer) :: bfs layer'
| None -> []
in bfs [0]
let reconstruct_first data =
tree_visitor fst
(function MatchSimple | MatchPush _ | MatchPop -> true | _ -> false)
data
let reconstruct_second data = tree_visitor snd (fun _ -> true) data
let collect_trace idx tree nodes =
let rec collect_inner_node idx trace op =
match TraceNodes.find idx nodes with
| NodeData { op1; op2; stack } ->
let matching = begin match op with
| WrapperSimple | WrapperPush _ | WrapperPop | WrapperReplace _ -> Wrap op2
| Initialization | InitializationPush _ | InitializationPop | MatchDroppable -> Init op2
| MatchSimple | MatchPush _ | MatchPop | MatchReplace _ -> Pair (op1, op2)
end in collect_edge idx ((idx, stack, matching) :: trace)
| _ -> failwith "Bad tree structure"
and collect_edge idx trace =
match TraceTree.pred_e tree idx with
| [] -> trace
| [e] -> collect_inner_node (TraceTree.E.src e) trace (TraceTree.E.label e)
| _ -> failwith "Bad tree structure"
in collect_edge idx []
let extend_pm idx stack pm (tr1: TraceTypes.rich_trace) (tr2: TraceTypes.rich_trace) op =
let split = function (x, _):: l -> (x, l) | [] -> failwith "How can this be an empty list?" in
let (op2, tr2) = split tr2 in
let stack' = match op with
| WrapperPush m | MatchPush m | InitializationPush m -> m :: stack
| WrapperPop | MatchPop | InitializationPop -> List.tl stack
| WrapperSimple | MatchSimple | Initialization | MatchDroppable -> stack
| MatchReplace m | WrapperReplace m -> m :: List.tl stack in
match op with
| WrapperSimple | WrapperPush _ | WrapperPop | WrapperReplace _ ->
(pm @ [idx, stack', Wrap op2], stack', tr1, tr2)
| MatchSimple | MatchPush _ | MatchPop | MatchReplace _ ->
let (op1, tr1) = split tr1 in
(pm @ [idx, stack', Pair (op1, op2)], stack', tr1, tr2)
| Initialization | InitializationPush _ | InitializationPop | MatchDroppable ->
(pm @ [idx, stack', Init op2], stack', tr1, tr2)
let extract_data data =
List.fold_left (fun { tree; nodes } -> function
| MatchTracesObserver.RNode (id, op1, op2, stack) ->
{ tree = TraceTree.add_vertex tree id;
nodes = TraceNodes.add id (FinalNodeData { op1; op2; stack; trace_trace = [] }) nodes }
| MatchTracesObserver.REdge (src, tgt, op) ->
{ tree = TraceTree.add_edge_e tree (TraceTree.E.create src op tgt);
nodes =
let data = match TraceNodes.find src nodes with
| FinalNodeData data -> NodeData data
| NodeData data -> NodeData data
| _ -> failwith "Inconsistent trace tree"
in TraceNodes.add src data nodes }
| MatchTracesObserver.RFailure (id, fail) ->
{ tree;
nodes =
let data = match TraceNodes.find id nodes with
| FinalNodeData ({ trace_trace = [] } as node_class) ->
FinalNodeData { node_class with trace_trace = fail }
| NodeData ({ trace_trace = [] } as node_class) ->
NodeData { node_class with trace_trace = fail }
| _ -> failwith "Inconsistent trace tree"
in TraceNodes.add id data nodes }
| MatchTracesObserver.ROrigConsumedOk (id, trace, stack) ->
{ tree; nodes = TraceNodes.add id (SuccessNode) nodes }
| MatchTracesObserver.ROrigConsumedFailure (id, trace , stack) ->
{ tree; nodes = TraceNodes.add id (InitTailtraceData(trace, stack)) nodes }
| MatchTracesObserver.RXfrmConsumed (id, trace) ->
{ tree; nodes = TraceNodes.add id (EndtraceData trace) nodes }
| MatchTracesObserver.RBlockedShared (id, len1, len2, stack) ->
{ tree; nodes = TraceNodes.add id (BlockedData (len1, len2, stack)) nodes })
{ tree = TraceTree.empty; nodes = TraceNodes.empty } data
let find_fast_forward tree idx =
let step v =
match TraceTree.succ tree v with
| [ v' ] -> Some v'
| _ -> None
in let rec extend v =
match step v with
| Some v -> extend v
| None -> v
in match step idx with
| Some v -> Some (extend v)
| None -> None