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
|
import os
import sys
import tempfile
import subprocess
import time
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', conf.picosat_cmd, conf.picosat_output, ".")
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))
return rtn
def __write_temp_config_file__(conf):
# Ensure smap existence
utils.build_symbol_map()
# Load variable count
with open(sf(conf.variable_count_file)) as f:
f.readline()
var_num = int(f,readline())
# Write temporally file
wfile = tempfile.NamedTemporaryFile(delete=False)
for s in conf:
if s < 0:
nt = True
s *= -1
else:
nt = False
if s > var_num:
break;
if 'NONAMEGEN' in utils.smap[s]: # ignore generated names
continue
wfile.write('CONFIG_' + utils.smap[s] + '=')
if not nt:
wfile.write('y')
else:
wfile.write('n')
wfile.write('\n')
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[line[7:indx]] = True
else:
rtn[line[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
conf = __load_config_file__(file)
cstr = ""
for c in csort:
try:
if conf[c]:
cstr += '+'
else:
cstr += '-'
except ValueError:
cstr += '0'
# Add missing
csortfile = open(conf.hashconfigsort, 'a');
for key, val in conf:
try:
csort.index(key)
except ValueError:
indx = len(csort)
csort.append(key)
csortfile.write(key + '\n')
if val:
cstr += '+'
else:
cstr += '-'
close(csortfile)
hsh = hashlib.md5(bytes(cstr, 'UTF-8'))
return hsh.hexdigest()
def __register_conf__(conf):
with open(sf(conf.variable_count_file)) as f:
var_num = int(f.readline())
dtb = database.database()
# Solution to configuration
wfile = __write_temp_config_file__(conf)
hsh = __calchash__(wfile.name)
filen = os.path.join(sf(conf.configuration_folder, hsh))
hshf = hsh
if os.path.isfile(filen):
if compare(filen, wfile):
print("I: Generated existing configuration.")
continue
else:
print("W: Generated configuration with collision hash.")
# TODO this might have to be tweaked
raise Exception()
os.rename(wfile.name, filen)
dtb.add_configuration(hsh, hshf)
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.required_file)):
raise exceptions.MissingFile(conf.required_file,"Run allconfig.")
tfile = __buildtempcnf__(var_num, (conf.rules_file, conf.required_file), ())
try:
confs = __exec_sat__(tfile)
os.remove(tfile)
for conf in confs:
__register_conf__(conf)
except exceptions.NoSolution:
os.remove(tfile)
raise exceptions.NoSolution()
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:
try:
if conf2[key] != val:
return False
except ValueError:
return False
for key, val in conf2:
try:
if conf1[key] != val:
return False
except ValueError:
return False
return True
|
