aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitignore7
-rw-r--r--conf.py13
-rw-r--r--scripts/conf.py1
-rw-r--r--scripts/exceptions.py21
-rw-r--r--scripts/initialize.py42
-rw-r--r--scripts/iteration.py12
-rwxr-xr-xscripts/kconfig_parse.py22
-rw-r--r--scripts/kernel.py27
-rwxr-xr-xscripts/main_loop.py102
-rw-r--r--scripts/phase.py37
-rwxr-xr-xscripts/sat_solution24
-rwxr-xr-xscripts/sat_solution.py46
-rw-r--r--scripts/solution.py103
-rwxr-xr-xscripts/solution_kconfig38
-rw-r--r--scripts/utils.py29
15 files changed, 388 insertions, 136 deletions
diff --git a/.gitignore b/.gitignore
index c45e46d..0e79f26 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,4 +2,11 @@
.*
!/.gitignore
+build
__*__
+
+required
+
+# Programs
+programs/kconfig_parser
+programs/solution_gen
diff --git a/conf.py b/conf.py
index 1893fcc..b006d56 100644
--- a/conf.py
+++ b/conf.py
@@ -5,27 +5,30 @@ def pf(rfile):
return os.path.dirname(os.path.realpath(__file__)) + '/' + rfile
def checkXf(f, message):
+ "Check if file is executable. If not, raise MissingFile exception."
if os.path.isfile(f) and os.access(f, os.X_OK):
return f
else:
- print('Error: Missing executable file "' + f + '"\n' + message,
- file=sys.stderr)
- return None
+ raise MissingFile(f, message)
# Global configs
SRCARCH = 'x86' # Kernel architecture
ARCH = SRCARCH
+linux_make_args = ['-j8']
# Path settings
linux_sources = pf('linux')
linux_kconfig_head = 'Kconfig'
+required = pf('required')
build_folder = pf('build/')
+phase_file = build_folder + '/phase'
symbol_map_file = build_folder + '/symbol_map' # Also defined in kconfig_parser
rules_file = build_folder + '/rules' # Also defined in kconfig_parser
solved_file = build_folder + '/solved'
required_file = build_folder + '/required'
solution_file = build_folder + '/solution'
+iteration_file = build_folder + '/iteration'
-
-kconfig_parser = checkXf(pf('programs/kconfig_parser'),'You must build programs first.')
+# Programs paths
+kconfig_parser = checkXf(pf('programs/kconfig_parser'), 'You must build programs first.')
diff --git a/scripts/conf.py b/scripts/conf.py
index fc716b1..c2f891d 100644
--- a/scripts/conf.py
+++ b/scripts/conf.py
@@ -1,4 +1,3 @@
-#!/bin/python3
# This file is only loading ../conf.py
import os
import importlib.machinery
diff --git a/scripts/exceptions.py b/scripts/exceptions.py
new file mode 100644
index 0000000..722c44a
--- /dev/null
+++ b/scripts/exceptions.py
@@ -0,0 +1,21 @@
+class MissingFile(Exception):
+ def __init__(self, f, advice):
+ self.f = f
+ self.advice = advice
+ def __str__(self):
+ if advice == None:
+ return "No required file: " + f
+ else:
+ return "No required file: " + f + "\n" + advice
+
+class NoSolution(Exception):
+ def __init__(self):
+ pass
+ def __str__(self):
+ return "SAT solver found no solution. Statement is not satisfiable."
+
+class PhaseMismatch(Exception):
+ def __init__(self):
+ pass
+ def __str__(self):
+ return "Phase in " + conf.phase_file + " is unknown."
diff --git a/scripts/initialize.py b/scripts/initialize.py
new file mode 100644
index 0000000..2895444
--- /dev/null
+++ b/scripts/initialize.py
@@ -0,0 +1,42 @@
+import os
+import sys
+import subprocess
+
+import utils
+from conf import conf
+from exceptions import MissingFile
+
+def kconfig_parser():
+ "Execute kconfig_parser in linux_sources directory and parsed output is placed to build_folder."
+ env = dict(os.environ)
+ env['SRCARCH'] = conf.SRCARCH
+ env['ARCH'] = conf.ARCH
+ env['KERNELVERSION'] = 'KERNELVERSION' # hides error
+ wd = os.getcwd()
+ os.chdir(conf.linux_sources)
+ subprocess.call([conf.kconfig_parser, conf.linux_kconfig_head, conf.build_folder], env=env)
+ os.chdir(wd)
+
+def gen_requred():
+ "Generates required depenpency from required file."
+ utils.build_symbol_map()
+ srmap = {value:key for key, value in utils.smap.items()}
+
+ if not os.path.isfile(conf.required):
+ raise MissingFile(conf.required, None)
+
+ try:
+ os.remove(conf.required_file)
+ except OSError:
+ pass
+
+ with open(conf.required_file, 'w') as fout:
+ with open(conf.required, 'r') as f:
+ for line in f:
+ for word in line.rstrip().split():
+ if word[0] == '-':
+ fout.write('-')
+ word = word[1:]
+ fout.write(srmap[word] + " ")
+ fout.write("\n")
+
diff --git a/scripts/iteration.py b/scripts/iteration.py
new file mode 100644
index 0000000..f885b37
--- /dev/null
+++ b/scripts/iteration.py
@@ -0,0 +1,12 @@
+from conf import conf
+
+def reset():
+ with open(conf.iteration_file, 'w') as f:
+ f.write('0')
+
+def inc():
+ with open(conf.iteration_file, 'r') as f:
+ it = int(f.read())
+ it += 1
+ with open(conf.iteration_file, 'w') as f:
+ f.write(str(it))
diff --git a/scripts/kconfig_parse.py b/scripts/kconfig_parse.py
deleted file mode 100755
index 36d690b..0000000
--- a/scripts/kconfig_parse.py
+++ /dev/null
@@ -1,22 +0,0 @@
-#!/bin/python3
-import os
-import sys
-import subprocess
-from conf import conf
-
-def kconfig_parser():
- "Execute kconfig_parser in linux_sources directory and parsed output is placed to build_folder."
- env = dict(os.environ)
- env['SRCARCH'] = conf.SRCARCH
- env['ARCH'] = conf.ARCH
- env['KERNELVERSION'] = 'KERNELVERSION'
- wd = os.getcwd()
- os.chdir(conf.linux_sources)
- subprocess.call([conf.kconfig_parser, conf.linux_kconfig_head, conf.build_folder],
- env=env)
-
-def main():
- kconfig_parser()
-
-if __name__ == "__main__":
- main()
diff --git a/scripts/kernel.py b/scripts/kernel.py
new file mode 100644
index 0000000..f50a616
--- /dev/null
+++ b/scripts/kernel.py
@@ -0,0 +1,27 @@
+import os
+import sys
+import subprocess
+
+import utils
+from conf import conf
+
+
+def config():
+ # Executing old linux config
+ env = dict(os.environ)
+ wd = os.getcwd()
+ os.chdir(conf.linux_sources)
+ sprc = subprocess.Popen(['make', 'oldconfig'], env=utils.get_kernel_env())
+ for line in sprc.stdout:
+ if line == "* Restart config...":
+ print("Configuration failed")
+ sprc.kill()
+ else:
+ print(line)
+ os.chdir(wd)
+
+def make():
+ wd = os.getcwd()
+ os.chdir(conf.linux_sources)
+ subprocess.call(['make', '-j8'], env=utils.get_kernel_env())
+ os.chdir(wd)
diff --git a/scripts/main_loop.py b/scripts/main_loop.py
new file mode 100755
index 0000000..9dd8c08
--- /dev/null
+++ b/scripts/main_loop.py
@@ -0,0 +1,102 @@
+#!/bin/python3
+import os
+import sys
+import subprocess
+import signal
+from threading import Thread
+
+from conf import conf
+import initialize
+import phase
+import solution
+import kernel
+from exceptions import MissingFile
+import iteration
+
+def step():
+ phs = phase.get()
+ if phs == phase.phs("Not Initialized"):
+ try:
+ os.mkdir(conf.build_folder)
+ except FileExistsError:
+ pass
+ phase.set(1)
+ elif phs == phase.phs("Initializing"):
+ print("-- Initializing ...")
+ initialize.kconfig_parser()
+ try:
+ initialize.gen_requred()
+ except MissingFile:
+ pass
+ iteration.reset()
+ phase.set(2)
+ elif phs == phase.phs("Initialized"):
+ print("-- Initialized")
+ phase.set(3)
+ elif phs == phase.phs("Solution generating"):
+ print("-- Generating solution ...")
+ solution.generate()
+ iteration.inc()
+ phase.set(4)
+ elif phs == phase.phs("Solution generated"):
+ print("-- Solution generated")
+ phase.set(5)
+ elif phs == phase.phs("Solution applying"):
+ print("-- Applying generated solution ...")
+ solution.apply()
+ phase.set(6)
+ elif phs == phase.phs("Solution applied"):
+ print("-- Generated solution applied")
+ phase.set(2) # TODO edited
+ elif phs == phase.phs("Kernel configuration"):
+ print("-- Kernel configure ...")
+ phase.set(8)
+ elif phs == phase.phs("Kernel configured"):
+ print("-- Kernel configured")
+ phase.set(9)
+ elif phs == phase.phs("Kernel build"):
+ print("-- Build Linux ...")
+ kernel.build()
+ phase.set(10)
+ elif phs == phase.phs("Kernel built"):
+ print("-- Linux built")
+ phase.set(2)
+
+# TODO repair, not working
+def reset():
+ os.rmdir(conf.build_folder)
+ os.chdir(conf.linux_sources)
+ subprocess.call(['make','clean'])
+ os.rm('.config') # remove linux config file
+
+
+class mainThread(Thread):
+ def __init__(self, name):
+ Thread.__init__(self, name=name)
+ self.term = False
+ def run(self):
+ while not self.term:
+ step()
+
+def loop_term():
+ global thr
+ thr.term = True
+
+def sigterm_handler(_signo, _stack_frame):
+ loop_term()
+
+def main_loop():
+ global thr
+ thr = mainThread("thred")
+ thr.start()
+ try:
+ thr.join()
+ except KeyboardInterrupt:
+ loop_term()
+
+#################################################################################
+
+if __name__ == '__main__':
+ print("Start")
+ signal.signal(signal.SIGTERM, sigterm_handler)
+ main_loop()
diff --git a/scripts/phase.py b/scripts/phase.py
new file mode 100644
index 0000000..6578b13
--- /dev/null
+++ b/scripts/phase.py
@@ -0,0 +1,37 @@
+import os
+import sys
+
+from conf import conf
+
+phases = ("Not Initialized", #0
+ "Initializing", #1
+ "Initialized", #2
+ "Solution generating", #3
+ "Solution generated", #4
+ "Solution applying", #5
+ "Solution applied", #6
+ "Kernel configuration", #7
+ "Kernel configured", #8
+ "Kernel build", #9
+ "Kernel built" #10
+ )
+
+def get():
+ try:
+ with open(conf.phase_file) as f:
+ txtPhase = f.readline().rstrip()
+ if not txtPhase in phases:
+ raise PhaseMismatch()
+ return phases.index(txtPhase)
+ except FileNotFoundError:
+ return 0
+
+def set(phs):
+ with open(conf.phase_file, 'w') as f:
+ f.write(phases[phs])
+
+def pset(str):
+ set(phase.index(str))
+
+def phs(str):
+ return phases.index(str)
diff --git a/scripts/sat_solution b/scripts/sat_solution
deleted file mode 100755
index 07d5118..0000000
--- a/scripts/sat_solution
+++ /dev/null
@@ -1,24 +0,0 @@
-#!/bin/bash
-
-SAT_FOLDER=$1
-RULES="$1/rules"
-SOLUTION="$1/solution"
-
-W_FILE=`mktemp`
-
-if [ -r "$RULES" ]; then
- cat "$RULES" | sed 's/$/ 0/' > "$W_FILE"
-else
- echo "Error: No rules file in specified folder." 1>&2
- exit 1
-fi
-
-RL_COUNT=`wc -l < "$W_FILE"`
-NUM_VAR=`tail -1 "$RULES" | sed 's/ .*//' | sed 's/-//'`
-sed -i "1ip cnf $NUM_VAR $RL_COUNT" "$W_FILE"
-echo "CLAUSELES: $RL_COUNT"
-echo "VARIABLES: $NUM_VAR"
-
-minisat "$W_FILE" "$SOLUTION"
-
-rm "$W_FILE"
diff --git a/scripts/sat_solution.py b/scripts/sat_solution.py
deleted file mode 100755
index 1a44678..0000000
--- a/scripts/sat_solution.py
+++ /dev/null
@@ -1,46 +0,0 @@
-#!/bin/python3
-import os
-import sys
-import tempfile
-import subprocess
-from conf import conf
-
-if not os.path.isfile(conf.rules_file):
- print("Error: Rules are not generated yet, or wrong build_folder.\nCheck existence of " + rules_file, file=sys.stderr)
- sys.exit(1)
-
-
-#w_file = tempfile.NamedTemporaryFile(delete=False)
-w_file = open('bld', 'w')
-# Join files to one single file
-lines = set()
-for ln in open(conf.rules_file, 'r'):
- if ln not in lines:
- lines.add(ln)
-if os.path.isfile(conf.solved_file):
- for ln in open(conf.solved_file, 'r'):
- if ln not in lines:
- lines.add(ln)
-if os.path.isfile(conf.required_file):
- for ln in open(conf.required_file, 'r'):
- if ln not in lines:
- lines.add(ln)
-
-with open(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(first_line + '\n')
-for ln in lines:
- w_file.write(ln)
-
-w_file.close()
-
-print("temp file: " + w_file.name)
-print("Output: " + conf.solution_file)
-subprocess.call(['minisat', w_file.name, conf.solution_file])
-
-#os.remove(w_file.name)
diff --git a/scripts/solution.py b/scripts/solution.py
new file mode 100644
index 0000000..0ad1c4f
--- /dev/null
+++ b/scripts/solution.py
@@ -0,0 +1,103 @@
+import os
+import sys
+import tempfile
+import subprocess
+
+import utils
+from conf import conf
+
+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(conf.rules_file):
+ raise Exception("Rules file missing. Run kconfig_parse and check ecistence of " + rules_file)
+
+ w_file = tempfile.NamedTemporaryFile(delete=False)
+ # Join files to one single temporary file
+ lines = set()
+ with open(conf.rules_file, 'r') as f:
+ for lnn in open(conf.rules_file, 'r'):
+ ln = lnn.rstrip()
+ if ln not in lines:
+ lines.add(ln)
+ if os.path.isfile(conf.solved_file):
+ for lnn in open(conf.solved_file, 'r'):
+ ln = lnn.rstrip()
+ if ln not in lines:
+ lines.add(ln)
+ if os.path.isfile(conf.required_file):
+ for lnn in open(conf.required_file, 'r'):
+ ln = lnn.rstrip()
+ if ln not in lines:
+ lines.add(ln)
+
+ with open(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
+ subprocess.call(['minisat', w_file.name, conf.solution_file])
+
+ os.remove(w_file.name)
+
+def apply():
+ """Apply generated solution to kernel source.
+ """
+ # Check if solution_file exist
+ if not os.path.isfile(conf.solution_file):
+ raise Exception("Solution file is missing. Run sat_solution and check existence of " + conf.solution_file)
+
+ utils.build_symbol_map() # Ensure smap existence
+
+ # Read solution if satisfiable
+ with open(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 negotation solution to solver_file
+ with open(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(conf.linux_sources + '/.config', 'w') as f:
+ for txt in solut:
+ if txt[0] == '-':
+ nt = True
+ txt = txt[1:]
+ else:
+ nt = False
+ if 'NONAMEGEN' in txt: # ignore generated names
+ continue
+
+ f.write('CONFIG_' + utils.smap[txt] + '=')
+ if not nt:
+ f.write('y')
+ else:
+ f.write('n')
+ f.write('\n')
diff --git a/scripts/solution_kconfig b/scripts/solution_kconfig
deleted file mode 100755
index 7f9e5dd..0000000
--- a/scripts/solution_kconfig
+++ /dev/null
@@ -1,38 +0,0 @@
-#!/bin/bash
-
-SAT_FOLDER="$1"
-CONF="$2"
-LINKER="$1/linker"
-SOLUTION="$1/solution"
-
-SAT=`head -1 "$SOLUTION"`
-SOL=`tail -1 "$SOLUTION"`
-
-if [[ ! -w "$CONF" ]]; then
- echo "No file \"$CONF\"" >&2
- exit 1
-fi
-
-if [[ "$SAT" != "SAT" ]]; then
- echo "No solution" >&2
- exit 1
-fi
-
-for exp in $SOL; do
- if [[ "$exp" != "0" ]]; then
- if [[ `echo "$exp" | head -c 1` = "-" ]]; then
- exp=`echo "$exp" | cut -c 2-`
- not="n"
- else
- not="y"
- fi
- lnk=`grep -e "^$exp:" "$LINKER" | sed 's/^[0-9]*\://'`
- if [[ "$lnk" != NONAMEGEN* ]]; then # Ignore no name configs
- if [[ -z `grep "^CONFIG_$lnk" "$CONF"` ]]; then
- echo "CONFIG_$lnk=$not" >> "$CONF"
- else
- sed "s/^CONFIG_$lnk=.*/CONFIG_$lnk=$not/" "$CONF" > "$CONF"
- fi
- fi
- fi
-done
diff --git a/scripts/utils.py b/scripts/utils.py
new file mode 100644
index 0000000..55ccb50
--- /dev/null
+++ b/scripts/utils.py
@@ -0,0 +1,29 @@
+import os
+import sys
+from conf import conf
+from exceptions import MissingFile
+
+def build_symbol_map():
+ """Generates global variable smap from symbol_map_file.
+ When file not exists, MissingFile exception is raised.
+ """
+ global smap
+ try:
+ smap
+ except NameError:
+ # Check if symbol_map_file exist
+ if not os.path.isfile(conf.symbol_map_file):
+ raise MissingFile(conf.symbol_map_file, "Run kconfig_parser to generate it.")
+
+ smap = dict()
+ with open(conf.symbol_map_file) as f:
+ for lnn in f:
+ w = lnn.rstrip().split(sep=':')
+ smap[w[0]] = w[1]
+
+def get_kernel_env():
+ env = dict(os.environ)
+ env['SRCARCH'] = conf.SRCARCH
+ env['ARCH'] = conf.ARCH
+ env['KERNELVERSION'] = 'KERNELVERSION' # hides error
+ return env