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
|
import os
import sys
import tempfile
import shutil
import subprocess
import time
import hashlib
import utils
from conf import conf
from conf import sf
import exceptions
import database
def __buildtempcnf__(variable_count, files, strlines):
""" Builds temporally file for cnf formulas
variable_count - number of variables in formulas
files - list of files with formulas
strlines - list of string lines with formulas"""
lines = set()
# Copy strlines
for ln in strlines:
lines.add(ln)
# Files
for file in files:
with open(file, 'r') as f:
for ln in f:
lines.add(ln.rstrip())
first_line = "p cnf " + str(variable_count) + " " + str(len(lines))
wfile = tempfile.NamedTemporaryFile(delete=False)
wfile.write(bytes(first_line + '\n', 'UTF-8'))
for ln in lines:
wfile.write(bytes(ln + ' 0\n', 'UTF-8'))
wfile.close()
return wfile.name
def __exec_sat__(file, args):
"""Executes SAT solver and returns configuration."""
picosat_cmd = [sf(conf.picosat), file]
picosat_cmd += conf.picosat_args
stdout = utils.callsubprocess('picosat', picosat_cmd, conf.picosat_output,
True, allow_all_exit_codes = True)
rtn = []
solut = []
for line in stdout:
if line[0] == 's':
try:
solut.remove(0)
rtn.append(solut)
except ValueError:
pass
solut = []
if not line.rstrip() == 's SATISFIABLE':
raise exceptions.NoSolution()
elif line[0] == 'v':
for sl in line[2:].split():
solut.append(int(sl))
try:
solut.remove(0)
rtn.append(solut)
except ValueError:
pass
return rtn
def __write_temp_config_file__(con, conf_num):
# Ensure smap existence
utils.build_symbol_map()
# Write temporally file
wfile = tempfile.NamedTemporaryFile(delete=False)
for s in con:
if s < 0:
nt = True
s *= -1
else:
nt = False
if s > conf_num:
break;
if 'NONAMEGEN' in utils.smap[s]: # ignore generated names
continue
wfile.write(bytes('CONFIG_' + utils.smap[s] + '=',
sys.getdefaultencoding()))
if not nt:
wfile.write(bytes('y', sys.getdefaultencoding()))
else:
wfile.write(bytes('n', sys.getdefaultencoding()))
wfile.write(bytes('\n', sys.getdefaultencoding()))
wfile.close()
return wfile.name
def __load_config_file__(file):
rtn = dict()
with open(file, 'r') as f:
for ln in f:
if ln[0] == '#' or not '=' in ln:
continue
indx = ln.index('=')
if (ln[indx + 1] == 'y'):
rtn[ln[7:indx]] = True
else:
rtn[ln[7:indx]] = True
return rtn
def __calchash__(file):
"""Calculates hash from configuration file"""
# Build hashconfigsort
csort = []
try:
with open(conf.hashconfigsort, 'r') as f:
for ln in f:
csort.append(ln.rstrip())
except FileNotFoundError:
pass
con = __load_config_file__(file)
cstr = ""
for c in csort:
try:
if con[c]:
cstr += c
except ValueError:
pass
# Add missing
csortfile = open(sf(conf.hashconfigsort), 'a');
for key, val in con.items():
try:
csort.index(key)
except ValueError:
indx = len(csort)
csort.append(key)
csortfile.write(key + '\n')
if val:
cstr += key
csortfile.close()
hsh = hashlib.md5(bytes(cstr, 'UTF-8'))
return hsh.hexdigest()
def __register_conf__(con, conf_num, generator):
dtb = database.database()
# Solution to configuration
wfile = __write_temp_config_file__(con, conf_num)
hsh = __calchash__(wfile)
filen = os.path.join(sf(conf.configurations_folder), hsh)
hshf = hsh
if os.path.isfile(filen):
if compare(filen, wfile):
print("I: Generated existing configuration.")
else:
print("W: Generated configuration with collision hash.")
# TODO this might have to be tweaked
raise Exception()
shutil.move(wfile, filen)
dtb.add_configuration(hsh, hshf, generator)
def __generate_single__(var_num, conf_num):
measure_list = set()
if not os.path.isfile(sf(conf.single_generated_file)):
with open(sf(conf.measure_file), 'r') as fi:
for ln in fi:
measure_list.add(int(ln))
else:
with open(sf(conf.single_generated_file), 'r') as f:
for ln in f:
measure_list.append(int(ln))
if measure_list:
return False
tfile = __buildtempcnf__(var_num, (sf(conf.rules_file),
sf(conf.fixed_file)), (str(measure_list.pop())))
try:
confs = __exec_sat__(tfile, ['-i', '0'])
for con in confs:
__register_conf__(con, conf_num, 'single-sat')
except exceptions.NoSolution:
pass
finally:
os.remove(tfile)
with open(sf(conf.single_generated_file), 'w') as fo:
fo.writelines(measure_list)
return True
def __generate_random__(var_num, conf_num):
# TODO
#tfile = __buildtempcnf__(var_num, (sf(conf.rules_file), sf(conf.fixed_file)), ())
#try:
#confs = __exec_sat__(tfile, [])
#for con in confs:
#__register_conf__(con, conf_num)
#finally:
#os.remove(tfile)
return False
def generate():
"""Collect boolean equations from files rules and required
And get solution with picosat
"""
# Check if rules_file exist. If it was generated.
if not os.path.isfile(sf(conf.rules_file)):
raise exceptions.MissingFile(conf.rules_file,"Run parse_kconfig.")
if not os.path.isfile(sf(conf.fixed_file)):
raise exceptions.MissingFile(conf.required_file,"Run allconfig and initialization process.")
# Load variable count
with open(sf(conf.variable_count_file)) as f:
var_num = f.readline()
conf_num = f.readline()
if __generate_single__(var_num, conf_num):
return
elif __generate_random__(var_num, conf_num):
return
raise exceptions.NoNewConfiguration()
def compare(file1, file2):
"""Compared two configuration"""
conf1 = __load_config_file__(file1)
conf2 = __load_config_file__(file2)
# This is not exactly best comparison method
for key, val in conf1.items():
try:
if conf2[key] != val:
return False
except ValueError:
return False
for key, val in conf2.items():
try:
if conf1[key] != val:
return False
except ValueError:
return False
return True
|
