From a0d366e58a94e163c6cb9f097727ce000681d182 Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Fri, 29 Jul 2022 09:21:45 -0400
Subject: [PATCH] some cleanup, added some rough parser tests, and started
altering the engines section
---
sbysrc/sby_core.py | 25 +++++++++++++++++--------
tests/parser/.gitignore | 4 ++++
tests/parser/Makefile | 2 ++
tests/parser/engines.sby | 13 +++++++++++++
tests/parser/options.sby | 4 ++++
tests/parser/setup.sby | 8 ++++++++
tests/parser/stage.sby | 12 ++++++++++++
7 files changed, 60 insertions(+), 8 deletions(-)
create mode 100644 tests/parser/.gitignore
create mode 100644 tests/parser/Makefile
create mode 100644 tests/parser/engines.sby
create mode 100644 tests/parser/options.sby
create mode 100644 tests/parser/setup.sby
create mode 100644 tests/parser/stage.sby
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 <NAME> (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 *