Newer
Older
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
#!/usr/bin/python3
import re
import os
import sys
debug = True
lines = sys.stdin.readlines()
lemma = sys.argv[1]
# INPUT:
# - lines contain a list of "%i:goal" where "%i" is the index of the goal
# - lemma contain the name of the lemma under scrutiny
# OUTPUT:
# - (on stdout) a list of ordered index separated by EOL
vk=dict()
rank = [] # list of list of goals, main list is ordered by priority
maxPrio = 124
for i in range(0,maxPrio):
rank.append([])
if lemma!="AnyLemma":
print("applying lemma")
for line in lines:
num = line.split(':')[0]
if re.match('.*!Pk\(.*', line): rank[106].append(num)
elif re.match('.*!Ltk\(.*', line): rank[106].append(num)
elif re.match('.*!PkCPS\(.*', line): rank[106].append(num)
elif re.match('.*!LtkCPS\(.*', line): rank[106].append(num)
elif re.match('.*!CP_Init\(.*', line): rank[106].append(num)
elif re.match('.*EV_Data_Keys.*', line): rank[109].append(num)
elif re.match('.*EV_Start_Auth.*', line): rank[109].append(num)
elif re.match('.*TPM_Keys.*', line): rank[109].append(num)
elif re.match('.*EV_Data.*', line): rank[108].append(num)
elif re.match('.*TPM_EK_QPD.*', line): rank[108].append(num)
elif re.match('.*!TPM_EK_QPD.*', line): rank[108].append(num)
elif re.match('.*CertRes.*', line): rank[107].append(num)
elif re.match('.*!CertRes.*', line): rank[107].append(num)
elif re.match('.*CertReq.*', line): rank[107].append(num) #?
elif re.match('.*!KU\( ~x.*', line): rank[101].append(num)
elif re.match('.*!KU\( ~y.*', line): rank[101].append(num)
elif re.match('.*!KU\( ~sk.*', line): rank[101].append(num)
elif re.match('.*!KU\( ~g.*', line): rank[101].append(num)
elif re.match('.*!KD\(.*', line): rank[97].append(num)
elif re.match('.*!KU\( \'ch.*', line): rank[96].append(num)
elif re.match('.*!KU\( \$\w+ .*', line): rank[95].append(num)
elif re.match('.*~~>.*', line):
if re.match('.*\(#i.*', line): rank[91].append(num)
elif re.match('.*\(#vk\..*', line):
i=re.search('.*\(#vk\.(\d+),.*', line).group(1)
vk[int(i)]=num
rank[92]=[vk[key] for key in sorted(vk.keys())]
elif re.match('.*\(#vk.*', line): rank[93].append(num)
else: rank[90].append(num) # 86?
elif re.match('.*!KU\( Pk.*', line): rank[22].append(num)
elif re.match('.*!KU\( multp\(.*\'P2\'\)', line): rank[22].append(num)
#
elif re.match('.*!KU\( E_S.*', line): rank[40].append(num)
elif re.match('.*!KU\( \'.*', line): rank[39].append(num)
elif re.match('.*!KU\( multp.*', line): rank[33].append(num)
elif re.match('.*!KU\( plus.*', line): rank[33].append(num)
elif re.match('.*!KU\( Nonce.*', line): rank[33].append(num)
elif re.match('.*!KU\( sign.*', line): rank[33].append(num)
elif re.match('.*!KU\( H_n_2.*', line): rank[22].append(num)
elif re.match('.*!KU\( pk\(.*', line): rank[22].append(num)
elif re.match('.*!KU\( H_k_7.*', line): rank[21].append(num)
elif re.match('.*!KU\( H_k_2.*', line): rank[21].append(num)
elif re.match('.*!KU\( h\(<\$CP.*', line): rank[19].append(num)
elif re.match('.*!KU\( h\(.*', line): rank[20].append(num)
elif re.match('.*!KU\( MAC\(.*', line): rank[20].append(num)
elif re.match('.*!KU\( H_SHA256.*', line): rank[19].append(num)
elif re.match('.*!KU\( BSN.*', line): rank[19].append(num)
elif re.match('.*!KU\( ~i_x.*', line): rank[19].append(num)
elif re.match('.*!KU\( QPub.*', line): rank[19].append(num)
elif re.match('.*!KU\( certData.*', line): rank[19].append(num)
elif re.match('.*!KU\( \$CP\..*', line): rank[23].append(num) #?
#
elif re.match('.*!KU\( ~.*', line): rank[92].append(num)
elif re.match('.*!KU\( i_x_t.*', line): rank[8].append(num)
elif re.match('.*!KU\( dataID.*', line): rank[7].append(num)
elif re.match('.*!KU\( sid.*', line): rank[7].append(num)
elif re.match('.*!KU\( nonce.*', line): rank[6].append(num)
elif re.match('.*!KU\( x.*', line): rank[5].append(num)
elif re.match('.*!KU\( n.*', line): rank[4].append(num)
elif re.match('.*', line): rank[15].append(num)
else:
exit(0)
# Ordering all goals by ranking (higher first)
for listGoals in reversed(rank):
for goal in listGoals:
sys.stderr.write(goal)
print(goal)