From 0caa62802ccb3ee67e05c948a9e334504cae9cc4 Mon Sep 17 00:00:00 2001 From: "William D. Jones" Date: Fri, 6 Jul 2018 01:36:41 -0400 Subject: Gate POSIX-only signals and resource module to only run on POSIX Python implementations. --- backends/smt2/smtio.py | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) (limited to 'backends/smt2/smtio.py') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 1a8d2484c..3fc823e3e 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -17,7 +17,9 @@ # import sys, re, os, signal -import resource, subprocess +import subprocess +if os.name == "posix": + import resource from copy import deepcopy from select import select from time import time @@ -27,12 +29,13 @@ from threading import Thread # This is needed so that the recursive SMT2 S-expression parser # does not run out of stack frames when parsing large expressions -smtio_reclimit = 64 * 1024 -smtio_stacksize = 128 * 1024 * 1024 -if sys.getrecursionlimit() < smtio_reclimit: - sys.setrecursionlimit(smtio_reclimit) -if resource.getrlimit(resource.RLIMIT_STACK)[0] < smtio_stacksize: - resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, -1)) +if os.name == "posix": + smtio_reclimit = 64 * 1024 + smtio_stacksize = 128 * 1024 * 1024 + if sys.getrecursionlimit() < smtio_reclimit: + sys.setrecursionlimit(smtio_reclimit) + if resource.getrlimit(resource.RLIMIT_STACK)[0] < smtio_stacksize: + resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, -1)) # currently running solvers (so we can kill them) @@ -51,8 +54,9 @@ def force_shutdown(signum, frame): os.kill(p.pid, signal.SIGTERM) sys.exit(1) +if os.name == "posix": + signal.signal(signal.SIGHUP, force_shutdown) signal.signal(signal.SIGINT, force_shutdown) -signal.signal(signal.SIGHUP, force_shutdown) signal.signal(signal.SIGTERM, force_shutdown) def except_hook(exctype, value, traceback): @@ -1053,4 +1057,3 @@ class MkVcd: print("b0 %s" % self.nets[path][0], file=self.f) else: print("b1 %s" % self.nets[path][0], file=self.f) - -- cgit v1.2.3 From 2b935421718c9a8d8f2183d9cb4a4973c078bcfa Mon Sep 17 00:00:00 2001 From: Arjen Roodselaar Date: Sun, 4 Nov 2018 21:58:09 -0800 Subject: Use conservative stack size for SMT2 on MacOS --- backends/smt2/smtio.py | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'backends/smt2/smtio.py') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 3fc823e3e..e8ed5e63b 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -32,10 +32,15 @@ from threading import Thread if os.name == "posix": smtio_reclimit = 64 * 1024 smtio_stacksize = 128 * 1024 * 1024 + smtio_stacklimit = resource.RLIM_INFINITY + if os.uname().sysname == "Darwin": + # MacOS has rather conservative stack limits + smtio_stacksize = 16 * 1024 * 1024 + smtio_stacklimit = resource.getrlimit(resource.RLIMIT_STACK)[1] if sys.getrecursionlimit() < smtio_reclimit: sys.setrecursionlimit(smtio_reclimit) if resource.getrlimit(resource.RLIMIT_STACK)[0] < smtio_stacksize: - resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, -1)) + resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, smtio_stacklimit)) # currently running solvers (so we can kill them) -- cgit v1.2.3 From 79075d123f749ad39bf35f658f00a79a24efcf98 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 6 Nov 2018 10:05:23 +0100 Subject: Improve stack rlimit code in smtio.py Signed-off-by: Clifford Wolf --- backends/smt2/smtio.py | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'backends/smt2/smtio.py') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index e8ed5e63b..e417b7758 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -31,16 +31,16 @@ from threading import Thread # does not run out of stack frames when parsing large expressions if os.name == "posix": smtio_reclimit = 64 * 1024 - smtio_stacksize = 128 * 1024 * 1024 - smtio_stacklimit = resource.RLIM_INFINITY - if os.uname().sysname == "Darwin": - # MacOS has rather conservative stack limits - smtio_stacksize = 16 * 1024 * 1024 - smtio_stacklimit = resource.getrlimit(resource.RLIMIT_STACK)[1] if sys.getrecursionlimit() < smtio_reclimit: sys.setrecursionlimit(smtio_reclimit) - if resource.getrlimit(resource.RLIMIT_STACK)[0] < smtio_stacksize: - resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, smtio_stacklimit)) + + smtio_stacksize = 128 * 1024 * 1024 + current_rlimit_stack = resource.getrlimit(resource.RLIMIT_STACK) + if current_rlimit_stack[0] != resource.RLIM_INFINITY: + if current_rlimit_stack[1] != resource.RLIM_INFINITY: + smtio_stacksize = min(smtio_stacksize, smtio_stacklimit) + if current_rlimit_stack[0] < smtio_stacksize: + resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, current_rlimit_stack[1])) # currently running solvers (so we can kill them) -- cgit v1.2.3 From 4c50e3abb9b39fe088cc0a08c63fcadb8abdabb7 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 6 Nov 2018 10:09:03 +0100 Subject: Fix for improved smtio.py rlimit code Signed-off-by: Clifford Wolf --- backends/smt2/smtio.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backends/smt2/smtio.py') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index e417b7758..108f6bcfe 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -38,7 +38,7 @@ if os.name == "posix": current_rlimit_stack = resource.getrlimit(resource.RLIMIT_STACK) if current_rlimit_stack[0] != resource.RLIM_INFINITY: if current_rlimit_stack[1] != resource.RLIM_INFINITY: - smtio_stacksize = min(smtio_stacksize, smtio_stacklimit) + smtio_stacksize = min(smtio_stacksize, current_rlimit_stack[1]) if current_rlimit_stack[0] < smtio_stacksize: resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, current_rlimit_stack[1])) -- cgit v1.2.3 From f6c4485a3ac315fbed76f1a2e1f22df7afb36886 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 6 Nov 2018 11:11:05 +0100 Subject: Run solver in non-incremental mode whem smtio.py is configured for non-incremental solving Signed-off-by: Clifford Wolf --- backends/smt2/smtio.py | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) (limited to 'backends/smt2/smtio.py') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index e8ed5e63b..4c3245984 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -163,19 +163,28 @@ class SmtIo: self.unroll = False if self.solver == "yices": - self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts + if self.noincr: + self.popen_vargs = ['yices-smt2'] + self.solver_opts + else: + self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts if self.solver == "z3": self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts if self.solver == "cvc4": - self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts + if self.noincr: + self.popen_vargs = ['cvc4', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts + else: + self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts if self.solver == "mathsat": self.popen_vargs = ['mathsat'] + self.solver_opts if self.solver == "boolector": - self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts + if self.noincr: + self.popen_vargs = ['boolector', '--smt2'] + self.solver_opts + else: + self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts self.unroll = True if self.solver == "abc": -- cgit v1.2.3 From b54bf7c0f9720526dffce684ef1353b81f99547c Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 7 Nov 2018 15:32:34 +0100 Subject: Limit stack size to 16 MB on Darwin Signed-off-by: Clifford Wolf --- backends/smt2/smtio.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'backends/smt2/smtio.py') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 108f6bcfe..afbcf1fc4 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -34,9 +34,12 @@ if os.name == "posix": if sys.getrecursionlimit() < smtio_reclimit: sys.setrecursionlimit(smtio_reclimit) - smtio_stacksize = 128 * 1024 * 1024 current_rlimit_stack = resource.getrlimit(resource.RLIMIT_STACK) if current_rlimit_stack[0] != resource.RLIM_INFINITY: + smtio_stacksize = 128 * 1024 * 1024 + if os.uname().sysname == "Darwin": + # MacOS has rather conservative stack limits + smtio_stacksize = 16 * 1024 * 1024 if current_rlimit_stack[1] != resource.RLIM_INFINITY: smtio_stacksize = min(smtio_stacksize, current_rlimit_stack[1]) if current_rlimit_stack[0] < smtio_stacksize: -- cgit v1.2.3 From e112d2fbf5a31f00ef19e6d05f28fecc1e9c56b9 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 6 Feb 2019 16:35:59 +0100 Subject: Add missing blackslash-to-slash convertion to smtio.py (matching Smt2Worker::get_id() behavior) Signed-off-by: Clifford Wolf --- backends/smt2/smtio.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backends/smt2/smtio.py') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 68783e744..ab20a4af2 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -784,7 +784,7 @@ class SmtIo: def get_path(self, mod, path): assert mod in self.modinfo - path = path.split(".") + path = path.replace("\\", "/").split(".") for i in range(len(path)-1): first = ".".join(path[0:i+1]) -- cgit v1.2.3 From c23bbc429103ca84cb8a9cfb674aacf7d14109c6 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 16 Jun 2019 23:12:03 +0200 Subject: Add timescale and generated-by header to yosys-smtbmc MkVcd Signed-off-by: Clifford Wolf --- backends/smt2/smtio.py | 2 ++ 1 file changed, 2 insertions(+) (limited to 'backends/smt2/smtio.py') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index ab20a4af2..cea0fc56c 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -1023,6 +1023,8 @@ class MkVcd: assert t >= self.t if t != self.t: if self.t == -1: + print("$version Generated by Yosys-SMTBMC $end", file=self.f) + print("$timescale 1ns $end", file=self.f) print("$var integer 32 t smt_step $end", file=self.f) print("$var event 1 ! smt_clock $end", file=self.f) -- cgit v1.2.3 From b3c36b444808be36a4fb35a3d78ba3f9691b3da0 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 26 Jun 2019 10:58:39 +0200 Subject: Escape scope names starting with dollar sign in smtio.py Signed-off-by: Clifford Wolf --- backends/smt2/smtio.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'backends/smt2/smtio.py') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index cea0fc56c..ae7968a1b 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -1043,7 +1043,10 @@ class MkVcd: scope = scope[:-1] while uipath[:-1] != scope: - print("$scope module %s $end" % uipath[len(scope)], file=self.f) + scopename = uipath[len(scope)] + if scopename.startswith("$"): + scopename = "\\" + scopename + print("$scope module %s $end" % scopename, file=self.f) scope.append(uipath[len(scope)]) if path in self.clocks and self.clocks[path][1] == "event": -- cgit v1.2.3 From ab4b9e8db481cd24b61cc0dc14bb5bf74d08006d Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Mon, 15 Jul 2019 23:33:18 +0800 Subject: smt: handle failure of setrlimit syscall --- backends/smt2/smtio.py | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'backends/smt2/smtio.py') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index ae7968a1b..bac68ac70 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -43,7 +43,11 @@ if os.name == "posix": if current_rlimit_stack[1] != resource.RLIM_INFINITY: smtio_stacksize = min(smtio_stacksize, current_rlimit_stack[1]) if current_rlimit_stack[0] < smtio_stacksize: - resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, current_rlimit_stack[1])) + try: + resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, current_rlimit_stack[1])) + except ValueError: + # couldn't get more stack, just run with what we have + pass # currently running solvers (so we can kill them) -- cgit v1.2.3