Cache invariants, color PASS/FAIL/[assumed], & syntax definitions

.gitignore

@@ -36,3 +36,10 @@ specs
 
 # These are library directories
 gnutls
+ivy/include/*.h
+include/
+ivy/bin/
+ivy/lib/
+ivy/z3/
+*.so
+bin/z3

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 (https://py-filelock.readthedocs.io/en/latest/index.html)
 
 symbolic link (linux) or directory junction (windows) from ~/.ipython/nbextensions/ivy to ivy2/ivy
 

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():
@@ -169,7 +170,17 @@ def get_checked_actions():
 def print_dots():
     print '...',
     sys.stdout.flush()
-
+
+class bcolors:
+    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):
@@ -186,14 +197,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 +235,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 +600,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 +725,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 +736,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
 
@@ -810,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__":

ivy/ivy_solver.py

@@ -23,6 +23,9 @@
 import logic as lg
 
 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
 
@@ -38,6 +41,26 @@ def set_seed(seed):
 opt_seed = iu.Parameter("seed",0,process=int)
 opt_seed.set_callback(set_seed)
 
+def set_database(db):
+    print 'Using {} as a database of proven invariants'.format(db)
+
+def check_db(db):
+    try:
+        lock = FileLock(db + ".lock")
+        with lock:
+            with open(db, 'r') as fr:
+                _ = fr.read()
+    except:
+        try:
+            with open(db, 'w') as fw:
+                pass
+        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,17 +1113,49 @@ def model_if_none(clauses1,implied,model):
             s.pop()
     return h
 
+def databaseContains(tag):
+    if opt_database.get() == None or tag == None:
+        return False
+    try:
+        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()) + "\": "
+            + str(e))
+    return False
+
+def addToDatabase(tag):
+    if opt_database.get() != None and tag != None and len(tag) > 0:
+        try:
+            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(e))
+    return
 
 def decide(s,atoms=None):
     # print "solving{"
-    # f = open("ivy.smt2","w")
-    # f.write(s.to_smt2())
-    # f.close()
+    tag = str(hash(s.to_smt2()))
+    if databaseContains(tag):
+        print "(found in {}) ".format(opt_database.get()),
+        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:
+        addToDatabase(tag)
     return res
 
 def get_small_model(clauses, sorts_to_minimize, relations_to_minimize, final_cond=None, shrink=True):

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

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

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