diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 9264569..8f988a6 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -246,7 +246,8 @@ class SbyAbort(BaseException): class SbyConfig: def __init__(self): self.options = dict() - self.engines = list() + # Define a default case for the engine block + self.engines = list() # { None: list() } self.setup = dict() self.stage = dict() self.script = list() @@ -257,6 +258,7 @@ class SbyConfig: def parse_config(self, f): mode = None + engine_mode = None for line in f: raw_line = line @@ -290,18 +292,26 @@ class SbyConfig: if section == "engines": mode = "engines" - if len(self.engines) != 0: - self.error(f"sby file syntax error: '[engines]' section already defined") - if args is not None: - self.error(f"sby file syntax error: '[engines]' section does not accept any arguments. got {args}") - continue + if len(entries) > 2: + self.error(f"sby file syntax error: [engine] sections expects at most 1 argument, got more '{line}'") + if len(entries) == 2 and entries[1] not in ("bmc", "prove", "cover", "live"): + self.error(f"sby file syntax error: Expected one of 'bmc, prove, cover, live' not '{entries[1]}'") + elif len(entries) == 2: + pass + # if entries[1] not in self.engines: + # self.engines[entries[1]] = list() + # else: + # self.error(f"Already defined engine block for mode '{entries[1]}'") + + # [setup] if entries[0] == "setup": mode = "setup" if len(self.setup) != 0 or len(entries) != 1: self.error(f"sby file syntax error: {line}") continue + # [stage (PARENTS...)] if entries[0] == "stage": mode = "stage" if len(entries) > 3 or len(entries) < 2: @@ -377,11 +387,11 @@ class SbyConfig: if mode == "engines": entries = line.split() + # self.engines[engine_mode].append(entries) self.engines.append(entries) continue if mode == "setup": - self.error("[setup] section not yet supported") kvp = line.split() if kvp[0] not in ("cutpoint", "disable", "enable", "assume", "define"): self.error(f"sby file syntax error: {line}") @@ -403,7 +413,6 @@ class SbyConfig: continue if mode == "stage": - self.error("[stage] section not yet supported") kvp = line.split() if key is None or key == '': self.error(f"sby file syntax error: in stage mode but unknown key") diff --git a/tests/parser/.gitignore b/tests/parser/.gitignore new file mode 100644 index 0000000..b87b190 --- /dev/null +++ b/tests/parser/.gitignore @@ -0,0 +1,4 @@ +* +!Makefile +!.gitignore +!*.sby diff --git a/tests/parser/Makefile b/tests/parser/Makefile new file mode 100644 index 0000000..7827c43 --- /dev/null +++ b/tests/parser/Makefile @@ -0,0 +1,2 @@ +SUBDIR=parser +include ../make/subdir.mk diff --git a/tests/parser/engines.sby b/tests/parser/engines.sby new file mode 100644 index 0000000..2277151 --- /dev/null +++ b/tests/parser/engines.sby @@ -0,0 +1,13 @@ +[options] +mode bmc +depth 1 +expect error + +[engines] +smtbmc + +[engines bmc] +smtbmc + +[engines cover] +smtbmc diff --git a/tests/parser/options.sby b/tests/parser/options.sby new file mode 100644 index 0000000..666953d --- /dev/null +++ b/tests/parser/options.sby @@ -0,0 +1,4 @@ +[options] +mode bmc +depth 1 +expect error diff --git a/tests/parser/setup.sby b/tests/parser/setup.sby new file mode 100644 index 0000000..6ca49e3 --- /dev/null +++ b/tests/parser/setup.sby @@ -0,0 +1,8 @@ +[options] +mode bmc +depth 1 +expect error + + +[setup] +enable * diff --git a/tests/parser/stage.sby b/tests/parser/stage.sby new file mode 100644 index 0000000..b69a186 --- /dev/null +++ b/tests/parser/stage.sby @@ -0,0 +1,12 @@ +[options] +mode bmc +depth 1 +expect error + + +[stage stage_1] +mode prove +depth 20 +timeout 60 +expect error +enable *