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
|
import os
import sys
import tempfile
import subprocess
import utils
from conf import conf
from conf import sf
from exceptions import NoSolution
def generate():
"""Collect boolean equations from files: rules, solved and required
And get solution with minisat
Relevant configurations
rules_file
solver_file
required_file
solution_file
"""
# Check if rules_file exist. If it was generated.
if not os.path.isfile(sf(conf.rules_file)):
raise Exception("Rules file missing. Run parse_kconfig and check ecistence of " + rules_file)
w_file = tempfile.NamedTemporaryFile(delete=False)
# Join files to one single temporary file
lines = set()
with open(sf(conf.rules_file), 'r') as f:
for lnn in open(sf(conf.rules_file), 'r'):
ln = lnn.rstrip()
if ln not in lines:
lines.add(ln)
if os.path.isfile(sf(conf.solved_file)):
for lnn in open(sf(conf.solved_file), 'r'):
ln = lnn.rstrip()
if ln not in lines:
lines.add(ln)
if os.path.isfile(sf(conf.required_file)):
for lnn in open((conf.required_file), 'r'):
ln = lnn.rstrip()
if ln not in lines:
lines.add(ln)
with open(sf(conf.symbol_map_file)) as f:
for var_num, l in enumerate(f):
pass
var_num += 1
lines_count = len(lines)
first_line = "p cnf " + str(var_num) + " " + str(lines_count)
w_file.write(bytes(first_line + '\n', 'UTF-8'))
for ln in lines:
w_file.write(bytes(ln + ' 0\n', 'UTF-8'))
w_file.close()
# Execute minisat
if conf.minisat_output:
subprocess.call(['minisat', w_file.name, sf(conf.solution_file)])
else:
subprocess.call(['minisat', w_file.name, sf(conf.solution_file)], stdout=subprocess.DEVNULL)
os.remove(w_file.name)
def apply():
"""Apply generated solution to kernel source.
"""
# Check if solution_file exist
if not os.path.isfile(sf(conf.solution_file)):
raise Exception("Solution file is missing. Run sat_solution and check existence of " + sf(conf.solution_file))
utils.build_symbol_map() # Ensure smap existence
# Read solution if satisfiable
with open(sf(conf.solution_file), 'r') as f:
if not f.readline().rstrip() == 'SAT':
raise NoSolution()
solut = f.readline().split()
solut.remove('0') # Remove 0 at the end
# Write solution to output_confs file
with open(sf(conf.output_confs), 'a') as f:
iteration = 0
with open(sf(conf.iteration_file)) as f:
iteration = int(f.readline)
f.write(str(iteration) + ':')
for txt in solut:
f.write(txt + ' ')
f.write('\n')
# Write negotation solution to solver_file
with open(sf(conf.solved_file), 'a') as f:
for txt in solut:
if txt[0] == '-':
ntx = ""
txt = txt[1:]
else:
ntx = "-"
f.write( ntx + txt + " ")
f.write("\n")
# Write solution to .config file in linux source folder
with open(sf(conf.linux_dot_config), 'w') as f:
for txt in solut:
if txt[0] == '-':
nt = True
txt = txt[1:]
else:
nt = False
if 'NONAMEGEN' in utils.smap[txt]: # ignore generated names
continue
f.write('CONFIG_' + utils.smap[txt] + '=')
if not nt:
f.write('y')
else:
f.write('n')
f.write('\n')
|
