-
Notifications
You must be signed in to change notification settings - Fork 1
/
path_condition_generator_worker.py
708 lines (479 loc) · 32.5 KB
/
path_condition_generator_worker.py
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
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
from t_core.messages import Packet
from t_core.iterator import Iterator
import time
from multiprocessing import Process
from core.himesis_utils import expand_graph, shrink_graph, delete_graph, disjoint_model_union, print_graph, graph_to_dot, get_preds_and_succs
from copy import deepcopy
import numpy.random as nprnd
from profiler import *
from util.progress import ProgressBar
from PCDict import PCDict
#needed to use kernprof
class DummyProcess:
def join(self):
pass
def start(self):
self.run()
class path_condition_generator_worker(Process):
def __init__(self, layer_rules, rulesToTreat, rulesForSecondPhase, pruner, layer, num, report_progress, verbosity):
super(path_condition_generator_worker, self).__init__()
self.layer_rules = layer_rules
self.rulesToTreat = rulesToTreat
self.rulesForSecondPhase = rulesForSecondPhase
self.layer = layer
self.num = num
self.currentPathConditionSet = None
self.worker_list = None
self.verbosity = verbosity
self.rule_names = None
self.ruleCombinators = None
self.ruleTraceCheckers = None
self.overlappingRules = None
self.subsumption = None
self.loopingRuleSubsumption = None
nprnd.seed(num)
self.report_progress = report_progress
self.pruner = pruner
self.pc_dict = None
def load_pc_dict(self, pcs):
#print("PC length: " + str(len(pcs)))
self.pc_dict = PCDict(pcs)
def getRuleNamesInPathCondition(self, pcName):
ruleNames = []
for token in pcName.split("_"):
if token == 'E':
pass
else:
rulename = token.split("-")[0]
ruleNames.append(rulename)
return ruleNames
#@do_cprofile
#@profile
def run(self):
#start_time = time.time()
#print("Running thread")
pathConSetLength = len(self.currentPathConditionSet)
newPathConditionSet = []
new_pc_dict = {}
name_dict = {}
reverse_name_dict = {}
progress_bar = None
if self.report_progress:
progress_bar = ProgressBar(pathConSetLength)
pcs_to_prune = []
pcs_to_prune_less = []
for pathConditionIndex in range(pathConSetLength):
pc_name = self.currentPathConditionSet[pathConditionIndex]
if self.report_progress:
progress_bar.update_progress(pathConditionIndex)
pc = self.pc_dict[pc_name]
#store the preds and succs of the pc graph if needed
pc_preds = []
pc_succs = []
childrenPathConditions = [pc_name]
# produce a fresh copy of the path condition in pc_dict, associated with the name of the path condition.
# this frees up the original parent path condition that will not be changed throughout the execution of
# the rules in the layer, while its copy will. This will avoid matching over a rewritten parent path condition.
#self.pc_dict[pc_name] = shrink_graph(deepcopy(pc))
###########################################################################
# Run first phase: run all rules without any overlaps with subsuming rules
###########################################################################
for rule in self.layer_rules:
rule_name = rule.name
if self.verbosity >= 2:
print("--------------------------------------")
print("Treating rule: " + self.rule_names[rule_name])
print("Combining with:")
print("Path Condition:" + pc_name)
#if self.verbosity >= 1:
#print "Layer: " + str(self.layer+1)
#print "Number of Path Conditions generated so far: " + str(len(self.currentPathConditionSet))
#print "Number of Path Conditions Percentage: " + str(int(pathConditionIndex / float(pathConSetLength) * 100))
# calculate if the rule is in a subsuming loop and has a subsuming parent
ruleInLoopAndHasSubsumingParent = False
for loop in self.loopingRuleSubsumption:
if rule_name in loop and loop[0] != rule_name:
ruleInLoopAndHasSubsumingParent = True
# can symbolically execute only if the path condition contains no rule that subsumes
# the rule being executed or rule subsumed by the rule being executed.
# in this way we guarantee that all rules in a partial order get executed
# at least once (when the larger rules don't execute), and overlaps are
# dealt with during the second phase - i.e. all rules that execute and subsume
# others have to get their subsumed rules executed too.
if ruleInLoopAndHasSubsumingParent:
if self.verbosity:
print("Rule is in loop and has subsuming parent, skipping")
continue
subsumingRules = []
if rule_name in self.overlappingRules.keys():
subsumingRules = self.overlappingRules[rule_name]
subsumedRules = []
if rule_name in self.subsumption.keys():
subsumedRules = self.subsumption[rule_name]
# possible cases of rule combination
######################################
# Case 1: Rule has no dependencies
######################################
# the rule is disjointly added to the path condition
if len(self.ruleCombinators[rule_name]) == 1:
if self.verbosity >= 2 : print("Case 1: Rule has no dependencies")
# The rule only gets ran in the first phase if it does not overlap with any other rule.
# check if any of the subsuming rules exists in the path condition
localPathConditionLayerAccumulator = []
for child_pc_index in range(len(childrenPathConditions)):
child_pc_name = childrenPathConditions[child_pc_index]
has_subsuming = any(sRule in child_pc_name for sRule in subsumingRules)
if has_subsuming:
if self.verbosity >= 2:
print("Skipping child: " + child_pc_name + " due to presence of subsuming rule")
continue
has_subsumed = any(sRule in child_pc_name for sRule in subsumedRules)
if has_subsumed:
if self.verbosity >= 2:
print("Skipping child: " + child_pc_name + " due to presence of subsumed rule")
continue
# if not (rule_name in self.overlappingRules.keys() or\
# (rule_name in self.overlappingRules.keys() and subsumedRulesinPC)):
cpc = self.pc_dict[child_pc_name]
#take off the num of nodes in the name
cpc_name = cpc.name.split(".")[0]
new_name = cpc_name + '_' + rule_name + "-"
# create a new path condition which is the result of combining the rule with the current path condition being examined
newPathCond = cpc.copy()
newPathCond = disjoint_model_union(newPathCond,rule)
new_name += "." + str(newPathCond.vcount())
# name the new path condition as the combination of the previous path condition and the rule
newPathCond.name = new_name
if self.pruner.isPathConditionStillFeasible(newPathCond, self.rulesToTreat):
shrunk_newCond = shrink_graph(newPathCond)
self.pc_dict[new_name] = shrunk_newCond
new_pc_dict[new_name] = shrunk_newCond
if self.verbosity >= 2 : print("Created path condition with name: " + newPathCond.name)
localPathConditionLayerAccumulator.append(new_name)
#print_graph(newPathCond)
# store the newly created path condition as a child
childrenPathConditions.append(new_name)
newPathConditionSet.extend(localPathConditionLayerAccumulator)
else:
#########################################################################
# Case 2: Rule has dependencies but cannot execute because
# not all the backward links can be found in the path condition
#########################################################################
# gather the matcher for only the backward links in the rule being combined.
# it is the first matcher (LHS) of the combinators in the list.
ruleBackwardLinksMatcher = self.ruleTraceCheckers[rule_name]
# check if the backward links cannot be found by matching them on the path condition
# if not pc_preds or not pc_succs:
# pc_preds, pc_succs = get_preds_and_succs(pc)
#pc_preds = [(len(tmp), tmp) for tmp in pc.get_adjlist(mode=2)]
#pc_succs = [(len(tmp), tmp) for tmp in pc.get_adjlist(mode=1)]
p = Packet()
p.graph = pc
ruleBackwardLinksMatcher.packet_in(p, preds=pc_preds, succs=pc_succs)
if not ruleBackwardLinksMatcher.is_success:
if self.verbosity >= 2 : print("Case 2: Rule has dependencies but cannot execute")
else:
#graph_to_dot(pc.name + "_par", pc)
#########################################################################
# Case 3: Rule has dependencies that may or will execute
#########################################################################
if self.verbosity >= 2 : print("Case 3: Rule has dependencies that may or will execute")
# go through the partial and the total rule combinators
for combinator in range(2):
combinatorMatcher = self.ruleCombinators[rule_name][combinator][0]
if self.verbosity >= 2 : print("Combinator: " + combinatorMatcher.condition.name)
# check whether we are dealing with a partial or a total combinator
isTotalCombinator = False
#if combinator == len(self.ruleCombinators[rule_name]) - 1:
if combinator == 1:
isTotalCombinator = True
# find all the matches of the rule combinator in the path condition that the rule combines with
p = Packet()
p.graph = pc
#print_graph(p.graph)
combinatorMatcher.packet_in(p, preds=pc_preds, succs=pc_succs)
# if self.rule_names[rule.name] == "HereferenceOUTeTypeSolveRefEReferenceEClassifierEReferenceEClassifier":
# graph_to_dot("pathCondition_par_" + pc.name, pc)
#graph_to_dot("combinator_par_" + combinatorMatcher.condition.name, combinatorMatcher.condition)
#print_graph(combinatorMatcher.condition)
#print_graph(pc)
# now go through the path conditions resulting from combination of the rule and the
# path condition from the previous layer currently being treated in order to apply
# the combinator's RHS to every possibility of match of the combinator's LHS
if self.verbosity >= 2 :
if combinatorMatcher.is_success:
print("Matching was successful")
else:
print("Matching was not successful")
if combinatorMatcher.is_success:
# holds the result of combining the path conditions generated so far when combining
# the rule with the path condition using the multiple combinators
partialTotalPathCondLayerAccumulator = []
# now combine the rule with the newly created path condition using the current combinator
# in all the places where the rule matched on top of the path condition
i = Iterator()
#p_copy = deepcopy(p)
#p_copy = i.packet_in(p_copy)
p = i.packet_in(p)
#
# pathCondSubnum = 0
#
# while i.is_success and pathCondSubnum < 1:
#go through all the children of this path condition
for child_pc_index in range(len(childrenPathConditions)):
#get the name of the child
child_pc_name = childrenPathConditions[child_pc_index]
has_subsuming = any(sRule in child_pc_name for sRule in subsumingRules)
if has_subsuming:
if self.verbosity >= 2:
print("Skipping child: " + child_pc_name + " due to presence of subsuming rule")
continue
has_subsumed = any(sRule in child_pc_name for sRule in subsumedRules)
if has_subsumed:
if self.verbosity >= 2:
print("Skipping child: " + child_pc_name + " due to presence of subsumed rule")
continue
if self.verbosity >= 2 :
print("--> Combining with path condition: " + child_pc_name)
# # only combine if the rule hasn't executed yet on that path condition
#
# # get all the rule names in the name of the rule being executed (can be merged with subsumed rules).
# # also get the rule names of all rules already present in the path condition
# ruleNamesInRule = rule.name.split("_")
# ruleNamesInPC = child_pc_name.split("_")
# # cleanup the dashes from the rule names in the path condition
# for nameIndex in range(len(ruleNamesInPC)):
# ruleNamesInPC[nameIndex] = ruleNamesInPC[nameIndex].split("-")[0]
#get the path condition from the dictionary
cpc = self.pc_dict[child_pc_name]
# if the combinator is not the total one, make a copy of the path condition in the set
# of combinations generated so far.
# the total combinator is always the one at the end of the combinator list for the rule.
# name the new path condition as the combination of the previous path condition and the rule
newPathCondName = cpc.name.split(".")[0] + "_" + rule.name
p_copy = deepcopy(p)
newPathCond = cpc.copy()
p_copy.graph = newPathCond
rewriter = self.ruleCombinators[rule.name][combinator][1]
p_copy = rewriter.packet_in(p_copy)
newPathCond = p_copy.graph
# check if the equations on the attributes of the newly created path condition are satisfied
#if not is_consistent(newPathCond):
if not rewriter.is_success:
if self.verbosity >= 2:
print("Path Condition: " + newPathCondName + " has inconsistent equations")
# elif not self.pruner.isPathConditionStillFeasible(newPathCond,
# rulesToTreat):
# if self.verbosity >= 2:
# print("Path Condition: " + newPathCondName + " was pruned")
else:
valid = True
if isTotalCombinator:
#print("Going to write a total: " + newPathCondName)
newPathCondName = newPathCondName +"-T"# + str(pathCondSubnum)
newPathCondName += "." + str(len(newPathCond.vs))
newPathCond.name = newPathCondName
if not self.pruner.isPathConditionStillFeasible(
newPathCond, self.rulesToTreat):
valid = False
if self.verbosity >= 2:
print("Total: Possible PC: " + newPathCondName + " valid?: " + str(valid))
# because the rule combines totally with a path condition in the accumulator we just copy it
# directly on top of the accumulated path condition
# several totals my exist, so the original PC may be rewritten multiple times
# previousTotalPC = None
# writeOverPreviousTotalPC = False
if valid:
try:
reverse_name = reverse_name_dict[cpc.name]
name_dict[reverse_name] = newPathCondName
reverse_name_dict[newPathCondName] = reverse_name
except KeyError:
name_dict[cpc.name] = newPathCondName
reverse_name_dict[newPathCondName] = cpc.name
#prune the old path condition
pcs_to_prune.append(childrenPathConditions[child_pc_index])
pcs_to_prune_less.append(childrenPathConditions[child_pc_index])
#change the child's name in the child's array
childrenPathConditions[child_pc_index] = newPathCondName
else:
#print("Going to write a partial: " + newPathCondName)
newPathCondName = newPathCondName +"-P"# + str(pathCondSubnum)
newPathCondName += "." + str(len(newPathCond.vs))
newPathCond.name = newPathCondName
# we are dealing with a partial combination of the rule.
# create a copy of the path condition in the accumulator because this match of the rule is partial.
if not self.pruner.isPathConditionStillFeasible(
newPathCond, self.rulesToTreat):
valid = False
else:
# add the result to the local accumulator
partialTotalPathCondLayerAccumulator.append(newPathCond.name)
if self.verbosity >= 2:
print("Partial: Possible PC: " + newPathCondName + " valid?: " + str(valid))
# store the parent of the newly created path condition
childrenPathConditions.append(newPathCond.name)
if self.verbosity >= 2:
print("Created path condition with name: " + newPathCondName)
# store the new path condition
shrunk_newCond = shrink_graph(newPathCond)
self.pc_dict[newPathCondName] = shrunk_newCond
if valid:
new_pc_dict[newPathCondName] = shrunk_newCond
else:
pcs_to_prune.append(newPathCondName)
#p = i.next_in(p)
#pathCondSubnum += 1
newPathConditionSet.extend(partialTotalPathCondLayerAccumulator)
###########################################################################
# Run second phase: run all rules with any overlaps with subsuming rules on
# path conditions generated during the first phase
###########################################################################
# print("--------------------------------")
# print("overlapping rules: " + str(self.overlappingRules.keys()))
# print("rules in layer: " + str(ruleNamesInLayer))
# print("Rules for second phase: " + str(rulesForSecondPhase))
for pathConditionIndex2 in range(len(childrenPathConditions)):
for rule_name in self.rulesForSecondPhase:
ruleNamesInPC = []
for token in childrenPathConditions[pathConditionIndex2].split("_"):
ruleNamesInPC.append(token.split("-")[0])
# print("Rule names in PC: " + str(ruleNamesInPC))
# print("Overlaps looked for: " + str(self.overlappingRules[rule_name]))
# print("Intersection: " + str(set(self.overlappingRules[rule_name]).intersection(set(ruleNamesInPC))))
# check if any of the subsuming rules exists in the path condition's name,
# otherwise don't even try to apply the rule.
# check also if the rules has not been previously executed as a rule with no dependencies
if set(self.overlappingRules[rule_name]).intersection(set(ruleNamesInPC)) != set() and\
rule_name not in childrenPathConditions[pathConditionIndex2]:
if self.verbosity >= 2 : print("Executing rule " + self.rule_names[rule_name] + " in second phase for overlaps.")
#combinatorMatcher = None
#combinatorRewriter = None
if len(self.ruleCombinators[rule_name]) == 1:
# Case 1: Rule has no dependencies
combinatorMatcher = self.ruleCombinators[rule_name][0][0]
combinatorRewriter = self.ruleCombinators[rule_name][0][1]
else:
# Case 3: Rule has dependencies that may or will execute
combinatorMatcher = self.ruleCombinators[rule_name][2][0]
combinatorRewriter = self.ruleCombinators[rule_name][2][1]
# execute the rule
p = Packet()
cpc = self.pc_dict[childrenPathConditions[pathConditionIndex2]]
p.graph = cpc
p = combinatorMatcher.packet_in(p)
# print "----> PC Name: " + childrenPathConditions[pathConditionIndex]
#print ("-----------------------------> Match: " + str(combinatorMatcher.is_success))
i = Iterator()
p = i.packet_in(p)
# print "Match site:"
# for matchSite in p.match_sets.keys():
# print str(p.match_sets[matchSite])
numOfOverlaps = 0
while i.is_success:
numOfOverlaps = numOfOverlaps + 1
beforeOverlappingPC = p.graph.copy()
p = combinatorRewriter.packet_in(p)
if not combinatorRewriter.is_success:
if self.verbosity >= 2:
print("Graph: " + p.graph.name + " has inconsistent equations")
p.graph = beforeOverlappingPC
#print("--------------------------------> Rewrite: " + str(combinatorRewriter.is_success))
p = i.next_in(p)
newPathCond = p.graph
newPathCondName = cpc.name.split(".")[0] + "_" + rule_name + "-OVER" + str(numOfOverlaps)
newPathCondName += "." + str(len(newPathCond.vs))
# replace the original path condition by the result of overlapping the subsumed rule on it
# previousTotalPC = None
# writeOverPreviousTotalPC = False
try:
reverse_name = reverse_name_dict[cpc.name]
if reverse_name in name_dict:
pcs_to_prune.append(name_dict[reverse_name])
name_dict[reverse_name] = newPathCondName
reverse_name_dict[newPathCondName] = reverse_name
except KeyError:
name_dict[cpc.name] = newPathCondName
reverse_name_dict[newPathCondName] = cpc.name
# for nameTotalPC in name_dict.keys():
# if name_dict[nameTotalPC] == cpc.name:
# previousTotalPC = nameTotalPC
# writeOverPreviousTotalPC = True
# break
#
# if not writeOverPreviousTotalPC:
# name_dict[cpc.name] = newPathCondName
# reverse_name_dict[newPathCondName] = cpc.name
# else:
# name_dict[previousTotalPC] = newPathCondName
# reverse_name_dict[newPathCondName] = previousTotalPC
childrenPathConditions[pathConditionIndex2] = newPathCondName
if self.verbosity >= 2:
print("Second Phase: Created new path condition: " + newPathCondName)
newPathCond.name = newPathCondName
shrunk_pc = shrink_graph(newPathCond)
self.pc_dict[newPathCondName] = shrunk_pc
new_pc_dict[newPathCondName] = shrunk_pc
if not self.pruner.isPathConditionStillFeasible(pc, self.rulesToTreat):
pcs_to_prune.append(pc_name)
#print("Current length: " + str(len(self.currentPathConditionSet)))
#print("New length: " + str(len(newPathConditionSet)))
self.currentPathConditionSet = list(set(self.currentPathConditionSet))
pruning_debug = False
if self.pruner.do_pruning:
#pruning_time = time.time()
for pathCondName in pcs_to_prune:
#print("Pruning: " + pathCondName)
#
try:
del self.pc_dict[pathCondName]
if pruning_debug:
print("Pruned from new pc dict: " + pathCondName)
except KeyError:
pass
delete_graph(pathCondName)
try:
del new_pc_dict[pathCondName]
if pruning_debug:
print("Pruned from new pc dict: " + pathCondName)
except KeyError:
pass
# work around bug
if pathCondName not in pcs_to_prune_less:
try:
newPathConditionSet.remove(pathCondName)
if pruning_debug:
print("Pruned from new path cond set: " + pathCondName)
except ValueError:
pass
if pathCondName not in name_dict:
try:
self.currentPathConditionSet.remove(pathCondName)
if pruning_debug:
print("Pruned from set: " + pathCondName)
except ValueError:
pass
# else:
# del name_dict[pathCondName]
# try:
# #delete_graph(name_dict[pathCondName])
# print("Removing: " + name_dict[pathCondName])
# #del name_dict[pathCondName]
# except KeyError:
# pass
# for key, value in dict.copy(name_dict).items():
# if pathCondName == value:
# del name_dict[key]
#print("Time taken for pruning: " + str(time.time() - pruning_time))
self.currentPathConditionSet.extend(newPathConditionSet)
self.currentPathConditionSet = list(set(self.currentPathConditionSet))
# print("currentPathConditionSet: " + str(self.currentPathConditionSet))
# print("new_pc_dict: " + str(new_pc_dict.keys()))
# print("name_dict: " + str(name_dict.keys()))
if self.pruner.do_pruning:
self.pruner.print_results()
#print(asizeof.asized(self, detail = 2).format())
#print("Thread finished: Took " + str(time.time() - start_time) + " seconds")
self.worker_list[0] = self.currentPathConditionSet
self.worker_list[1] = new_pc_dict
self.worker_list[2] = name_dict