From b878d58e199fb8a2460a4f4039f212f359a7f853 Mon Sep 17 00:00:00 2001 From: max Date: Fri, 17 Jun 2022 12:39:57 -0700 Subject: [PATCH 1/9] Untested basic implementation of functionality in solver. --- ivy/ivy_solver.py | 48 ++++++++++++++++++++++++++++++++++++----------- 1 file changed, 37 insertions(+), 11 deletions(-) diff --git a/ivy/ivy_solver.py b/ivy/ivy_solver.py index 278e78b8..6ccf2d7f 100644 --- a/ivy/ivy_solver.py +++ b/ivy/ivy_solver.py @@ -1090,20 +1090,46 @@ def model_if_none(clauses1,implied,model): s.pop() return h +def databaseContains(database, tag): + if database == None or tag == None: + return False + try: + with open(database, 'r') as fr: + for line in fr: + if line.strip() == tag: + return True + except Exception as e: + raise iu.IvyError(None,"Encountered error looking for \"" + + str(tag) + "\" in database \"" + str(database) + "\": " + + str(e)) + return False -def decide(s,atoms=None): +def addToDatabase(database, tag): + if database != None and tag != None: + try: + with open(database, 'a') as fw: + fw.write(tag) + except Exception as e: + raise iu.IvyError(None, "Encountered error writing \"" + + str(tag) + "\" to database \"" + str(database) + "\": " + + str(e)) + return + +def decide(s,atoms=None,database=None): # print "solving{" - # f = open("ivy.smt2","w") - # f.write(s.to_smt2()) - # f.close() + tag = hash(s.to_smt2()) + if databaseContains(database, tag): + return z3.unsat res = s.check() if atoms == None else s.check(atoms) if res == z3.unknown: print s.to_smt2() raise iu.IvyError(None,"Solver produced inconclusive result") # print "}" + if res == z3.unsat and database != None: + addToDatabase(database, tag) return res -def get_small_model(clauses, sorts_to_minimize, relations_to_minimize, final_cond=None, shrink=True): +def get_small_model(clauses, sorts_to_minimize, relations_to_minimize, final_cond=None, shrink=True, database=None): """ Return a HerbrandModel with a "small" model of clauses. @@ -1144,7 +1170,7 @@ def get_small_model(clauses, sorts_to_minimize, relations_to_minimize, final_con # iu.dbg('the_fmla') s.add(the_fmla) - # res = decide(s) + # res = decide(s, database=database) # if res == z3.unsat: # return None @@ -1178,7 +1204,7 @@ def get_small_model(clauses, sorts_to_minimize, relations_to_minimize, final_con the_fmla = clauses_to_z3(foo) # iu.dbg('the_fmla') s.add(the_fmla) - res = decide(s) + res = decide(s, database=database) if res != z3.unsat: if fc.sat(): res = z3.unsat @@ -1190,9 +1216,9 @@ def get_small_model(clauses, sorts_to_minimize, relations_to_minimize, final_con s.pop() else: s.add(clauses_to_z3(final_cond)) - res = decide(s) + res = decide(s, database=database) else: - res = decide(s) + res = decide(s, database=database) if res == z3.unsat: return None @@ -1204,7 +1230,7 @@ def get_small_model(clauses, sorts_to_minimize, relations_to_minimize, final_con s.push() sc = size_constraint(x, n) s.add(formula_to_z3(sc)) - res = decide(s) + res = decide(s, database=database) if res == z3.sat: break else: @@ -1367,7 +1393,7 @@ def filter_redundant_facts(clauses,axioms): s2.add(c) keep = [] for fmla,alit in zip(neg_fmlas,alits): - if decide(s2,[alit]) == z3.sat: + if decide(s2,atoms=[alit],database=database) == z3.sat: keep.append(fmla) # print "unsat_core res = {}".format(res) return Clauses(pos_fmlas+keep,list(clauses.defs)) From 32734084790a256ba69f3f5cb88ef7ae60912b18 Mon Sep 17 00:00:00 2001 From: max Date: Fri, 17 Jun 2022 12:46:53 -0700 Subject: [PATCH 2/9] Untested basic implementation with a command-line option --- ivy/ivy_solver.py | 42 +++++++++++++++++++++++++++++------------- 1 file changed, 29 insertions(+), 13 deletions(-) diff --git a/ivy/ivy_solver.py b/ivy/ivy_solver.py index 6ccf2d7f..d80677a3 100644 --- a/ivy/ivy_solver.py +++ b/ivy/ivy_solver.py @@ -38,6 +38,22 @@ def set_seed(seed): opt_seed = iu.Parameter("seed",0,process=int) opt_seed.set_callback(set_seed) +database = None +def set_database(db): + print 'using {} as a database of proven invariants'.format(db) + database = db + +def check_db(db): + try: + with open(db, 'r') as fr: + _ = fr.read() + except: + return False + return True + +opt_database = iu.Parameter("database",None,check_db) +opt_database.set_callback(set_database) + def set_macro_finder(truth): z3.set_param('smt.macro_finder',truth) @@ -1090,7 +1106,7 @@ def model_if_none(clauses1,implied,model): s.pop() return h -def databaseContains(database, tag): +def databaseContains(tag): if database == None or tag == None: return False try: @@ -1104,7 +1120,7 @@ def databaseContains(database, tag): + str(e)) return False -def addToDatabase(database, tag): +def addToDatabase(tag): if database != None and tag != None: try: with open(database, 'a') as fw: @@ -1115,21 +1131,21 @@ def addToDatabase(database, tag): + str(e)) return -def decide(s,atoms=None,database=None): +def decide(s,atoms=None): # print "solving{" tag = hash(s.to_smt2()) - if databaseContains(database, tag): + if databaseContains(tag): return z3.unsat res = s.check() if atoms == None else s.check(atoms) if res == z3.unknown: print s.to_smt2() raise iu.IvyError(None,"Solver produced inconclusive result") # print "}" - if res == z3.unsat and database != None: - addToDatabase(database, tag) + if res == z3.unsat: + addToDatabase(tag) return res -def get_small_model(clauses, sorts_to_minimize, relations_to_minimize, final_cond=None, shrink=True, database=None): +def get_small_model(clauses, sorts_to_minimize, relations_to_minimize, final_cond=None, shrink=True): """ Return a HerbrandModel with a "small" model of clauses. @@ -1170,7 +1186,7 @@ def get_small_model(clauses, sorts_to_minimize, relations_to_minimize, final_con # iu.dbg('the_fmla') s.add(the_fmla) - # res = decide(s, database=database) + # res = decide(s) # if res == z3.unsat: # return None @@ -1204,7 +1220,7 @@ def get_small_model(clauses, sorts_to_minimize, relations_to_minimize, final_con the_fmla = clauses_to_z3(foo) # iu.dbg('the_fmla') s.add(the_fmla) - res = decide(s, database=database) + res = decide(s) if res != z3.unsat: if fc.sat(): res = z3.unsat @@ -1216,9 +1232,9 @@ def get_small_model(clauses, sorts_to_minimize, relations_to_minimize, final_con s.pop() else: s.add(clauses_to_z3(final_cond)) - res = decide(s, database=database) + res = decide(s) else: - res = decide(s, database=database) + res = decide(s) if res == z3.unsat: return None @@ -1230,7 +1246,7 @@ def get_small_model(clauses, sorts_to_minimize, relations_to_minimize, final_con s.push() sc = size_constraint(x, n) s.add(formula_to_z3(sc)) - res = decide(s, database=database) + res = decide(s) if res == z3.sat: break else: @@ -1393,7 +1409,7 @@ def filter_redundant_facts(clauses,axioms): s2.add(c) keep = [] for fmla,alit in zip(neg_fmlas,alits): - if decide(s2,atoms=[alit],database=database) == z3.sat: + if decide(s2,[alit]) == z3.sat: keep.append(fmla) # print "unsat_core res = {}".format(res) return Clauses(pos_fmlas+keep,list(clauses.defs)) From 6ca5c1e9aa526cf062ba2fb372d93c6912ea5399 Mon Sep 17 00:00:00 2001 From: max Date: Fri, 17 Jun 2022 12:50:29 -0700 Subject: [PATCH 3/9] Untested print statement indicating database hit. --- ivy/ivy_solver.py | 1 + 1 file changed, 1 insertion(+) diff --git a/ivy/ivy_solver.py b/ivy/ivy_solver.py index d80677a3..6df0fd66 100644 --- a/ivy/ivy_solver.py +++ b/ivy/ivy_solver.py @@ -1135,6 +1135,7 @@ def decide(s,atoms=None): # print "solving{" tag = hash(s.to_smt2()) if databaseContains(tag): + print "Found s in database {}".format(database) return z3.unsat res = s.check() if atoms == None else s.check(atoms) if res == z3.unknown: From 0f8dbec6756bcb8e2942946eefe26bfac42250f1 Mon Sep 17 00:00:00 2001 From: max Date: Fri, 17 Jun 2022 12:55:54 -0700 Subject: [PATCH 4/9] Untested colorizing of pass and fail --- ivy/ivy_check.py | 24 +++++++++++++++++------- 1 file changed, 17 insertions(+), 7 deletions(-) diff --git a/ivy/ivy_check.py b/ivy/ivy_check.py index 087bab5b..4eb091ea 100644 --- a/ivy/ivy_check.py +++ b/ivy/ivy_check.py @@ -169,7 +169,17 @@ def get_checked_actions(): def print_dots(): print '...', sys.stdout.flush() - + +class bcolors: + HEADER = '\033[95m' + OKBLUE = '\033[94m' + OKCYAN = '\033[96m' + OKGREEN = '\033[92m' + WARNING = '\033[93m' + FAIL = '\033[91m' + ENDC = '\033[0m' + BOLD = '\033[1m' + UNDERLINE = '\033[4m' class Checker(object): def __init__(self,conj,report_pass=True,invert=True): @@ -186,14 +196,14 @@ def start(self): if self.report_pass: print_dots() def sat(self): - print('FAIL') + print(bcolors.FAIL + 'FAIL' + bcolors.ENDC) global failures failures += 1 self.failed = True return not (diagnose.get() or opt_trace.get()) # ignore failures if not diagnosing def unsat(self): if self.report_pass: - print('PASS') + print(bcolors.OKGREEN + 'PASS' + bcolors.ENDC) def assume(self): return False def get_annot(self): @@ -224,7 +234,7 @@ def __init__(self,lf): self.lf = lf Checker.__init__(self,lf.formula,invert=False) def start(self): - print pretty_lf(self.lf) + " [assumed]" + print pretty_lf(self.lf) + bcolors.OKBLUE + " [assumed]" + bcolors.ENDC def assume(self): return True @@ -589,7 +599,7 @@ def check_isolate(): some_failed = True break if not some_failed: - print 'PASS' + print bcolors.OKGREEN + 'PASS' + bcolors.ENDC act.checked_assert.value = old_checked_assert else: print "" @@ -714,7 +724,7 @@ def mc_isolate(isolate,meth=ivy_mc.check_isolate): res = meth() if res is not None: print res - print 'FAIL' + print bcolors.FAIL + 'FAIL' + bcolors.ENDC exit(1) return for lineno in all_assert_linenos(): @@ -725,7 +735,7 @@ def mc_isolate(isolate,meth=ivy_mc.check_isolate): res = meth() if res is not None: print res - print 'FAIL' + print bcolors.FAIL + 'FAIL' + bcolors.ENDC exit(1) act.checked_assert.value = old_checked_assert From 29bbd5822d3064447815cba34198bf7b3600bc14 Mon Sep 17 00:00:00 2001 From: max Date: Fri, 17 Jun 2022 13:39:00 -0700 Subject: [PATCH 5/9] Tested and the color of PASS and [assumed] seems good, not yet sure about FAIL, and have not yet fully tested saving of invariants --- .gitignore | 7 +++++++ setup.py | 13 ++++++++++++- 2 files changed, 19 insertions(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index 9ccf383c..730ddbb8 100644 --- a/.gitignore +++ b/.gitignore @@ -36,3 +36,10 @@ specs # These are library directories gnutls +ivy/include/*.h +include/ +ivy/bin/ +ivy/lib/ +ivy/z3/ +*.so +bin/z3 diff --git a/setup.py b/setup.py index 7da79fcc..04856ca0 100644 --- a/setup.py +++ b/setup.py @@ -15,6 +15,7 @@ long_description = None setup(name='ms_ivy', + python_requires='<3', version='1.8.23', description='IVy verification tool', long_description=long_description, @@ -35,7 +36,17 @@ 'pydot', ] + (['applescript'] if platform.system() == 'Darwin' else []), entry_points = { - 'console_scripts': ['ivy=ivy.ivy:main','ivy_check=ivy.ivy_check:main','ivy_to_cpp=ivy.ivy_to_cpp:main','ivy_show=ivy.ivy_show:main','ivy_ev_viewer=ivy.ivy_ev_viewer:main','ivyc=ivy.ivy_to_cpp:ivyc','ivy_to_md=ivy.ivy_to_md:main','ivy_libs=ivy.ivy_libs:main','ivy_shell=ivy.ivy_shell:main','ivy_launch=ivy.ivy_launch:main'], + 'console_scripts': [ + 'ivy=ivy.ivy:main', + 'ivy_check=ivy.ivy_check:main', + 'ivy_to_cpp=ivy.ivy_to_cpp:main', + 'ivy_show=ivy.ivy_show:main', + 'ivy_ev_viewer=ivy.ivy_ev_viewer:main', + 'ivyc=ivy.ivy_to_cpp:ivyc', + 'ivy_to_md=ivy.ivy_to_md:main', + 'ivy_libs=ivy.ivy_libs:main', + 'ivy_shell=ivy.ivy_shell:main', + 'ivy_launch=ivy.ivy_launch:main'], }, zip_safe=False) From fd39e676d185efc3dee4fa477e57f6ede6c699f8 Mon Sep 17 00:00:00 2001 From: max Date: Fri, 17 Jun 2022 15:45:23 -0700 Subject: [PATCH 6/9] Got read/writing from/to DB working with nice print statements. Seems to work correctly when I test it with my own model. --- ivy/ivy_solver.py | 28 +++++++++++++++------------- 1 file changed, 15 insertions(+), 13 deletions(-) diff --git a/ivy/ivy_solver.py b/ivy/ivy_solver.py index 6df0fd66..745df99b 100644 --- a/ivy/ivy_solver.py +++ b/ivy/ivy_solver.py @@ -38,17 +38,19 @@ def set_seed(seed): opt_seed = iu.Parameter("seed",0,process=int) opt_seed.set_callback(set_seed) -database = None def set_database(db): - print 'using {} as a database of proven invariants'.format(db) - database = db + print 'Using {} as a database of proven invariants'.format(db) def check_db(db): try: with open(db, 'r') as fr: _ = fr.read() except: - return False + try: + with open(db, 'w') as fw: + pass + except: + return False return True opt_database = iu.Parameter("database",None,check_db) @@ -1107,35 +1109,35 @@ def model_if_none(clauses1,implied,model): return h def databaseContains(tag): - if database == None or tag == None: + if opt_database.get() == None or tag == None: return False try: - with open(database, 'r') as fr: + with open(opt_database.get(), 'r') as fr: for line in fr: if line.strip() == tag: return True except Exception as e: raise iu.IvyError(None,"Encountered error looking for \"" - + str(tag) + "\" in database \"" + str(database) + "\": " + + str(tag) + "\" in database \"" + str(opt_database.get()) + "\": " + str(e)) return False def addToDatabase(tag): - if database != None and tag != None: + if opt_database.get() != None and tag != None and len(tag) > 0: try: - with open(database, 'a') as fw: - fw.write(tag) + with open(opt_database.get(), 'a') as fw: + fw.write(tag + "\n") except Exception as e: raise iu.IvyError(None, "Encountered error writing \"" - + str(tag) + "\" to database \"" + str(database) + "\": " + + str(tag) + "\" to database \"" + str(opt_database.get()) + "\": " + str(e)) return def decide(s,atoms=None): # print "solving{" - tag = hash(s.to_smt2()) + tag = str(hash(s.to_smt2())) if databaseContains(tag): - print "Found s in database {}".format(database) + print "(found in {}) ".format(opt_database.get()), return z3.unsat res = s.check() if atoms == None else s.check(atoms) if res == z3.unknown: From 8258c28377440b71136f040f912a606d4e219f05 Mon Sep 17 00:00:00 2001 From: max Date: Wed, 22 Jun 2022 13:45:50 -0700 Subject: [PATCH 7/9] Added syntax highlighting --- lib/sublime-text/ivy.sublime-syntax | 87 +++++++++++++++++++++++++++++ lib/vim/install_vim.sh | 7 +++ lib/vim/ivy.vim | 65 +++++++++++++++++++++ 3 files changed, 159 insertions(+) create mode 100644 lib/sublime-text/ivy.sublime-syntax create mode 100644 lib/vim/install_vim.sh create mode 100644 lib/vim/ivy.vim diff --git a/lib/sublime-text/ivy.sublime-syntax b/lib/sublime-text/ivy.sublime-syntax new file mode 100644 index 00000000..b10bde63 --- /dev/null +++ b/lib/sublime-text/ivy.sublime-syntax @@ -0,0 +1,87 @@ +%YAML 1.2 +--- +# See http://www.sublimetext.com/docs/syntax.html +file_extensions: + - ivy +scope: source.example-c +contexts: + main: + # Strings begin and end with quotes, and use backslashes as an escape + # character + - match: '"' + scope: punctuation.definition.string.begin.example-c + push: double_quoted_string + + # Comments begin with a '#' and finish at the end of the line + - match: '#' + scope: punctuation.definition.comment.example-c + push: line_comment + + # Keywords are if, else for and while. + # Note that blackslashes don't need to be escaped within single quoted + # strings in YAML. When using single quoted strings, only single quotes + # need to be escaped: this is done by using two single quotes next to each + # other. + - match: '\b(if|else|for|while)\b' + scope: keyword.control.example-c + + # Numbers + - match: '\b(-)?[0-9.]+\b' + scope: constant.numeric.example-c + + # Imports + - match: '\b(include|export|instance)\b' + scope: keyword.control.import.example-c + + # Definitions + - match: '\b(module)\b' + scope: entity.name.class.example-c + + # Definitions + - match: '\b(after|before)\b' + scope: entity.name.trait.example-c + + # Functions + - match: '\b(action)\b' + scope: entity.name.function.example-c + + # Meta Types + - match: '\b(var|parameter|type)\b' + scope: storage.type.class.example-c + + # Actual Types + - match: '\b(nat|bool|int|array|map|bool_vec|vec|relation)\b' + scope: storage.type.example-c + + # with blablabla + - match: '\b(with)\b' + scope: entity.other.inherited-class.example-c + + # spec, impl, etc. + - match: '\b(specification|implementation|definition|implement|invariant|require|assert|assume)\b' + scope: entity.other.attribute-name.example-c + + # Arithmetic operators + - match: \+|\-|\*|\*\*|/|//|%|<<|>>|&|\||\^|~ + scope: keyword.operator.arithmetic.example-c + + # Comparison Operators + - match: <\=|>\=|\=\=|<|>|~\= + scope: keyword.operator.comparison.example-c + + # Assignment + - match: :=|= + scope: keyword.operator.assignment.example-c + + double_quoted_string: + - meta_scope: string.quoted.double.example-c + - match: '\\.' + scope: constant.character.escape.example-c + - match: '"' + scope: punctuation.definition.string.end.example-c + pop: true + + line_comment: + - meta_scope: comment.line.example-c + - match: $ + pop: true \ No newline at end of file diff --git a/lib/vim/install_vim.sh b/lib/vim/install_vim.sh new file mode 100644 index 00000000..f03af0d3 --- /dev/null +++ b/lib/vim/install_vim.sh @@ -0,0 +1,7 @@ +#!/bin/sh + +mkdir -R ~/.vim/syntax +cp ivy.vim ~/.vim/syntax + +mkdir -R ~/.vim/ftdetect +echo "au BufRead,BufNewFile *.ivy set filetype=ivy" >> ~/.vim/ftdetect diff --git a/lib/vim/ivy.vim b/lib/vim/ivy.vim new file mode 100644 index 00000000..32060877 --- /dev/null +++ b/lib/vim/ivy.vim @@ -0,0 +1,65 @@ +" Vim syntax file +" Language: Ivy Model Checker +" Maintainer: Josh Jeppson +" Latest Revision: 9 November 2021 + +if exists("b:current_syntax") + finish +endif + +" Keywords + +syn keyword ivyLang import with include export mixin using attribute + +syn keyword ivyControlFlow if else for forall while decreases +syn keyword ivyControlFlow of instantiate derived +syn keyword ivyControlFlow link call after init execute +syn keyword ivyControlFlow before after around returns +syn keyword ivyControlFlow update params ensures requires modifies +syn keyword ivyControlFlow rely mixord extract some maximizing +syn keyword ivyControlFlow apply global named + +syn keyword ivyObjects this instance fresh local entry macro progress autoinstance +syn keyword ivyObjects temporal tactic subclass field template process + +syn keyword ivyBlocks module function individual action relation object specification +syn keyword ivyBlocks class object method destructor private public ghost implement implementation + +syn keyword ivyCheck property parameter alias trusted proof require +syn keyword ivyChecks invariant variant ensure assume relation axiom +syn keyword ivyChecks monitor exists axiom definition isolate delegate +syn keyword ivyChecks conjecture schema concept assert from theorem + +syn keyword ivyTypes type nat bool int interpret state set null bv + +syn keyword ivyConstants true false + +" Integers (with +/- at the front) +syn match ivyNumber '[\n \t]\d\+' +syn match ivyNumber '[+-]\d\+' + +" Floating points (including scientific notation) +syn match ivyNumber '[+-]\d\+\.\d*' +" TODO: Add support for scientific notation + +" Strings +syn region ivyString start='"' end='"' + +" Comments +syn match ivyComment "#.*$" + +" Blocks +syn region ivyBlock start="{" end="}" fold transparent + +" Putting it together: +let b:current_syntax = "ivy" + +hi def link ivyComment Comment +hi def link ivyControlFlow Statement +hi def link ivyBlocks Statement +hi def link ivyChecks Statement +hi def link ivyObjects Type +hi def link ivyTypes Type +hi def link ivyNumber Constant +hi def link ivyString Constant +hi def link ivyLang PreProc From 23790cc1e974d9069af4e52fe888edb07d2d456f Mon Sep 17 00:00:00 2001 From: max Date: Thu, 23 Jun 2022 14:07:28 -0700 Subject: [PATCH 8/9] Added file locking per Ken's suggestion, untested. --- INSTALL | 1 + ivy/ivy_check.py | 39 ++++++++++++++++++++------------------- ivy/ivy_solver.py | 26 +++++++++++++++++--------- 3 files changed, 38 insertions(+), 28 deletions(-) diff --git a/INSTALL b/INSTALL index 64f8a643..314a0094 100644 --- a/INSTALL +++ b/INSTALL @@ -5,6 +5,7 @@ IPython 3.2 ply (python lex yacc) Z3 python interface (import z3 should work) pygraphviz 1.3.1 (which requires graphviz) +filelock (available via pypy) symbolic link (linux) or directory junction (windows) from ~/.ipython/nbextensions/ivy to ivy2/ivy diff --git a/ivy/ivy_check.py b/ivy/ivy_check.py index 4eb091ea..e707dc1e 100644 --- a/ivy/ivy_check.py +++ b/ivy/ivy_check.py @@ -31,13 +31,14 @@ import sys from collections import defaultdict -diagnose = iu.BooleanParameter("diagnose",False) -coverage = iu.BooleanParameter("coverage",True) -checked_action = iu.Parameter("action","") -opt_trusted = iu.BooleanParameter("trusted",False) -opt_mc = iu.BooleanParameter("mc",False) -opt_trace = iu.BooleanParameter("trace",False) -opt_separate = iu.BooleanParameter("separate",None) +diagnose = iu.BooleanParameter("diagnose",False) +coverage = iu.BooleanParameter("coverage",True ) +checked_action = iu.Parameter ("action" ,"" ) +opt_trusted = iu.BooleanParameter("trusted" ,False) +opt_mc = iu.BooleanParameter("mc" ,False) +opt_trace = iu.BooleanParameter("trace" ,False) +opt_separate = iu.BooleanParameter("separate",None ) +opt_colors = iu.BooleanParameter("colors" ,True ) def display_cex(msg,ag): if diagnose.get(): @@ -171,15 +172,15 @@ def print_dots(): sys.stdout.flush() class bcolors: - HEADER = '\033[95m' - OKBLUE = '\033[94m' - OKCYAN = '\033[96m' - OKGREEN = '\033[92m' - WARNING = '\033[93m' - FAIL = '\033[91m' - ENDC = '\033[0m' - BOLD = '\033[1m' - UNDERLINE = '\033[4m' + HEADER = '\033[95m' if opt_colors.get() else '' + OKBLUE = '\033[94m' if opt_colors.get() else '' + OKCYAN = '\033[96m' if opt_colors.get() else '' + OKGREEN = '\033[92m' if opt_colors.get() else '' + WARNING = '\033[93m' if opt_colors.get() else '' + FAIL = '\033[91m' if opt_colors.get() else '' + ENDC = '\033[0m' if opt_colors.get() else '' + BOLD = '\033[1m' if opt_colors.get() else '' + UNDERLINE = '\033[4m' if opt_colors.get() else '' class Checker(object): def __init__(self,conj,report_pass=True,invert=True): @@ -820,13 +821,13 @@ def main(): with utl.ErrorPrinter(): ivy_init.source_file(sys.argv[1],ivy_init.open_read(sys.argv[1]),create_isolate=False) if isinstance(act.checked_assert.get(),iu.LocationTuple) and act.checked_assert.get().filename == 'none.ivy' and act.checked_assert.get().line == 0: - print 'NOT CHECKED' + print bcolors.WARNING + 'NOT CHECKED' + bcolors.ENDC exit(0); check_module() if some_bounded: - print "BOUNDED" + print bcolors.WARNING + "BOUNDED" + bcolors.ENDC else: - print "OK" + print bcolors.OKGREEN + "OK" + bcolors.ENDC if __name__ == "__main__": diff --git a/ivy/ivy_solver.py b/ivy/ivy_solver.py index 745df99b..abe5d98b 100644 --- a/ivy/ivy_solver.py +++ b/ivy/ivy_solver.py @@ -23,6 +23,7 @@ import logic as lg import sys +from filelock import FileLock # Following accounts for Z3 API symbols that are hidden as of Z3-4.5.0 @@ -43,8 +44,10 @@ def set_database(db): def check_db(db): try: - with open(db, 'r') as fr: - _ = fr.read() + lock = FileLock(db + ".lock") + with lock: + with open(db, 'r') as fr: + _ = fr.read() except: try: with open(db, 'w') as fw: @@ -1112,10 +1115,12 @@ def databaseContains(tag): if opt_database.get() == None or tag == None: return False try: - with open(opt_database.get(), 'r') as fr: - for line in fr: - if line.strip() == tag: - return True + lock = FileLock(opt_database.get() + ".lock") + with lock: + with open(opt_database.get(), 'r') as fr: + for line in fr: + if line.strip() == tag: + return True except Exception as e: raise iu.IvyError(None,"Encountered error looking for \"" + str(tag) + "\" in database \"" + str(opt_database.get()) + "\": " @@ -1125,11 +1130,14 @@ def databaseContains(tag): def addToDatabase(tag): if opt_database.get() != None and tag != None and len(tag) > 0: try: - with open(opt_database.get(), 'a') as fw: - fw.write(tag + "\n") + lock = FileLock(opt_database.get() + ".lock") + with lock: + with open(opt_database.get(), 'a') as fw: + fw.write(tag + "\n") except Exception as e: raise iu.IvyError(None, "Encountered error writing \"" - + str(tag) + "\" to database \"" + str(opt_database.get()) + "\": " + + str(tag) + + "\" to database \"" + str(opt_database.get()) + "\": " + str(e)) return From 48eb1bf1d67fe9b71d17c544e3dbc321134eec9b Mon Sep 17 00:00:00 2001 From: max Date: Thu, 23 Jun 2022 15:43:58 -0700 Subject: [PATCH 9/9] Tested locking, seems to work, also got rid of annoying log statement --- INSTALL | 2 +- ivy/ivy_solver.py | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/INSTALL b/INSTALL index 314a0094..df37ee52 100644 --- a/INSTALL +++ b/INSTALL @@ -5,7 +5,7 @@ IPython 3.2 ply (python lex yacc) Z3 python interface (import z3 should work) pygraphviz 1.3.1 (which requires graphviz) -filelock (available via pypy) +filelock (https://py-filelock.readthedocs.io/en/latest/index.html) symbolic link (linux) or directory junction (windows) from ~/.ipython/nbextensions/ivy to ivy2/ivy diff --git a/ivy/ivy_solver.py b/ivy/ivy_solver.py index abe5d98b..7c927144 100644 --- a/ivy/ivy_solver.py +++ b/ivy/ivy_solver.py @@ -24,6 +24,8 @@ import sys from filelock import FileLock +import logging +logging.getLogger("filelock").setLevel(logging.INFO) # Following accounts for Z3 API symbols that are hidden as of Z3-4.5.0