From 5186ca79710fe935d1f7ed27c4a34e913ab547e8 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 12 Dec 2013 18:24:54 -0500 Subject: [PATCH] First attempt at incorporating LFSC proof checker into CVC4. --- .travis.yml | 36 +- COPYING | 21 + Makefile.am | 16 +- Makefile.builds.in | 4 +- NEWS | 1 + configure.ac | 6 +- proofs/lfsc_checker/.gitignore | 16 + proofs/lfsc_checker/AUTHORS | 5 + proofs/lfsc_checker/COPYING | 17 + proofs/lfsc_checker/INSTALL | 370 +++++ proofs/lfsc_checker/Makefile.am | 30 + proofs/lfsc_checker/NEWS | 9 + proofs/lfsc_checker/README | 83 + proofs/lfsc_checker/check.cpp | 1383 +++++++++++++++++ proofs/lfsc_checker/check.h | 167 ++ .../lfsc_checker/chunking_memory_management.h | 157 ++ proofs/lfsc_checker/code.cpp | 1377 ++++++++++++++++ proofs/lfsc_checker/code.h | 15 + proofs/lfsc_checker/configure.ac | 47 + proofs/lfsc_checker/expr.cpp | 966 ++++++++++++ proofs/lfsc_checker/expr.h | 367 +++++ proofs/lfsc_checker/libwriter.cpp | 238 +++ proofs/lfsc_checker/libwriter.h | 28 + proofs/lfsc_checker/main.cpp | 139 ++ proofs/lfsc_checker/position.h | 30 + proofs/lfsc_checker/print_smt2.cpp | 122 ++ proofs/lfsc_checker/print_smt2.h | 17 + proofs/lfsc_checker/scccode.cpp | 609 ++++++++ proofs/lfsc_checker/scccode.h | 27 + proofs/lfsc_checker/sccwriter.cpp | 977 ++++++++++++ proofs/lfsc_checker/sccwriter.h | 86 + proofs/lfsc_checker/trie.cpp | 24 + proofs/lfsc_checker/trie.h | 129 ++ src/Makefile.am | 7 +- src/smt/options | 2 + src/smt/smt_engine.cpp | 12 + src/smt/smt_engine.h | 5 + src/smt/smt_engine_check_proof.cpp | 36 + 38 files changed, 7562 insertions(+), 19 deletions(-) create mode 100644 proofs/lfsc_checker/.gitignore create mode 100644 proofs/lfsc_checker/AUTHORS create mode 100644 proofs/lfsc_checker/COPYING create mode 100644 proofs/lfsc_checker/INSTALL create mode 100644 proofs/lfsc_checker/Makefile.am create mode 100644 proofs/lfsc_checker/NEWS create mode 100644 proofs/lfsc_checker/README create mode 100644 proofs/lfsc_checker/check.cpp create mode 100644 proofs/lfsc_checker/check.h create mode 100644 proofs/lfsc_checker/chunking_memory_management.h create mode 100644 proofs/lfsc_checker/code.cpp create mode 100644 proofs/lfsc_checker/code.h create mode 100644 proofs/lfsc_checker/configure.ac create mode 100644 proofs/lfsc_checker/expr.cpp create mode 100644 proofs/lfsc_checker/expr.h create mode 100644 proofs/lfsc_checker/libwriter.cpp create mode 100644 proofs/lfsc_checker/libwriter.h create mode 100644 proofs/lfsc_checker/main.cpp create mode 100644 proofs/lfsc_checker/position.h create mode 100644 proofs/lfsc_checker/print_smt2.cpp create mode 100644 proofs/lfsc_checker/print_smt2.h create mode 100644 proofs/lfsc_checker/scccode.cpp create mode 100644 proofs/lfsc_checker/scccode.h create mode 100644 proofs/lfsc_checker/sccwriter.cpp create mode 100644 proofs/lfsc_checker/sccwriter.h create mode 100644 proofs/lfsc_checker/trie.cpp create mode 100644 proofs/lfsc_checker/trie.h create mode 100644 src/smt/smt_engine_check_proof.cpp diff --git a/.travis.yml b/.travis.yml index 8acc8a546..b8d958ed5 100644 --- a/.travis.yml +++ b/.travis.yml @@ -3,9 +3,11 @@ compiler: - gcc - clang env: - - TRAVIS_CVC4_CONFIG='production --enable-language-bindings=java,c' - - TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c' - - TRAVIS_CVC4_DISTCHECK=yes + - TRAVIS_CVC4=yes TRAVIS_CVC4_CONFIG='production --enable-language-bindings=java,c' + - TRAVIS_CVC4=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c' + - TRAVIS_CVC4=yes TRAVIS_CVC4_DISTCHECK=yes + - TRAVIS_LFSC=yes + - TRAVIS_LFSC=yes TRAVIS_LFSC_DISTCHECK=yes before_install: # dhart/ppa is for cxxtest package, which doesn't appear officially until quantal - travis_retry sudo apt-add-repository -y ppa:dhart/ppa @@ -16,17 +18,29 @@ before_script: - export PATH=$PATH:$JAVA_HOME/bin - export JAVA_CPPFLAGS=-I$JAVA_HOME/include - ./autogen.sh - - echo $TRAVIS_CVC4_CONFIG - - normal="$(echo -e '\033[0m')" red="$normal$(echo -e '\033[01;31m')" green="$normal$(echo -e '\033[01;32m')" - - ./configure --enable-unit-testing --enable-proof --with-portfolio $TRAVIS_CVC4_CONFIG || (echo; cat builds/config.log; echo; echo "${red}CONFIGURE FAILED${normal}"; exit 1) script: - normal="$(echo -e '\033[0m')" red="$normal$(echo -e '\033[01;31m')" green="$normal$(echo -e '\033[01;32m')" - - if [ -n "$TRAVIS_CVC4_DISTCHECK" ]; then - make -j2 distcheck CVC4_REGRESSION_ARGS='--no-early-exit' || (echo; echo "${red}DISTCHECK FAILED${normal}"; echo; exit 1); + - if [ -n "$TRAVIS_CVC4" ]; then + echo "CVC4 config - $TRAVIS_CVC4_CONFIG" && + (./configure --enable-unit-testing --enable-proof --with-portfolio $TRAVIS_CVC4_CONFIG || (echo; cat builds/config.log; echo; echo "${red}CONFIGURE FAILED${normal}"; exit 1)) && + if [ -n "$TRAVIS_CVC4_DISTCHECK" ]; then + make -j2 distcheck CVC4_REGRESSION_ARGS='--no-early-exit' || (echo; echo "${red}DISTCHECK FAILED${normal}"; echo; exit 1); + else + (make -j2 check CVC4_REGRESSION_ARGS='--no-early-exit' || (echo; echo "${red}BUILD/TEST FAILED${normal}"; echo; exit 1)) && + (make check BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-early-exit' || (echo; echo "${red}PORTFOLIO TEST FAILED${normal}"; echo; exit 1)) && + (make -j2 examples || (echo; echo "${red}COULD NOT BUILD EXAMPLES${normal}"; echo; exit 1)); + fi; + elif [ -n "$TRAVIS_LFSC" ]; then + cd proofs/lfsc_checker && + (./configure || (echo; cat builds/config.log; echo; echo "${red}CONFIGURE FAILED${normal}"; exit 1)) && + if [ -n "$TRAVIS_LFSC_DISTCHECK" ]; then + make -j2 distcheck || (echo; echo "${red}LFSC DISTCHECK FAILED${normal}"; echo; exit 1); + else + make -j2 || (echo; echo "${red}LFSC BUILD FAILED${normal}"; echo; exit 1); + fi; else - (make -j2 check CVC4_REGRESSION_ARGS='--no-early-exit' || (echo; echo "${red}BUILD/TEST FAILED${normal}"; echo; exit 1)) && - (make check BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-early-exit' || (echo; echo "${red}PORTFOLIO TEST FAILED${normal}"; echo; exit 1)) && - (make -j2 examples || (echo; echo "${red}COULD NOT BUILD EXAMPLES${normal}"; echo; exit 1)); + echo "${red}Unknown Travis-CI configuration${normal}"; + exit 1; fi && (echo; echo "${green}EVERYTHING SEEMED TO PASS!${normal}") matrix: diff --git a/COPYING b/COPYING index 40cbdaa6b..dd6a1582a 100644 --- a/COPYING +++ b/COPYING @@ -257,3 +257,24 @@ you build a version of CVC4 that does not use GLPK, configure CVC4 with "--without-glpk" before building (though that is the default). It can then be used in contexts where you want to license CVC4 under the (modified) BSD license. + +CVC4 sources incorporate those of the LFSC proof checker, which is +covered by the following license: + + LFSC is copyright (C) 2012, 2013 The University of Iowa. All rights + reserved. + + LFSC is open-source; distribution is under the terms of the modified + BSD license. + + THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS + AS IS AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT + OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, + SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT + LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, + DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Makefile.am b/Makefile.am index 41586cbe7..40f4c7006 100644 --- a/Makefile.am +++ b/Makefile.am @@ -5,8 +5,13 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas AUTOMAKE_OPTIONS = foreign ACLOCAL_AMFLAGS = -I config -SUBDIRS = src test contrib -DIST_SUBDIRS = $(SUBDIRS) examples +SUBDIRS_BASE = src test contrib +if CVC4_PROOF + SUBDIRS = proofs/lfsc_checker $(SUBDIRS_BASE) +else + SUBDIRS = $(SUBDIRS_BASE) +endif +DIST_SUBDIRS = proofs/lfsc_checker $(SUBDIRS_BASE) examples .PHONY: examples examples: all @@ -125,7 +130,12 @@ EXTRA_DIST = \ doc/SmtEngine.3cvc_template.in \ doc/options.3cvc_template.in \ doc/libcvc4parser.3.in \ - doc/libcvc4compat.3.in + doc/libcvc4compat.3.in \ + proofs/signatures/example.plf \ + proofs/signatures/sat.plf \ + proofs/signatures/smt.plf \ + proofs/signatures/th_base.plf + man_MANS = \ doc/cvc4.1 \ doc/pcvc4.1 \ diff --git a/Makefile.builds.in b/Makefile.builds.in index 33df24f95..296e5a974 100644 --- a/Makefile.builds.in +++ b/Makefile.builds.in @@ -192,12 +192,12 @@ endif # The descent into "src" with target "check" is to build check # prerequisites (e.g. CHECK_PROGRAMS, CHECK_LTLIBRARIES, ...). -check test units: +check test units: all (cd $(CURRENT_BUILD)/src && $(MAKE) check) +(cd $(CURRENT_BUILD)/test && $(MAKE) $@) systemtests regress: all +(cd $(CURRENT_BUILD)/test && $(MAKE) $@) -units%: +units%: all (cd $(CURRENT_BUILD)/src && $(MAKE) check) +(cd $(CURRENT_BUILD)/test && $(MAKE) units TEST_PREFIX=$(subst units:,,$@)) regress%: all diff --git a/NEWS b/NEWS index 46f5deee2..9f17bfaa4 100644 --- a/NEWS +++ b/NEWS @@ -4,6 +4,7 @@ Changes since 1.3 ================= * Timed statistics are now properly updated even on process abort. +* The LFSC proof checker has been incorporated into CVC4 sources. Changes since 1.2 ================= diff --git a/configure.ac b/configure.ac index 89d59cfff..1cd7a4696 100644 --- a/configure.ac +++ b/configure.ac @@ -10,12 +10,13 @@ m4_define(_CVC4_RELEASE_STRING, _CVC4_MAJOR[.]_CVC4_MINOR[]m4_if(_CVC4_RELEASE,[ dnl Preprocess CL args. Defined in config/cvc4.m4 CVC4_AC_INIT -AC_PREREQ(2.61) -AC_INIT([cvc4], _CVC4_RELEASE_STRING) +AC_PREREQ([2.68]) +AC_INIT([cvc4], _CVC4_RELEASE_STRING, [cvc-bugs@cs.nyu.edu]) AC_CONFIG_SRCDIR([src/include/cvc4_public.h]) AC_CONFIG_AUX_DIR([config]) AC_CONFIG_MACRO_DIR([config]) AC_CONFIG_LIBOBJ_DIR([src/lib]) +AC_CONFIG_SUBDIRS([proofs/lfsc_checker]) m4_ifdef([AM_SILENT_RULES],[AM_SILENT_RULES([yes])]) @@ -515,6 +516,7 @@ AC_MSG_RESULT([$enable_proof]) if test "$enable_proof" = yes; then CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROOF" fi +AM_CONDITIONAL([CVC4_PROOF], [test "$enable_proof" = yes]) AC_MSG_CHECKING([whether to optimize libcvc4]) diff --git a/proofs/lfsc_checker/.gitignore b/proofs/lfsc_checker/.gitignore new file mode 100644 index 000000000..1f799d15a --- /dev/null +++ b/proofs/lfsc_checker/.gitignore @@ -0,0 +1,16 @@ +/autom4te.cache +/stamp-h +/config.h.in +/config.log +/config.status +/config.cache +/libtool +/stamp-h1 +.dep +Makefile.in +/configure +/aclocal.m4 +*~ +\#*\# +/config/ +*.swp diff --git a/proofs/lfsc_checker/AUTHORS b/proofs/lfsc_checker/AUTHORS new file mode 100644 index 000000000..0bd0a37b0 --- /dev/null +++ b/proofs/lfsc_checker/AUTHORS @@ -0,0 +1,5 @@ +The core authors and designers of the LFSC proof checker are: + + Andy Reynolds + Aaron Stump + diff --git a/proofs/lfsc_checker/COPYING b/proofs/lfsc_checker/COPYING new file mode 100644 index 000000000..b220a3147 --- /dev/null +++ b/proofs/lfsc_checker/COPYING @@ -0,0 +1,17 @@ +LFSC is copyright (C) 2012, 2013 The University of Iowa. +All rights reserved. + +LFSC is open-source; distribution is under the terms of the modified +BSD license. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS +AS IS AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/proofs/lfsc_checker/INSTALL b/proofs/lfsc_checker/INSTALL new file mode 100644 index 000000000..a1e89e18a --- /dev/null +++ b/proofs/lfsc_checker/INSTALL @@ -0,0 +1,370 @@ +Installation Instructions +************************* + +Copyright (C) 1994-1996, 1999-2002, 2004-2011 Free Software Foundation, +Inc. + + Copying and distribution of this file, with or without modification, +are permitted in any medium without royalty provided the copyright +notice and this notice are preserved. This file is offered as-is, +without warranty of any kind. + +Basic Installation +================== + + Briefly, the shell commands `./configure; make; make install' should +configure, build, and install this package. The following +more-detailed instructions are generic; see the `README' file for +instructions specific to this package. Some packages provide this +`INSTALL' file but do not implement all of the features documented +below. The lack of an optional feature in a given package is not +necessarily a bug. More recommendations for GNU packages can be found +in *note Makefile Conventions: (standards)Makefile Conventions. + + The `configure' shell script attempts to guess correct values for +various system-dependent variables used during compilation. It uses +those values to create a `Makefile' in each directory of the package. +It may also create one or more `.h' files containing system-dependent +definitions. Finally, it creates a shell script `config.status' that +you can run in the future to recreate the current configuration, and a +file `config.log' containing compiler output (useful mainly for +debugging `configure'). + + It can also use an optional file (typically called `config.cache' +and enabled with `--cache-file=config.cache' or simply `-C') that saves +the results of its tests to speed up reconfiguring. Caching is +disabled by default to prevent problems with accidental use of stale +cache files. + + If you need to do unusual things to compile the package, please try +to figure out how `configure' could check whether to do them, and mail +diffs or instructions to the address given in the `README' so they can +be considered for the next release. If you are using the cache, and at +some point `config.cache' contains results you don't want to keep, you +may remove or edit it. + + The file `configure.ac' (or `configure.in') is used to create +`configure' by a program called `autoconf'. You need `configure.ac' if +you want to change it or regenerate `configure' using a newer version +of `autoconf'. + + The simplest way to compile this package is: + + 1. `cd' to the directory containing the package's source code and type + `./configure' to configure the package for your system. + + Running `configure' might take a while. While running, it prints + some messages telling which features it is checking for. + + 2. Type `make' to compile the package. + + 3. Optionally, type `make check' to run any self-tests that come with + the package, generally using the just-built uninstalled binaries. + + 4. Type `make install' to install the programs and any data files and + documentation. When installing into a prefix owned by root, it is + recommended that the package be configured and built as a regular + user, and only the `make install' phase executed with root + privileges. + + 5. Optionally, type `make installcheck' to repeat any self-tests, but + this time using the binaries in their final installed location. + This target does not install anything. Running this target as a + regular user, particularly if the prior `make install' required + root privileges, verifies that the installation completed + correctly. + + 6. You can remove the program binaries and object files from the + source code directory by typing `make clean'. To also remove the + files that `configure' created (so you can compile the package for + a different kind of computer), type `make distclean'. There is + also a `make maintainer-clean' target, but that is intended mainly + for the package's developers. If you use it, you may have to get + all sorts of other programs in order to regenerate files that came + with the distribution. + + 7. Often, you can also type `make uninstall' to remove the installed + files again. In practice, not all packages have tested that + uninstallation works correctly, even though it is required by the + GNU Coding Standards. + + 8. Some packages, particularly those that use Automake, provide `make + distcheck', which can by used by developers to test that all other + targets like `make install' and `make uninstall' work correctly. + This target is generally not run by end users. + +Compilers and Options +===================== + + Some systems require unusual options for compilation or linking that +the `configure' script does not know about. Run `./configure --help' +for details on some of the pertinent environment variables. + + You can give `configure' initial values for configuration parameters +by setting variables in the command line or in the environment. Here +is an example: + + ./configure CC=c99 CFLAGS=-g LIBS=-lposix + + *Note Defining Variables::, for more details. + +Compiling For Multiple Architectures +==================================== + + You can compile the package for more than one kind of computer at the +same time, by placing the object files for each architecture in their +own directory. To do this, you can use GNU `make'. `cd' to the +directory where you want the object files and executables to go and run +the `configure' script. `configure' automatically checks for the +source code in the directory that `configure' is in and in `..'. This +is known as a "VPATH" build. + + With a non-GNU `make', it is safer to compile the package for one +architecture at a time in the source code directory. After you have +installed the package for one architecture, use `make distclean' before +reconfiguring for another architecture. + + On MacOS X 10.5 and later systems, you can create libraries and +executables that work on multiple system types--known as "fat" or +"universal" binaries--by specifying multiple `-arch' options to the +compiler but only a single `-arch' option to the preprocessor. Like +this: + + ./configure CC="gcc -arch i386 -arch x86_64 -arch ppc -arch ppc64" \ + CXX="g++ -arch i386 -arch x86_64 -arch ppc -arch ppc64" \ + CPP="gcc -E" CXXCPP="g++ -E" + + This is not guaranteed to produce working output in all cases, you +may have to build one architecture at a time and combine the results +using the `lipo' tool if you have problems. + +Installation Names +================== + + By default, `make install' installs the package's commands under +`/usr/local/bin', include files under `/usr/local/include', etc. You +can specify an installation prefix other than `/usr/local' by giving +`configure' the option `--prefix=PREFIX', where PREFIX must be an +absolute file name. + + You can specify separate installation prefixes for +architecture-specific files and architecture-independent files. If you +pass the option `--exec-prefix=PREFIX' to `configure', the package uses +PREFIX as the prefix for installing programs and libraries. +Documentation and other data files still use the regular prefix. + + In addition, if you use an unusual directory layout you can give +options like `--bindir=DIR' to specify different values for particular +kinds of files. Run `configure --help' for a list of the directories +you can set and what kinds of files go in them. In general, the +default for these options is expressed in terms of `${prefix}', so that +specifying just `--prefix' will affect all of the other directory +specifications that were not explicitly provided. + + The most portable way to affect installation locations is to pass the +correct locations to `configure'; however, many packages provide one or +both of the following shortcuts of passing variable assignments to the +`make install' command line to change installation locations without +having to reconfigure or recompile. + + The first method involves providing an override variable for each +affected directory. For example, `make install +prefix=/alternate/directory' will choose an alternate location for all +directory configuration variables that were expressed in terms of +`${prefix}'. Any directories that were specified during `configure', +but not in terms of `${prefix}', must each be overridden at install +time for the entire installation to be relocated. The approach of +makefile variable overrides for each directory variable is required by +the GNU Coding Standards, and ideally causes no recompilation. +However, some platforms have known limitations with the semantics of +shared libraries that end up requiring recompilation when using this +method, particularly noticeable in packages that use GNU Libtool. + + The second method involves providing the `DESTDIR' variable. For +example, `make install DESTDIR=/alternate/directory' will prepend +`/alternate/directory' before all installation names. The approach of +`DESTDIR' overrides is not required by the GNU Coding Standards, and +does not work on platforms that have drive letters. On the other hand, +it does better at avoiding recompilation issues, and works well even +when some directory options were not specified in terms of `${prefix}' +at `configure' time. + +Optional Features +================= + + If the package supports it, you can cause programs to be installed +with an extra prefix or suffix on their names by giving `configure' the +option `--program-prefix=PREFIX' or `--program-suffix=SUFFIX'. + + Some packages pay attention to `--enable-FEATURE' options to +`configure', where FEATURE indicates an optional part of the package. +They may also pay attention to `--with-PACKAGE' options, where PACKAGE +is something like `gnu-as' or `x' (for the X Window System). The +`README' should mention any `--enable-' and `--with-' options that the +package recognizes. + + For packages that use the X Window System, `configure' can usually +find the X include and library files automatically, but if it doesn't, +you can use the `configure' options `--x-includes=DIR' and +`--x-libraries=DIR' to specify their locations. + + Some packages offer the ability to configure how verbose the +execution of `make' will be. For these packages, running `./configure +--enable-silent-rules' sets the default to minimal output, which can be +overridden with `make V=1'; while running `./configure +--disable-silent-rules' sets the default to verbose, which can be +overridden with `make V=0'. + +Particular systems +================== + + On HP-UX, the default C compiler is not ANSI C compatible. If GNU +CC is not installed, it is recommended to use the following options in +order to use an ANSI C compiler: + + ./configure CC="cc -Ae -D_XOPEN_SOURCE=500" + +and if that doesn't work, install pre-built binaries of GCC for HP-UX. + + HP-UX `make' updates targets which have the same time stamps as +their prerequisites, which makes it generally unusable when shipped +generated files such as `configure' are involved. Use GNU `make' +instead. + + On OSF/1 a.k.a. Tru64, some versions of the default C compiler cannot +parse its `' header file. The option `-nodtk' can be used as +a workaround. If GNU CC is not installed, it is therefore recommended +to try + + ./configure CC="cc" + +and if that doesn't work, try + + ./configure CC="cc -nodtk" + + On Solaris, don't put `/usr/ucb' early in your `PATH'. This +directory contains several dysfunctional programs; working variants of +these programs are available in `/usr/bin'. So, if you need `/usr/ucb' +in your `PATH', put it _after_ `/usr/bin'. + + On Haiku, software installed for all users goes in `/boot/common', +not `/usr/local'. It is recommended to use the following options: + + ./configure --prefix=/boot/common + +Specifying the System Type +========================== + + There may be some features `configure' cannot figure out +automatically, but needs to determine by the type of machine the package +will run on. Usually, assuming the package is built to be run on the +_same_ architectures, `configure' can figure that out, but if it prints +a message saying it cannot guess the machine type, give it the +`--build=TYPE' option. TYPE can either be a short name for the system +type, such as `sun4', or a canonical name which has the form: + + CPU-COMPANY-SYSTEM + +where SYSTEM can have one of these forms: + + OS + KERNEL-OS + + See the file `config.sub' for the possible values of each field. If +`config.sub' isn't included in this package, then this package doesn't +need to know the machine type. + + If you are _building_ compiler tools for cross-compiling, you should +use the option `--target=TYPE' to select the type of system they will +produce code for. + + If you want to _use_ a cross compiler, that generates code for a +platform different from the build platform, you should specify the +"host" platform (i.e., that on which the generated programs will +eventually be run) with `--host=TYPE'. + +Sharing Defaults +================ + + If you want to set default values for `configure' scripts to share, +you can create a site shell script called `config.site' that gives +default values for variables like `CC', `cache_file', and `prefix'. +`configure' looks for `PREFIX/share/config.site' if it exists, then +`PREFIX/etc/config.site' if it exists. Or, you can set the +`CONFIG_SITE' environment variable to the location of the site script. +A warning: not all `configure' scripts look for a site script. + +Defining Variables +================== + + Variables not defined in a site shell script can be set in the +environment passed to `configure'. However, some packages may run +configure again during the build, and the customized values of these +variables may be lost. In order to avoid this problem, you should set +them in the `configure' command line, using `VAR=value'. For example: + + ./configure CC=/usr/local2/bin/gcc + +causes the specified `gcc' to be used as the C compiler (unless it is +overridden in the site shell script). + +Unfortunately, this technique does not work for `CONFIG_SHELL' due to +an Autoconf bug. Until the bug is fixed you can use this workaround: + + CONFIG_SHELL=/bin/bash /bin/bash ./configure CONFIG_SHELL=/bin/bash + +`configure' Invocation +====================== + + `configure' recognizes the following options to control how it +operates. + +`--help' +`-h' + Print a summary of all of the options to `configure', and exit. + +`--help=short' +`--help=recursive' + Print a summary of the options unique to this package's + `configure', and exit. The `short' variant lists options used + only in the top level, while the `recursive' variant lists options + also present in any nested packages. + +`--version' +`-V' + Print the version of Autoconf used to generate the `configure' + script, and exit. + +`--cache-file=FILE' + Enable the cache: use and save the results of the tests in FILE, + traditionally `config.cache'. FILE defaults to `/dev/null' to + disable caching. + +`--config-cache' +`-C' + Alias for `--cache-file=config.cache'. + +`--quiet' +`--silent' +`-q' + Do not print messages saying which checks are being made. To + suppress all normal output, redirect it to `/dev/null' (any error + messages will still be shown). + +`--srcdir=DIR' + Look for the package's source code in directory DIR. Usually + `configure' can determine that directory automatically. + +`--prefix=DIR' + Use DIR as the installation prefix. *note Installation Names:: + for more details, including other options available for fine-tuning + the installation locations. + +`--no-create' +`-n' + Run the configure checks, but stop before creating any output + files. + +`configure' also accepts some other, not widely useful, options. Run +`configure --help' for more details. + diff --git a/proofs/lfsc_checker/Makefile.am b/proofs/lfsc_checker/Makefile.am new file mode 100644 index 000000000..ff483f5fb --- /dev/null +++ b/proofs/lfsc_checker/Makefile.am @@ -0,0 +1,30 @@ +AM_CXXFLAGS = -Wall -Wno-deprecated + +bin_PROGRAMS = lfsc-checker + +lfsc_checker_SOURCES = \ + main.cpp +lfsc_checker_LDADD = \ + @builddir@/liblfsc_checker.la + +noinst_LTLIBRARIES = liblfsc_checker.la + +liblfsc_checker_la_SOURCES = \ + check.cpp \ + check.h \ + chunking_memory_management.h \ + code.cpp \ + code.h \ + expr.cpp \ + expr.h \ + libwriter.cpp \ + libwriter.h \ + position.h \ + print_smt2.cpp \ + print_smt2.h \ + scccode.cpp \ + scccode.h \ + sccwriter.cpp \ + sccwriter.h \ + trie.cpp \ + trie.h diff --git a/proofs/lfsc_checker/NEWS b/proofs/lfsc_checker/NEWS new file mode 100644 index 000000000..1a357ab4c --- /dev/null +++ b/proofs/lfsc_checker/NEWS @@ -0,0 +1,9 @@ +This file contains a summary of important user-visible changes to the +LFSC proof checker. + +Changes since pre-1.0 (unversioned) releases +============================================ + +* Incorporated the LFSC checker into the CVC4 project. + +-- Morgan Deters Thu, 12 Dec 2013 18:16:08 -0500 diff --git a/proofs/lfsc_checker/README b/proofs/lfsc_checker/README new file mode 100644 index 000000000..5073569bc --- /dev/null +++ b/proofs/lfsc_checker/README @@ -0,0 +1,83 @@ +lfsc: a high-performance LFSC proof checker. + +Andy Reynolds and Aaron Stump + +---------------------------------------------------------------------- +Command line parameters for LFSC: + +lfsc [sig_1 .... sig_n] [opts_1...opts_n] + +[sig_1 .... sig_n] are signature files, and options [opts_1...opts_n] +are any of the following: + +--compile-scc : Write out all side conditions contained in signatures + specified on the command line to files scccode.h, scccode.cpp (see + below for example) + +--run-scc : Run proof checking with compiled side condition code (see + below). + +--compile-scc-debug : Write side condition code to scccode.h, + scccode.cpp that contains print statements (for debugging running of + side condition code). + + + + +Typical usage: + +./src/opt/lfsc [sig_1 .... sig_n] [proof] [opts_1...opts_n] + +A proof is typically specified at the end of the list of input files +in file [proof]. This will tell LFSC to type check the proof term in +the file [proof]. The extension (*.plf) is commonly used for both +user signature files and proof files. + + + + +Side condition code compilation: + +LFSC may be used with side condition code compilation. This will take +all side conditions ("program" constructs) in the user signature and +produce equivalent C++ code in the output files scccode.h, +scccode.cpp. + +An example for QF_IDL running with side condition code compilation: + +(1) In the src/ directory, run LFSC with the command line parameters: + +./opt/lfsc ../sat-tests/sat.plf ../sat-tests/smt.plf \ + ../sat-tests/cnf_conv.plf ../sat-tests/th_base.plf \ + ../sat-tests/th_idl.plf --compile-scc + +This will produce scccode.h and scccode.cpp in the working directory +where lfsc was run (here, src/). + +(2) Recompile the code base for lfsc. This will produce a copy of the +LFSC executable that is capable of calling side conditions directly as +compiled C++. + +(3) To check a proof.plf* with side condition code compilation, run +LFSC with the command line parameters: + +./opt/lfsc ../sat-tests/sat.plf ../sat-tests/smt.plf \ + ../sat-tests/cnf_conv.plf ../sat-tests/th_base.plf \ + ../sat-tests/th_idl.plf --run-scc proof.plf + + + +*Note that this proof must be compatible with the proof checking + signature. The proof generator is responsible for producing a proof + in the proper format that can be checked by the proof signature + specified when running LFSC. + +For example, in the case of CLSAT in the QF_IDL logic, older proofs +(proofs produced before Feb 2009) may be incompatible with the newest +version of the resolution checking signature (sat.plf). The newest +version of CLSAT -- which can be checked out from the Iowa repository +with + +svn co https://svn.divms.uiowa.edu/repos/clc/clsat/trunk clsat + +should produce proofs compatible with the current version of sat.plf. diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp new file mode 100644 index 000000000..8ef114115 --- /dev/null +++ b/proofs/lfsc_checker/check.cpp @@ -0,0 +1,1383 @@ +#include "position.h" +#include "check.h" +#include "code.h" +#include "expr.h" +#include "trie.h" +#include "sccwriter.h" +#include "libwriter.h" +#ifndef _MSC_VER +#include +#endif +#include +#include +#include +#include "scccode.h" +#include "print_smt2.h" + +using namespace std; +#ifndef _MSC_VER +using namespace __gnu_cxx; +#endif + +int linenum = 1; +int colnum = 1; +const char *filename = 0; +FILE *curfile = 0; + +//#define USE_HASH_MAPS + +symmap2 progs; +std::vector< Expr* > ascHoles; + +#ifdef USE_HASH_MAPS +hash_map symbols; +hash_map symbol_types; +#else +Trie > *symbols = new Trie >; +#endif + +hash_map imports; +std::map mark_map; +std::vector< std::pair< std::string, std::pair > > local_sym_names; + +Expr *not_defeq1 = 0; +Expr *not_defeq2 = 0; + +bool tail_calls = true; +bool big_check = true; + +void report_error(const string &msg) { + if (filename) { + Position p(filename,linenum,colnum); + p.print(cout); + } + cout << "\n"; + cout << msg; + cout << "\n"; + if (not_defeq1 && not_defeq2) { + cout << "The following terms are not definitionally equal:\n1. "; + not_defeq1->print(cout); + cout << "\n2. "; + not_defeq2->print(cout); + } + cout.flush(); + _exit(1); +} + +Expr *call_run_code(Expr *code) { + if (dbg_prog) { + cout << "[Running "; + code->print(cout); + cout << "\n"; + } + Expr *computed_result = run_code(code); + if (dbg_prog) { + cout << "] returning "; + if (computed_result) + computed_result->print(cout); + else + cout << "fail"; + cout << "\n"; + } + return computed_result; +} + +char our_getc_c = 0; + +int IDBUF_LEN = 2048; +char idbuf[2048]; + +Expr *statType = new CExpr(TYPE, 0); +Expr *statKind = new CExpr(KIND, 0); +Expr *statMpz = new CExpr(MPZ,0); +Expr *statMpq = new CExpr(MPQ,0); + +int open_parens = 0; + +// only call in check() +void eat_rparen() { + eat_char(')'); + open_parens--; +} + +void eat_excess(int prev) { + while(open_parens > prev) + eat_rparen(); +} + +/* There are four cases for check(): + +1. expected=0, create is false: check() sets computed to be the classifier of + the checked term. + +2. expected=0, create is true: check() returns + the checked expression and sets computed to be its classifier. + +3. expected is non-null, create is false: check returns NULL. + +4. expected is non-null, create is true: check returns the term that + was checked. + +We consume the reference for expected, to enable tail calls in the +application case. + +If is_hole is NULL, then the expression parsed may not be a hole. +Otherwise, it may be, and we will set *is_hole to true if it is +(but leave *is_hole alone if it is not). + +*/ + +bool allow_run = false; +int app_rec_level = 0; + +Expr *check(bool create, Expr *expected, Expr **computed = NULL, + bool *is_hole = 0, bool return_pos = false, bool inAsc = false ) { + start_check: + //std::cout << "check code "; + //if( expected ) + // expected->print( std::cout ); + //std::cout << std::endl; + char d = non_ws(); + switch(d) { + case '(': { + + open_parens++; + + char c = non_ws(); + switch (c) { + case EOF: + report_error("Unexpected end of file."); + break; + case '!': { // the pi case + string id(prefix_id()); +#ifdef DEBUG_SYM_NAMES + Expr *sym = new SymSExpr(id,SYMS_EXPR); +#else + Expr *sym = new SymExpr(id); + //std::cout << "name " << id << " " << sym << std::endl; +#endif + allow_run = true; + int prevo = open_parens; + Expr *domain = check(true, statType); + eat_excess(prevo); + allow_run = false; +#ifdef USE_HASH_MAPS + Expr *prev = symbols[id]; + Expr *prevtp = symbol_types[id]; + symbols[id] = sym; + symbol_types[id] = domain; +#else + pairprev = + symbols->insert(id.c_str(),pair(sym,domain)); +#endif + if (expected) + expected->inc(); + Expr *range = check(create, expected, computed, NULL, return_pos); + eat_excess(prevo); + eat_rparen(); + +#ifdef USE_HASH_MAPS + symbols[id] = prev; + symbol_types[id] = prevtp; +#else + symbols->insert(id.c_str(),prev); +#endif + if (expected) { + int o = expected->followDefs()->getop(); + expected->dec(); + if (o != TYPE && o != KIND) + report_error(string("The expected classifier for a pi abstraction") + +string("is neither \"type\" nor \"kind\".\n") + +string("1. the expected classifier: ") + +expected->toString()); + if (create){ + CExpr* ret = new CExpr(PI, sym, domain, range); + ret->calc_free_in(); + return ret; + } + return 0; + } + else { + if (create){ + CExpr* ret = new CExpr(PI, sym, domain, range); + ret->calc_free_in(); + return ret; + } + int o = (*computed)->followDefs()->getop(); + if (o != TYPE && o != KIND) + report_error(string("The classifier for the range of a pi") + +string("abstraction is neither \"type\" nor ") + +string("\"kind\".\n1. the computed classifier: ") + +range->toString()); + return 0; + } + } + case '%': { // the case for big lambda + if (expected || create || !return_pos || !big_check) + report_error(string("Big lambda abstractions can only be used") + +string("in the return position of a \"bigcheck\"\n") + +string("command.")); + string id(prefix_id()); +#ifdef DEBUG_SYM_NAMES + SymExpr *sym = new SymSExpr(id, SYMS_EXPR); +#else + SymExpr *sym = new SymExpr(id); + //std::cout << "name " << id << " " << sym << std::endl; +#endif + + int prevo = open_parens; + Expr *expected_domain = check(true, statType); + eat_excess(prevo); + +#ifdef USE_HASH_MAPS + Expr *prev = symbols[id]; + Expr *prevtp = symbol_types[id]; + symbols[id] = sym; + symbol_types[id] = expected_domain; +#else + pair prevpr = + symbols->insert(id.c_str(), pair(sym,expected_domain)); + Expr *prev = prevpr.first; + Expr *prevtp = prevpr.second; +#endif + expected_domain->inc(); // because we have stored it in the symbol table + + //will clean up local sym name eventually + local_sym_names.push_back( std::pair< std::string, std::pair >( id, prevpr ) ); + if (prev) + prev->dec(); + if (prevtp) + prevtp->dec(); + create = false; + expected = NULL; + // computed unchanged + is_hole = NULL; + // return_pos unchanged + + // note we will not store the proper return type in computed. + + goto start_check; + } + + case '\\': { // the lambda case + if (!expected) + report_error(string("We are computing a type for a lambda ") + +string("abstraction, but we can only check\n") + +string("such against a type. Try inserting an ") + +string("ascription (using ':').\n")); + Expr *orig_expected = expected; + expected = expected->followDefs(); + if (expected->getop() != PI) + report_error(string("We are type-checking a lambda abstraction, but\n") + +string("the expected type is not a pi abstraction.\n") + +string("1. The expected type: ") + expected->toString()); + string id(prefix_id()); +#ifdef DEBUG_SYM_NAMES + SymExpr *sym = new SymSExpr(id, SYMS_EXPR); +#else + SymExpr *sym = new SymExpr(id); + //std::cout << "name " << id << " " << sym << std::endl; +#endif + + CExpr *pitp = (CExpr *)expected; + Expr *expected_domain = pitp->kids[1]; + Expr *expected_range = pitp->kids[2]; + SymExpr *pivar = (SymExpr *)pitp->kids[0]; + if (expected_range->followDefs()->getop() == TYPE) + report_error(string("The expected classifier for a lambda abstraction") + +string(" a kind, not a type.\n") + +string("1. The expected classifier: ") + +expected->toString()); + + /* we need to map the pivar to the new sym, because in our + higher-order matching we may have (_ x) to unify with t. + The x must be something from an expected type, since only these + can have holes. We want to map expected vars x to computed vars y, + so that we can set the hole to be \ y t, where t contains ys but + not xs. */ + +#ifdef USE_HASH_MAPS + Expr *prev = symbols[id]; + Expr *prevtp = symbol_types[id]; + symbols[id] = sym; + symbol_types[id] = expected_domain; +#else + pair prevpr = + symbols->insert(id.c_str(), pair(sym,expected_domain)); + Expr *prev = prevpr.first; + Expr *prevtp = prevpr.second; +#endif + Expr *prev_pivar_val = pivar->val; + sym->inc(); + pivar->val = sym; + + expected_domain->inc(); // because we have stored it in the symbol table + expected_range->inc(); // because we will pass it to a recursive call + + if (tail_calls && big_check && return_pos && !create) { + //will clean up local sym name eventually + local_sym_names.push_back( std::pair< std::string, std::pair >( id, prevpr ) ); + if (prev_pivar_val) + prev_pivar_val->dec(); + if (prev) + prev->dec(); + if (prevtp) + prevtp->dec(); + orig_expected->dec(); + create = false; + expected = expected_range; + computed = NULL; + is_hole = NULL; + // return_pos unchanged + goto start_check; + } + else { + + int prev = open_parens; + Expr *range = check(create, expected_range, NULL, NULL, return_pos); + eat_excess(prev); + eat_rparen(); + +#ifdef USE_HASH_MAPS + symbols[id] = prev; + symbol_types[id] = prevtp; +#else + symbols->insert(id.c_str(), prevpr); +#endif + expected_domain->dec(); // because removed from the symbol table now + + pivar->val = prev_pivar_val; + + orig_expected->dec(); + + sym->dec(); // the pivar->val reference + if (create) + return new CExpr(LAM, sym, range); + sym->dec(); // the symbol table reference, otherwise in the new LAM + return 0; + } + } + case '^': { // the run case + if (!allow_run || !create || !expected) + report_error(string("A run expression (operator \"^\") appears in") + +string(" a disallowed position.")); + + Expr *code = read_code(); + //string errstr = (string("The first argument in a run expression must be") + // +string(" a call to a program.\n1. the argument: ") + // +code->toString()); + + /* determine expected type of the result term, and make sure + the code term is an allowed one. */ +#if 0 + Expr *progret; + if (code->isArithTerm()) + progret = statMpz; + else { + if (code->getop() != APP) + report_error(errstr); + + CExpr *call = (CExpr *)code; + + // prog is not known to be a SymExpr yet + CExpr *prog = (CExpr *)call->get_head(); + + if (prog->getop() != PROG) + report_error(errstr); + + progret = prog->kids[0]->get_body(); + } +#else + Expr *progret = NULL; + if (code->isArithTerm()) + progret = statMpz; + else { + if (code->getop() == APP) + { + CExpr *call = (CExpr *)code; + + // prog is not known to be a SymExpr yet + CExpr *prog = (CExpr *)call->get_head(); + + if (prog->getop() == PROG) + progret = prog->kids[0]->get_body(); + } + } +#endif + /* determine expected type of the result term, and make sure + the code term is an allowed one. */ + //Expr* progret = check_code( code ); + + /* the next term cannot be a hole where run expressions are introduced. + When they are checked in applications, it can be. */ + int prev = open_parens; + if( progret ) + progret->inc(); + Expr *trm = check(true, progret); + eat_excess(prev); + eat_rparen(); + + if (expected->getop() != TYPE) + report_error(string("The expected type for a run expression is not ") + +string("\"type\".\n") + +string("1. The expected type: ")+expected->toString()); + expected->dec(); + return new CExpr(RUN, code, trm); + } + + case ':': { // the ascription case + statType->inc(); + int prev = open_parens; + Expr *tp = check(true, statType, NULL, NULL, false, true ); + eat_excess(prev); + + if (!expected) + tp->inc(); + + Expr *trm = check(create, tp, NULL, NULL, return_pos); + eat_excess(prev); + eat_rparen(); + if (expected) { + if (!expected->defeq(tp)) + report_error(string("The expected type does not match the ") + +string("ascribed type in an ascription.\n") + +string("1. The expected type: ")+expected->toString() + +string("\n2. The ascribed type: ")+tp->toString()); + + // no need to dec tp, since it was consumed by the call to check + expected->dec(); + if (create) + return trm; + trm->dec(); + return 0; + } + else { + *computed = tp; + if (create) + return trm; + return 0; + } + } + case '@': { // the local definition case + string id(prefix_id()); +#ifdef DEBUG_SYM_NAMES + SymExpr *sym = new SymSExpr(id, SYMS_EXPR); +#else + SymExpr *sym = new SymExpr(id); +#endif + int prev_open = open_parens; + Expr *tp_of_trm; + Expr *trm = check(true, NULL, &tp_of_trm); + eat_excess(prev_open); + + sym->val = trm; + +#ifdef USE_HASH_MAPS + Expr *prev = symbols[id]; + Expr *prevtp = symbol_types[id]; + symbols[id] = sym; + symbol_types[id] = tp_of_trm; +#else + pair prevpr = + symbols->insert(id.c_str(), pair(sym,tp_of_trm)); + Expr *prev = prevpr.first; + Expr *prevtp = prevpr.second; +#endif + + if (tail_calls && big_check && return_pos && !create) { + if (prev) + prev->dec(); + if (prevtp) + prevtp->dec(); + // all parameters to check() unchanged here + goto start_check; + } + else { + int prev_open = open_parens; + Expr *body = check(create, expected, computed, is_hole, return_pos); + eat_excess(prev_open); + eat_rparen(); + +#ifdef USE_HASH_MAPS + symbols[id] = prev; + symbol_types[id] = prevtp; +#else + symbols->insert(id.c_str(), prevpr); +#endif + tp_of_trm->dec(); // because removed from the symbol table now + + sym->dec(); + return body; + } + } + case '~': { + int prev = open_parens; + Expr *e = check(create, expected, computed, is_hole, return_pos); + eat_excess(prev); + eat_rparen(); + + // this has been only very lightly tested -- ads. + + if (expected) { + if (expected != statMpz && expected != statMpq) + report_error("Negative sign where an numeric expression is expected."); + } + else { + if ((*computed) != statMpz && (*computed) != statMpq) + report_error("Negative sign where an numeric expression is expected."); + } + + if (create) { + if (e->getclass() == INT_EXPR) + { + IntExpr *ee = (IntExpr *)e; + mpz_neg(ee->n, ee->n); + return ee; + } + else if( e->getclass() == RAT_EXPR ) + { + RatExpr *ee = (RatExpr *)e; + mpq_neg(ee->n, ee->n); + return ee; + } + else + { + report_error("Negative sign with expr that is not an int. literal."); + } + } + else + return 0; + } + default: { // the application case + our_ungetc(c); + Expr *head_computed; + int prev = open_parens; + Expr *headtrm = check(create,0,&head_computed); + eat_excess(prev); + + CExpr *headtp = (CExpr *)head_computed->followDefs(); + headtp->inc(); + head_computed->dec(); + if ( headtp->cloned()) { + // we must clone + Expr *orig_headtp = headtp; + headtp = (CExpr *)headtp->clone(); + orig_headtp->dec(); + } + else + headtp->setcloned(); +#ifdef DEBUG_APPS + char tmp[100]; + sprintf(tmp,"(%d) ", app_rec_level++); + cout << tmp << "{ headtp = "; + headtp->debug(); +#endif + char c; + vector holes; + vector free_holes; + while ((c = non_ws()) != ')') { + our_ungetc(c); + if (headtp->getop() != PI) + report_error(string("The type of an applied term is not ") + + string("a pi-type.\n") + + string("\n1. the type of the term: ") + + headtp->toString() + + (headtrm ? (string("\n2. the term: ") + + headtrm->toString()) + : string(""))); + SymExpr *headtp_var = (SymExpr *)headtp->kids[0]; + Expr *headtp_domain = headtp->kids[1]; + Expr *headtp_range = headtp->kids[2]; + if (headtp_domain->getop() == RUN) { + CExpr *run = (CExpr *)headtp_domain; + Expr *code = run->kids[0]; + Expr *expected_result = run->kids[1]; + Expr *computed_result = call_run_code(code); + if (!computed_result) + report_error(string("A side condition failed.\n") + +string("1. the side condition: ") + +code->toString()); + if (!expected_result->defeq(computed_result)) + report_error(string("The expected result of a side condition ") + +string("does not match the computed result.\n") + +string("1. expected result: ") + +expected_result->toString() + +string("\n2. computed result: ") + +computed_result->toString()); + computed_result->dec(); + } + else { + // check an argument + bool var_in_range = headtp->get_free_in();//headtp_range->free_in(headtp_var); + bool arg_is_hole = false; + bool consumed_arg = false; + + bool create_arg = (create || var_in_range); + + headtp_domain->inc(); + + if (tail_calls && !create_arg && headtp_range->getop() != PI) { + // we can make a tail call to check() here. + + if (expected) { + if (!expected->defeq(headtp_range)) + report_error(string("The type expected for an application ") + + string("does not match the computed type.\n") + + string("1. The expected type: ") + + expected->toString() + + string("\n2. The computed type: ") + + headtp_range->toString() + + (headtrm ? (string("\n3. the application: ") + + headtrm->toString()) + : string(""))); + expected->dec(); + } + else { + headtp_range->inc(); + *computed = headtp_range; + } + + headtp->dec(); + + // same as below + for (int i = 0, iend = holes.size(); i < iend; i++) { + if (!holes[i]->val) + /* if the hole is free in the domain, we will be filling + it in when we make our tail call, since the domain + is the expected type for the argument */ + if (!headtp_domain->free_in(holes[i])) + report_error(string("A hole was left unfilled after ") + +string("checking an application.\n")); + holes[i]->dec(); + } + + create = false; + expected = headtp_domain; + computed = NULL; + is_hole = NULL; // the argument cannot be a hole + // return_pos is unchanged + +#ifdef DEBUG_APPS + cout << "Making tail call.\n"; +#endif + + goto start_check; + } + + Expr *arg = check(create_arg, headtp_domain, NULL, &arg_is_hole); + eat_excess(prev); + if (create) { +#ifndef USE_FLAT_APP + headtrm = new CExpr(APP, headtrm, arg); +#else + headtrm = Expr::make_app( headtrm, arg ); +#endif + consumed_arg = true; + } + if (var_in_range) { + Expr *tmp = arg->followDefs(); + tmp->inc(); + headtp_var->val = tmp; + } + if (arg_is_hole) { + if (consumed_arg) + arg->inc(); + else + consumed_arg = true; // not used currently +#ifdef DEBUG_HOLES + cout << "An argument is a hole: "; + arg->debug(); +#endif + holes.push_back((HoleExpr *)arg); + } + } + headtp_range->inc(); + headtp->dec(); + headtp = (CExpr *)headtp_range; + } + open_parens--; + + // check for remaining RUN in the head's type after all the arguments + + if (headtp->getop() == PI && headtp->kids[1]->getop() == RUN) { + CExpr *run = (CExpr *)headtp->kids[1]; + Expr *code = run->kids[0]->followDefs(); + Expr *expected_result = run->kids[1]; + Expr *computed_result = call_run_code(code); + if (!computed_result) + report_error(string("A side condition failed.\n") + +string("1. the side condition: ")+code->toString()); + if (!expected_result->defeq(computed_result)) + report_error(string("The expected result of a side condition ") + +string("does not match the computed result.\n") + +string("1. expected result: ") + +expected_result->toString() + +string("\n2. computed result: ") + +computed_result->toString()); + Expr *tmp = headtp->kids[2]; + tmp->inc(); + headtp->dec(); + headtp = (CExpr *)tmp; + computed_result->dec(); + } + +#ifdef DEBUG_APPS + for (int i = 0, iend = holes.size(); i < iend; i++) { + cout << tmp << "hole "; + holes[i]->debug(); + } + cout << "}"; + app_rec_level--; +#endif + + Expr *ret = 0; + if (expected) { + if (!expected->defeq(headtp)){ + report_error(string("The type expected for an application does not") + + string(" match the computed type.(2) \n") + + string("1. The expected type: ") + + expected->toString() + + string("\n2. The computed type: ") + + headtp->toString() + + (headtrm ? (string("\n3. the application: ") + + headtrm->toString()) + : string(""))); + + } + expected->dec(); + headtp->dec(); + if (create) + ret = headtrm; + } + else { + *computed = headtp; + if (create) + ret = headtrm; + } + + /* do this check here to give the defeq() call above a + chance to fill in some holes */ + for (int i = 0, iend = holes.size(); i < iend; i++) { + if (!holes[i]->val){ + if( inAsc ){ +#ifdef DEBUG_HOLES + std::cout << "Ascription Hole: "; + holes[i]->print( std::cout ); + std::cout << std::endl; +#endif + ascHoles.push_back( holes[i] ); + }else{ + report_error(string("A hole was left unfilled after checking") + +string(" an application (2).\n")); + } + } + holes[i]->dec(); + } + + return ret; + + } // end application case + } + } + case EOF: + report_error("Unexpected end of file."); + break; + + case '_': + if (!is_hole) + report_error("A hole is being used in a disallowed position."); + *is_hole = true; + if (expected) + expected->dec(); + return new HoleExpr(); + case '0': + case '1': + case '2': + case '3': + case '4': + case '5': + case '6': + case '7': + case '8': + case '9': { + our_ungetc(d); + string v; + char c; + while (isdigit(c = our_getc())) + v.push_back(c); + bool parseMpq = false; + string v2; + if( c=='/' ) + { + parseMpq = true; + v.push_back( c ); + while(isdigit(c = our_getc())) + v.push_back(c); + } + our_ungetc(c); + + + Expr *i = 0; + if (create) { + if( parseMpq ) + { + mpq_t num; + mpq_init(num); + if (mpq_set_str(num,v.c_str(),10) == -1) + report_error("Error reading a numeral."); + i = new RatExpr(num); + } + else + { + mpz_t num; + if (mpz_init_set_str(num,v.c_str(),10) == -1) + report_error("Error reading a numeral."); + i = new IntExpr(num); + } + } + + if (expected) { + if( ( !parseMpq && expected != statMpz ) || ( parseMpq && expected != statMpq ) ) + report_error(string("We parsed a numeric literal, but were ") + +string("expecting a term of a different type.\n") + +string("1. the expected type: ")+expected->toString()); + expected->dec(); + if (create) + return i; + return 0; + } + else { + if( parseMpq ) + { + statMpq->inc(); + *computed = statMpq; + if (create) + return i; + return statMpq; + } + else + { + statMpz->inc(); + *computed = statMpz; + if (create) + return i; + return statMpz; + } + } + } + default: { + our_ungetc(d); + string id(prefix_id()); +#ifdef USE_HASH_MAPS + Expr *ret = symbols[id]; + Expr *rettp = symbol_types[id]; +#else + pair p = symbols->get(id.c_str()); + Expr *ret = p.first; + Expr *rettp = p.second; +#endif + if (!ret) + report_error(string("Undeclared identifier: ")+id); + if (expected) { + if (!expected->defeq(rettp)) + report_error(string("The type expected for a symbol does not") + + string(" match the symbol's type.\n") + + string("1. The symbol: ") + + id + + string("\n2. The expected type: ") + + expected->toString() + + string("\n3. The symbol's type: ") + + rettp->toString()); + expected->dec(); + if (create) { + ret->inc(); + return ret; + } + return 0; + } + else { + if( computed ){ + *computed = rettp; + (*computed)->inc(); + } + if (create) { + ret->inc(); + return ret; + } + return 0; + } + } + } + + report_error("Unexpected operator at the start of a term."); + return 0; +} + +#ifdef USE_HASH_MAPS +void discard_old_symbol(const string &id) { + Expr *tmp = symbols[id]; + if (tmp) + tmp->dec(); + tmp = symbol_types[id]; + if (tmp) + tmp->dec(); +} +#endif + +int check_time; + +void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) { + int prev_linenum = linenum; + int prev_colnum = colnum; + const char *prev_filename = filename; + FILE * prev_curfile = curfile; + + // from code.h + dbg_prog = a.show_runs; + run_scc = a.run_scc; + tail_calls = !a.no_tail_calls; + + + char *f; + if (strcmp(_filename,"stdin") == 0) { + curfile = stdin; + f = strdup(_filename); + } + else { + if (prev_curfile) { + f = strdup(prev_filename); +#ifdef _MSC_VER + std::string str( f ); + for( int n=str.length(); n>=0; n-- ){ + if( str[n]=='\\' || str[n]=='/' ){ + str = str.erase( n, str.length()-n ); + break; + } + } + char *tmp = (char*)str.c_str(); +#else + char *tmp = dirname(f); +#endif + delete f; + f = new char[strlen(tmp) + 10 + strlen(_filename)]; + strcpy(f,tmp); + strcat(f,"/"); + strcat(f,_filename); + } + else + f = strdup(_filename); + curfile = fopen(f,"r"); + if (!curfile) + report_error(string("Could not open file \"") + + string(f) + + string("\" for reading.\n")); + } + + linenum = 1; + colnum = 1; + filename = f; + + char c; + while ((c = non_ws()) && c!=EOF ) { + if( c == '(' ) + { + char d; + switch ((d = non_ws())) { + case 'd': + char b; + if ((b = our_getc()) != 'e') + report_error(string("Unexpected start of command.")); + + switch ((b = our_getc())) { + case 'f': {// expecting "define" + + if (our_getc() != 'i' || our_getc() != 'n' || our_getc() != 'e') + report_error(string("Unexpected start of command.")); + + string id(prefix_id()); + Expr *ttp; + int prevo = open_parens; + Expr *t = check(true, 0, &ttp, NULL, true); + eat_excess(prevo); + + int o = ttp->followDefs()->getop(); + if (o == KIND) + report_error(string("Kind-level definitions are not supported.\n")); + SymSExpr *s = new SymSExpr(id); + s->val = t; +#ifdef USE_HASH_MAPS + discard_old_symbol(id); + symbols[id] = s; + symbol_types[id] = ttp; +#else + pair prev = + symbols->insert(id.c_str(), pair(s,ttp)); + if (prev.first) + prev.first->dec(); + if (prev.second) + prev.second->dec(); +#endif + break; + } + case 'c': {// expecting "declare" + if (our_getc() != 'l' || our_getc() != 'a' || our_getc() != 'r' + || our_getc() != 'e') + report_error(string("Unexpected start of command.")); + + string id(prefix_id()); + Expr *ttp; + int prevo = open_parens; + Expr *t = check(true, 0, &ttp, NULL, true); + eat_excess(prevo); + + ttp = ttp->followDefs(); + if (ttp->getop() != TYPE && ttp->getop() != KIND) + report_error(string("The expression declared for \"") + +id+string("\" is neither\na type nor a kind.\n") + +string("1. The expression: ") + +t->toString() + +string("\n2. Its classifier (should be \"type\" ") + +string("or \"kind\"): ")+ttp->toString()); + ttp->dec(); + SymSExpr *s = new SymSExpr(id); +#ifdef USE_HASH_MAPS + discard_old_symbol(id); + symbols[id] = s; + symbol_types[id] = t; +#else + pair prev = + symbols->insert(id.c_str(), pair(s,t)); + if( lw ) + lw->add_symbol( s, t ); + if (prev.first) + prev.first->dec(); + if (prev.second) + prev.second->dec(); +#endif + break; + } + default: + report_error(string("Unexpected start of command.")); + } // switch((b = our_getc())) following "de" + break; + case 'c': { + if (our_getc() != 'h' || our_getc() != 'e' || our_getc() != 'c' || our_getc() != 'k') + report_error(string("Unexpected start of command.")); + if( run_scc ){ + init_compiled_scc(); + } + Expr *computed; + big_check = true; + int prev = open_parens; + (void)check(false, 0, &computed, NULL, true); + + //print out ascription holes + for( int a=0; a<(int)ascHoles.size(); a++ ){ +#ifdef PRINT_SMT2 + print_smt2( ascHoles[a], std::cout ); +#else + ascHoles[a]->print( std::cout ); +#endif + std::cout << std::endl; + } + if( !ascHoles.empty() ) + std::cout << std::endl; + ascHoles.clear(); + + //clean up local symbols + for( int a=0; a<(int)local_sym_names.size(); a++ ){ +#ifdef USE_HASH_MAPS +#else + symbols->insert( local_sym_names[a].first.c_str(), local_sym_names[a].second ); +#endif + } + local_sym_names.clear(); + mark_map.clear(); + + eat_excess(prev); + + computed->dec(); + //cleanup(); + //exit(0); + break; + } + case 'o': { // opaque case + if (our_getc() != 'p' || our_getc() != 'a' || our_getc() != 'q' + || our_getc() != 'u' || our_getc() != 'e') + report_error(string("Unexpected start of command.")); + + string id(prefix_id()); + Expr *ttp; + int prevo = open_parens; + (void)check(false, 0, &ttp, NULL, true); + eat_excess(prevo); + + int o = ttp->followDefs()->getop(); + if (o == KIND) + report_error(string("Kind-level definitions are not supported.\n")); + SymSExpr *s = new SymSExpr(id); +#ifdef USE_HASH_MAPS + discard_old_symbol(id); + symbols[id] = s; + symbol_types[id] = ttp; +#else + pair prev = + symbols->insert(id.c_str(), pair(s,ttp)); + if (prev.first) + prev.first->dec(); + if (prev.second) + prev.second->dec(); +#endif + break; + } + case 'r': { // run case + if (our_getc() != 'u' || our_getc() != 'n') + report_error(string("Unexpected start of command.")); + Expr *code = read_code(); + check_code(code); + cout << "[Running-sc "; + code->print(cout); + Expr *tmp = run_code(code); + cout << "] = \n"; + if (tmp) { + tmp->print(cout); + tmp->dec(); + } + else + cout << "fail"; + cout << "\n"; + code->dec(); + break; + } + case 'p': { // program case + if (our_getc() != 'r' || our_getc() != 'o' || our_getc() != 'g' + || our_getc() != 'r' || our_getc() != 'a' || our_getc() != 'm') + report_error(string("Unexpected start of command.")); + + string progstr(prefix_id()); + SymSExpr *prog = new SymSExpr(progstr); + if (progs.find(progstr) != progs.end()) + report_error(string("Redeclaring program ")+progstr+string(".")); + progs[progstr] = prog; + eat_char('('); + char d; + vector vars; + vector tps; + Expr *tmp; + while ((d = non_ws()) != ')') { + our_ungetc(d); + eat_char('('); + string varstr = prefix_id(); +#ifdef USE_HASH_MAPS + if (symbols.find(varstr) != symbols.end()) +#else + if (symbols->get(varstr.c_str()).first != NULL) +#endif + report_error(string("A program variable is already declared") + +string(" (as a constant).\n1. The variable: ") + +varstr); + Expr *var = new SymSExpr(varstr); + vars.push_back(var); + statType->inc(); + int prev = open_parens; + Expr *tp = check(true, NULL, &tmp, 0, true); + if( tp->getclass()==SYMS_EXPR ){ +#ifdef USE_HASH_MAPS + Expr *tptp = symbol_types[((SymSExpr*)tp)->s]; +#else + pair p = symbols->get(((SymSExpr*)tp)->s.c_str()); + Expr *tptp = p.second; +#endif + if( !tptp->isType( statType ) ){ + report_error(string("Bad argument for side condition")); + } + }else{ + if (!tp->isDatatype()){ + report_error(string("Type for a program variable is not a ") + +string("datatype.\n1. the type: ")+tp->toString()); + } + } + eat_excess(prev); + + tps.push_back(tp); + eat_char(')'); + +#ifdef USE_HASH_MAPS + symbols[varstr] = var; + symbol_types[varstr] = tp; +#else + symbols->insert(varstr.c_str(), pair(var,tp)); +#endif + } + + if (!vars.size()) + report_error("A program lacks input variables."); + + statType->inc(); + int prev = open_parens; + Expr *progtp = check(true,statType,&tmp,0, true); + eat_excess(prev); + + if (!progtp->isDatatype()) + report_error(string("Return type for a program is not a") + +string(" datatype.\n1. the type: ")+progtp->toString()); + + Expr *progcode = read_code(); + + for (int i = vars.size() - 1, iend = 0; i >= iend; i--) { + vars[i]->inc(); // used below for the program code (progcode) + progtp = new CExpr(PI, vars[i], tps[i], progtp); + progtp->calc_free_in(); + } + + // just put the type here for type checking. Make sure progtp is kid 0. + prog->val = new CExpr(PROG, progtp); + + check_code(progcode); + + progcode = new CExpr(PROG, progtp, new CExpr(PROGVARS, vars), progcode); + //if compiling side condition code, give this code to the side condition code writer + if( a.compile_scc ){ + if( scw ){ + scw->add_scc( progstr, (CExpr*)progcode ); + } + } + + // remove the variables from the symbol table. + for (int i = 0, iend = vars.size(); i < iend; i++) { + string &s = ((SymSExpr *)vars[i])->s; + +#ifdef USE_HASH_MAPS + symbols[s] = NULL; + symbol_types[s] = NULL; +#else + symbols->insert(s.c_str(), pair(NULL,NULL)); +#endif + } + + progtp->inc(); + prog->val->dec(); + + prog->val = progcode; + + break; + } + + default: + report_error(string("Unexpected start of command.")); + } // switch((d = non_ws()) + + eat_char(')'); + } // while + else + { + if( c != ')' ) + { + char c2[2]; + c2[1] = 0; + c2[0] = c; + string syn = string("Bad syntax (mismatched parentheses?): "); + syn.append(string(c2)); + report_error(syn); + } + } + } + free(f); + if (curfile != stdin) + fclose(curfile); + linenum = prev_linenum; + colnum = prev_colnum; + filename = prev_filename; + curfile = prev_curfile; + +} + +class Deref : public Trie >::Cleaner { +public: + ~Deref() {} + void clean(pair p) { + Expr *tmp = p.first; + if (tmp) { +#ifdef DEBUG + cout << "Cleaning up "; + tmp->debug(); +#endif + tmp->dec(); + } + tmp = p.second; + if (tmp) { +#ifdef DEBUG + cout << " : "; + tmp->debug(); +#endif + tmp->dec(); + } +#ifdef DEBUG + cout << "\n"; +#endif + } +}; + +template <> +Trie >::Cleaner * +Trie >::cleaner = new Deref; + +void cleanup() { + symmap::iterator i, iend; +#ifdef USE_HASH_MAPS + Expr *tmp; + for (i = symbols.begin(), iend = symbols.end(); i != iend; i++) { + tmp = i->second; + if (tmp) { +#ifdef DEBUG + cout << "Cleaning up " << i->first << " : "; + tmp->debug(); +#endif + tmp->dec(); + } + } + for (i = symbol_types.begin(), iend = symbol_types.end(); i != iend; i++) { + tmp = i->second; + if (tmp) { +#ifdef DEBUG + cout << "Cleaning up " << i->first << " : "; + tmp->debug(); +#endif + tmp->dec(); + } + } +#else + delete symbols; +#endif + + // clean up programs + + symmap2::iterator j, jend; + for (j = progs.begin(), jend = progs.end(); j != jend; j++) { + SymExpr *p = j->second; + if (p) { + Expr *progcode = p->val; + p->val = NULL; + progcode->dec(); + p->dec(); + } + } +} + +void init() { +#ifdef USE_HASH_MAPS + string tp("type"); + symbols[tp] = statType; + symbol_types[tp] = statKind; + string mpz("mpz"); + symbols[mpz] = statMpz; + symbol_types[mpz] = statType; + statType->inc(); + sym +#else + symbols->insert("type", pair(statType, statKind)); + statType->inc(); + symbols->insert("mpz", pair(statMpz, statType)); + symbols->insert("mpq", pair(statMpq, statType)); +#endif +} diff --git a/proofs/lfsc_checker/check.h b/proofs/lfsc_checker/check.h new file mode 100644 index 000000000..a70599b0f --- /dev/null +++ b/proofs/lfsc_checker/check.h @@ -0,0 +1,167 @@ +#ifndef SC2_CHECK_H +#define SC2_CHECK_H + +#include "expr.h" +#include "trie.h" + +#ifdef _MSC_VER +#include +#include +#else +#include +#endif + +#include +#include +#include + +// see the help message in main.cpp for explanation +typedef struct args { + std::vector files; + bool show_runs; + bool no_tail_calls; + bool compile_scc; + bool compile_scc_debug; + bool run_scc; + bool use_nested_app; + bool compile_lib; +} args; + +extern int check_time; + +class sccwriter; +class libwriter; + +void init(); + +void check_file(const char *_filename, args a, sccwriter* scw = NULL, libwriter* lw = NULL); + +void cleanup(); + +extern char our_getc_c; + +void report_error(const std::string &); + +extern int linenum; +extern int colnum; +extern const char *filename; +extern FILE *curfile; + +inline void our_ungetc(char c) { + if (our_getc_c != 0) + report_error("Internal error: our_ungetc buffer full"); + our_getc_c = c; + if (c == '\n') { + linenum--; + colnum=-1; + } + else + colnum--; +} + +inline char our_getc() { + char c; + if (our_getc_c > 0) { + c = our_getc_c; + our_getc_c = 0; + } + else{ +#ifndef __linux__ + c = fgetc(curfile); +#else + c = fgetc_unlocked(curfile); +#endif + } + switch(c) { + case '\n': + linenum++; +#ifdef DEBUG_LINES + std::cout << "line " << linenum << "." << std::endl; +#endif + colnum = 1; + break; + case EOF: + break; + default: + colnum++; + } + + return c; +} + +// return the next character that is not whitespace +inline char non_ws() { + char c; + while(isspace(c = our_getc())); + if (c == ';') { + // comment to end of line + while((c = our_getc()) != '\n' && c != EOF); + return non_ws(); + } + return c; +} + +inline void eat_char(char expected) { + if (non_ws() != expected) { + char tmp[80]; + sprintf(tmp,"Expecting a \'%c\'",expected); + report_error(tmp); + } +} + +extern int IDBUF_LEN; +extern char idbuf[]; + +inline const char *prefix_id() { + int i = 0; + char c = idbuf[i++] = non_ws(); + while (!isspace(c) && c != '(' && c != ')' && c != EOF) { + if (i == IDBUF_LEN) + report_error("Identifier is too long"); + + idbuf[i++] = c = our_getc(); + } + our_ungetc(c); + idbuf[i-1] = 0; + return idbuf; +} + +#ifdef _MSC_VER +typedef std::hash_map symmap; +typedef std::hash_map symmap2; +#else +typedef __gnu_cxx::hash_map symmap; +typedef __gnu_cxx::hash_map symmap2; +#endif +extern symmap2 progs; +extern std::vector< Expr* > ascHoles; + +#ifdef USE_HASH_MAPS +extern symmap symbols; +extern symmap symbol_types; +#else +extern Trie > *symbols; +#endif + +extern std::map mark_map; + +extern std::vector< std::pair< std::string, std::pair > > local_sym_names; + +#ifndef _MSC_VER +namespace __gnu_cxx +{ + template<> struct hash< std::string > + { + size_t operator()( const std::string& x ) const + { + return hash< const char* >()( x.c_str() ); + } + }; +} +#endif + +extern Expr *statMpz; +extern Expr *statMpq; +extern Expr *statType; + +#endif diff --git a/proofs/lfsc_checker/chunking_memory_management.h b/proofs/lfsc_checker/chunking_memory_management.h new file mode 100644 index 000000000..bdf938d32 --- /dev/null +++ b/proofs/lfsc_checker/chunking_memory_management.h @@ -0,0 +1,157 @@ +/////////////////////////////////////////////////////////////////////////////// +// // +// Copyright (C) 2002 by the Board of Trustees of Leland Stanford // +// Junior University. See LICENSE for details. // +// // +/////////////////////////////////////////////////////////////////////////////// +/* chunking_memory_management.h + Aaron Stump, 6/11/99 + + This file contains macros that allow you easily to add chunking + memory management for classes. + + RCS Version: $Id: chunking_memory_management.h,v 1.1 2004/11/12 16:26:19 stump Exp $ + +*/ +#ifndef _chunking_memory_management_h_ +#define _chunking_memory_management_h_ + +#include + +/************************************************************************ + * MACRO: ADD_CHUNKING_MEMORY_MANAGEMENT_H() + * Aaron Stump, 6/11/99 + * + * ABSTRACT: This macro should be called exactly once inside the body + * of the declaration of the class THE_CLASS to add chunking memory + * management for the class. That class should not itself declare the + * operators new and delete. The macro + * C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_CC should be called with + * the same value for THE_CLASS in a .cc file for that class. + * + * NOTE that the access specifier will be public after calling this + * macro. + * + * THE_FIELD is a field of the class to use for the next pointer in the + * free list data structure. It can be of any type, but must have enough + * space to hold a pointer. + ************************************************************************/ +#define C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_H(THE_CLASS,THE_FIELD) \ +private:\ + static unsigned C_MACROS__CHUNK_SIZE;\ + static unsigned C_MACROS__BLOCK_SIZE;\ + static void *C_MACROS__freelist;\ + static bool C_MACROS__initialized;\ + static char *C_MACROS__next_free_block;\ + static char *C_MACROS__end_of_current_chunk;\ + \ + static void C_MACROS__allocate_new_chunk();\ +\ +public:\ + static void C_MACROS__init_chunks() {\ + if (!C_MACROS__initialized) {\ + C_MACROS__allocate_new_chunk();\ + C_MACROS__initialized = true;\ + }\ + }\ +\ + static void *operator new(size_t size, void *h = NULL);\ + static void operator delete(void *ptr)\ + + +/************************************************************************ + * MACRO: ADD_CHUNKING_MEMORY_MANAGEMENT_CC() + * Aaron Stump, 6/11/99 + * + * ABSTRACT: This macro should be called exactly once in a .cc file + * for the class THE_CLASS to add chunking memory management for the + * class. This macro should be called with the same value for + * THE_CLASS as was used in calling + * C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_H in the body of the + * declaration of THE_CLASS. THE_CHUNK_SIZE is the number of blocks + * of memory to get at once using malloc(). A block is the portion + * of memory needed for one instance of THE_CLASS. + * + * + * IMPLEMENTATION: + ************************************************************************ + * FUNCTION: allocate_new_chunk() + * Aaron Stump, 6/8/99 + * + * ABSTRACT: This method allocates a new chunk of memory to use for + * allocating instances of THE_CLASS. + ************************************************************************ + * FUNCTION: new() + * Aaron Stump, 6/8/99 + * + * ABSTRACT: This allocator uses chunks for more efficient allocation. + ************************************************************************ + * FUNCTION: delete() + * Aaron Stump, 6/8/99 + * + * ABSTRACT: This delete() puts the chunk pointed to by ptr on the + * freelist. + ************************************************************************ + * Chunking_Memory_Management_Initializer and its static instance are used + * to call the static init_chunks() method for THE_CLASS. + ************************************************************************/ +#define C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_CC(THE_CLASS,THE_FIELD,THE_CHUNK_SIZE) \ +unsigned THE_CLASS::C_MACROS__CHUNK_SIZE = THE_CHUNK_SIZE;\ +\ +unsigned THE_CLASS::C_MACROS__BLOCK_SIZE = sizeof(THE_CLASS);\ +\ +void * THE_CLASS::C_MACROS__freelist = NULL;\ +char * THE_CLASS::C_MACROS__next_free_block = NULL;\ +char * THE_CLASS::C_MACROS__end_of_current_chunk = NULL;\ +bool THE_CLASS::C_MACROS__initialized = false;\ +\ +void \ +THE_CLASS::C_MACROS__allocate_new_chunk() {\ +\ + unsigned tmp = C_MACROS__CHUNK_SIZE * C_MACROS__BLOCK_SIZE;\ + char *chunk = (char *)malloc(tmp);\ + \ + assert (chunk != NULL); \ +\ + C_MACROS__next_free_block = chunk;\ + C_MACROS__end_of_current_chunk = chunk + tmp;\ +}\ +\ +void * \ +THE_CLASS::operator new(size_t size, void *h) {\ + (void)size; /* size should always be _BLOCK_SIZE */\ +\ + if (h != NULL)\ + /* we're being told what memory we should use */\ + return h;\ +\ + char *new_block;\ +\ + if (C_MACROS__freelist) {\ + /* we have a block on the freelist that we can use */\ + new_block = (char *)C_MACROS__freelist; \ + C_MACROS__freelist = (void *)((THE_CLASS *)new_block)->THE_FIELD; \ + }\ + else {\ + /* we have to get a new block from a chunk (which we may */\ + /* have to allocate*/\ + \ + if (C_MACROS__next_free_block == C_MACROS__end_of_current_chunk)\ + C_MACROS__allocate_new_chunk();\ + \ + new_block = C_MACROS__next_free_block;\ + C_MACROS__next_free_block += C_MACROS__BLOCK_SIZE;\ + }\ + \ + return new_block;\ +}\ +\ +void \ +THE_CLASS::operator delete(void *ptr) {\ + void **f = (void **)&((THE_CLASS *)ptr)->THE_FIELD; \ + *f = C_MACROS__freelist; \ + C_MACROS__freelist = ptr; \ +} + +#endif + diff --git a/proofs/lfsc_checker/code.cpp b/proofs/lfsc_checker/code.cpp new file mode 100644 index 000000000..225700580 --- /dev/null +++ b/proofs/lfsc_checker/code.cpp @@ -0,0 +1,1377 @@ +#include "check.h" +#include "code.h" +#include + +#include "scccode.h" + +using namespace std; + +string *eat_str(const char *str, bool check_end = true) { + string *s = new string(); + char c, d; + while ((c = *str++)) { + d = our_getc(); + if (c != d) { + our_ungetc(d); + return s; + } + s->push_back(d); + } + + if (check_end && + (d = our_getc()) != ' ' && d != '(' && d != '\n' && d != '\t') { + our_ungetc(d); + return s; + } + + delete s; + return 0; +} + +SymSExpr *read_ctor() { + string id(prefix_id()); +#ifdef USE_HASH_TABLES + Expr *s = symbols[id]; + Expr *stp = symbol_types[id]; +#else + pair p = symbols->get(id.c_str()); + Expr *s = p.first; + Expr *stp = p.second; +#endif + + if (!stp) + report_error("Undeclared identifier parsing a pattern."); + + if (s->getclass() != SYMS_EXPR || ((SymExpr *)s)->val) + report_error("The head of a pattern is not a constructor."); + + s->inc(); + + return (SymSExpr *)s; +} + +Expr *read_case() { + eat_char('('); + Expr *pat = NULL; + vector vars; + +#ifdef USE_HASH_MAPS + vectorprevs; +#else + vector >prevs; +#endif + char d = non_ws(); + switch(d) { + case '(': { + // parse application + SymSExpr *s = read_ctor(); + pat = s; + char c; + while ((c = non_ws()) != ')') { + our_ungetc(c); + string varstr(prefix_id()); + SymSExpr *var = new SymSExpr(varstr); + vars.push_back(var); +#ifdef USE_HASH_MAPS + prevs.push_back(symbols[varstr]); + symbols[varstr] = var; +#else + prevs.push_back(symbols->insert(varstr.c_str(), + pair(var,NULL))); +#endif +#ifndef USE_FLAT_APP + pat = new CExpr(APP,pat,var); +#else + pat = Expr::make_app(pat,var); +#endif + } + break; + } + // default case + case 'd': { + delete eat_str("efault"); + } + break; + case EOF: + report_error("Unexpected end of file parsing a pattern."); + break; + default: + // could be an identifier + our_ungetc(d); + pat = read_ctor(); + break; + } + + Expr *ret = read_code(); + if( pat ) + ret = new CExpr(CASE, pat, ret); + + for (int i = 0, iend = prevs.size(); i < iend; i++) { + string &s = vars[i]->s; +#ifdef USE_HASH_MAPS + symbols[s] = prevs[i]; +#else + symbols->insert(s.c_str(), prevs[i]); +#endif + } + + eat_char(')'); + + return ret; +} + +Expr *read_code() { + string *pref = NULL; + char d = non_ws(); + switch(d) { + case '(': + { + char c = non_ws(); + switch (c) + { + case 'd': + { + our_ungetc('d'); + pref = eat_str("do"); + if (pref) + break; + Expr *ret = read_code(); + while ((c = non_ws()) != ')') { + our_ungetc(c); + ret = new CExpr(DO,ret,read_code()); + } + return ret; + } + case 'f': + { + our_ungetc('f'); + pref = eat_str("fail"); + if (pref) + break; + + Expr *c = read_code(); + eat_char(')'); + + //do we need to check this??? + //if (c->getclass() != SYMS_EXPR || ((SymExpr *)c)->val) + // report_error(string("\"fail\" must be used with a (undefined) base ") + // +string("type.\n1. the expression used: "+c->toString())); + + return new CExpr(FAIL, c); + } + case 'l': + { + our_ungetc('l'); + pref = eat_str("let"); + if (pref) + break; + + string id(prefix_id()); + SymSExpr *var = new SymSExpr(id); + + Expr *t1 = read_code(); + +#ifdef USE_HASH_MAPS + Expr *prev = symbols[id]; + symbols[id] = var; +#else + pair prev = + symbols->insert(id.c_str(), pair(var,NULL)); +#endif + + Expr *t2 = read_code(); + +#ifdef USE_HASH_MAPS + symbols[id] = prev; +#else + symbols->insert(id.c_str(), prev); +#endif + eat_char(')'); + return new CExpr(LET, var, t1, t2); + } + case 'i': + { + our_ungetc('i'); + pref = eat_str("ifmarked",false); + if (pref) + break; +#ifndef MARKVAR_32 + Expr *e1 = read_code(); + Expr *e2 = read_code(); + Expr *e3 = read_code(); + Expr *ret = new CExpr(IFMARKED, e1, e2, e3); +#else + int index = read_index(); + Expr *e1 = read_code(); + Expr *e2 = read_code(); + Expr *e3 = read_code(); + Expr *ret = NULL; + if( index>=1 && index<=32 ) + { + ret = new CExpr( IFMARKED, new IntExpr( index-1 ), e1, e2, e3 ); + } + else + { + std::cout << "Can't make IFMARKED with index = " << index << std::endl; + } + Expr::markedCount++; + //Expr *ret = new CExpr(IFMARKED, e1, e2, e3); +#endif + eat_char(')'); + return ret; + } + case 'm': + { + char c; + switch ((c = our_getc())) + { + case 'a': + { + char cc; + switch ((cc = our_getc())) { + case 't': + { + our_ungetc('t'); + pref = eat_str("tch"); + if (pref) { + pref->insert(0,"ma"); + break; + } + vector cases; + cases.push_back(read_code()); // the scrutinee + while ((c = non_ws()) != ')' && c != 'd') { + our_ungetc(c); + cases.push_back(read_case()); + } + if (cases.size() == 1) // counting scrutinee + report_error("A match has no cases."); + if (c == 'd') { + // we have a default case + //delete eat_str("efault"); + our_ungetc(c); + cases.push_back(read_case()); + } + return new CExpr(MATCH,cases); + } + case 'r': + { + our_ungetc('r'); + pref = eat_str("rkvar", false); + if (pref) { + pref->insert(0,"ma"); + break; + } + #ifndef MARKVAR_32 + Expr *ret = new CExpr(MARKVAR,read_code()); + #else + int index = read_index(); + CExpr* ret = NULL; + if( index>=1 && index<=32 ) + { + ret = new CExpr( MARKVAR, new IntExpr( index-1 ), read_code() ); + } + else + { + std::cout << "Can't make MARKVAR with index = " << index << std::endl; + } + Expr::markedCount++; + //Expr *ret = new CExpr(MARKVAR,read_code()); + #endif + + eat_char(')'); + return ret; + } + default: + our_ungetc(c); + pref = new string("ma"); + break; + } + } + case 'p': + { + our_ungetc('p'); + pref = eat_str("p_",false); + if (pref) { + pref->insert(0,"m"); + break; + } + char c = our_getc(); + switch(c) { + case 'a': + { + our_ungetc('a'); + pref = eat_str("add"); + if (pref) { + pref->insert(0,"mp_"); + break; + } + Expr* e1 = read_code(); + Expr* e2 = read_code(); + Expr *ret = new CExpr(ADD, e1, e2); + eat_char(')'); + return ret; + } + case 'n': + { + our_ungetc('n'); + pref = eat_str("neg"); + if (pref) { + pref->insert(0,"mp_"); + break; + } + + Expr *ret = new CExpr(NEG, read_code()); + eat_char(')'); + return ret; + } + case 'i': + { // mpz_if_neg + char c = our_getc(); + if( c=='f' ) + { + c = our_getc(); + switch( c ) + { + case 'n': { + our_ungetc('n'); + pref = eat_str("neg"); + if( pref ) { + pref->insert(0,"mp_if"); + break; + } + Expr* e1 = read_code(); + Expr* e2 = read_code(); + Expr* e3 = read_code(); + Expr* ret = new CExpr(IFNEG, e1, e2, e3 ); + eat_char(')'); + return ret; + } + case 'z': { + our_ungetc('z'); + pref = eat_str("zero"); + if( pref ) { + pref->insert(0,"mp_if"); + break; + } + Expr* e1 = read_code(); + Expr* e2 = read_code(); + Expr* e3 = read_code(); + Expr* ret = new CExpr(IFZERO, e1, e2, e3 ); + eat_char(')'); + return ret; + } + default: + our_ungetc(c); + pref = new string("mp_if"); + break; + } + } + else + { + our_ungetc(c); + pref = new string("mp_i"); + break; + } + } + case 'm': + { + our_ungetc('m'); + pref = eat_str("mul"); + if( pref ){ + pref->insert(0,"mp_"); + break; + } + Expr* e1 = read_code(); + Expr* e2 = read_code(); + Expr* ret = new CExpr(MUL, e1, e2 ); + eat_char(')'); + return ret; + } + case 'd': + { + our_ungetc('d'); + pref = eat_str("div"); + if( pref ){ + pref->insert(0,"mp_"); + break; + } + Expr* e1 = read_code(); + Expr* e2 = read_code(); + Expr* ret = new CExpr(DIV, e1, e2 ); + eat_char(')'); + return ret; + } + default: + our_ungetc(c); + pref = new string("mp_"); + break; + } + } + default: + our_ungetc(c); + pref = new string("m"); + break; + } + break; + } + case '~': { + Expr *e = read_code(); + if( e->getclass()==INT_EXPR ) + { + IntExpr *ee = (IntExpr *)e; + mpz_neg(ee->n, ee->n); + eat_char(')'); + return ee; + } + else if( e->getclass() == RAT_EXPR ) + { + RatExpr *ee = (RatExpr *)e; + mpq_neg(ee->n, ee->n); + eat_char(')'); + return ee; + } + else + { + report_error("Negative sign with expr that is not an int. literal."); + } + } + case 'c': + { + our_ungetc('c'); + pref = eat_str("compare"); + if (pref) + break; + Expr *e1 = read_code(); + Expr *e2 = read_code(); + Expr *e3 = read_code(); + Expr *e4 = read_code(); + eat_char(')'); + return new CExpr(COMPARE, e1, e2, e3, e4); + } + break; + case EOF: + report_error("Unexpected end of file."); + break; + default: + { // the application case + our_ungetc(c); + break; + } + } + // parse application + if (pref) + // we have eaten part of the name of an applied identifier + pref->append(prefix_id()); + else + pref = new string(prefix_id()); + + Expr *ret = progs[*pref]; + if (!ret) +#ifdef USE_HASH_TABLES + ret = symbols[*pref]; +#else + ret = symbols->get(pref->c_str()).first; +#endif + + if (!ret) + report_error(string("Undeclared identifier at head of an application: ") + +*pref); + + ret->inc(); + delete pref; + + while ((c = non_ws()) != ')') { + our_ungetc(c); +#ifndef USE_FLAT_APP + ret = new CExpr(APP,ret,read_code()); +#else + Expr* ke = read_code(); + ret = Expr::make_app(ret,ke); +#endif + } + return ret; + } // end case '(' + case EOF: + report_error("Unexpected end of file."); + break; + case '_': + report_error("Holes may not be used in code."); + return NULL; + case '0': + case '1': + case '2': + case '3': + case '4': + case '5': + case '6': + case '7': + case '8': + case '9': + { + our_ungetc(d); + string v; + char c; + while (isdigit(c = our_getc())) + v.push_back(c); + bool parseMpq = false; + if( c=='/' ) + { + parseMpq = true; + v.push_back(c); + while(isdigit(c = our_getc())) + v.push_back(c); + } + our_ungetc(c); + if( parseMpq ) + { + mpq_t num; + mpq_init(num); + if (mpq_set_str(num,v.c_str(),10) == -1 ) + report_error("Error reading a mpq numeral."); + + Expr* e = new RatExpr( num ); + return e; + } + else + { + mpz_t num; + if (mpz_init_set_str(num,v.c_str(),10) == -1) + report_error("Error reading a numeral."); + return new IntExpr(num); + } + } + default: + { + our_ungetc(d); + string id(prefix_id()); +#ifdef USE_HASH_MAPS + Expr *ret = symbols[id]; +#else + pair p = symbols->get(id.c_str()); + Expr *ret = p.first; +#endif + if (!ret) + ret = progs[id]; + if (!ret) + report_error(string("Undeclared identifier: ")+id); + ret->inc(); + return ret; + } + } + report_error("Unexpected operator in a piece of code."); + return 0; +} + +// the input is owned by the caller, the output by us (so do not dec it). +Expr *check_code(Expr *_e) { + CExpr *e = (CExpr *)_e; + switch (e->getop()) { + case NOT_CEXPR: + switch (e->getclass()) { + case INT_EXPR: + return statMpz; + case RAT_EXPR: + return statMpq; + case SYM_EXPR: { + report_error("Internal error: an LF variable is encountered in code"); + break; + } + case SYMS_EXPR: { +#ifdef USE_HASH_MAPS + Expr *tp = symbol_types[((SymSExpr *)e)->s]; +#else + Expr *tp = symbols->get(((SymSExpr *)e)->s.c_str()).second; +#endif + if (!tp) + report_error(string("A symbol is missing a type in a piece of code.") + +string("\n1. the symbol: ")+((SymSExpr *)e)->s); + return tp; + } + case HOLE_EXPR: + report_error("Encountered a hole unexpectedly in code."); + default: + report_error("Unrecognized form of expr in code."); + } + case APP: { +#ifdef USE_FLAT_APP + Expr* h = e->kids[0]->followDefs(); + vector argtps; + int counter = 1; + while( e->kids[counter] ) + { + argtps.push_back( check_code( e->kids[counter] ) ); + counter++; + } + int iend = counter-1; +#else + vector args; + Expr *h = (Expr *)e->collect_args(args); + + int iend = args.size(); + vector argtps(iend); + for (int i = 0; i < iend; i++) + argtps[i] = check_code(args[i]); +#endif + + Expr *tp = NULL; + if (h->getop() == PROG){ + tp = ((CExpr *)h)->kids[0]; + }else { +#ifdef USE_HASH_MAPS + tp = symbol_types[((SymSExpr *)h)->s]; +#else + tp = symbols->get(((SymSExpr *)h)->s.c_str()).second; +#endif + } + + if (!tp) + report_error(string("The head of an application is missing a type in ") + +string("code.\n1. the application: ")+e->toString()); + + tp = tp->followDefs(); + + if (tp->getop() != PI) + report_error(string("The head of an application does not have ") + +string("functional type in code.") + +string("\n1. the application: ")+e->toString()); + + CExpr *cur = (CExpr *)tp; + int i = 0; + while (cur->getop() == PI) { + if (i >= iend) + report_error(string("A function is not being fully applied in code.\n") + +string("1. the application: ")+e->toString() + +string("\n2. its (functional) type: ")+cur->toString()); + if( argtps[i]->getop()==APP ) + argtps[i] = ((CExpr*)argtps[i])->kids[0]; + if (argtps[i] != cur->kids[1]) { + char buf[1024]; + sprintf(buf,"%d",i); + report_error(string("Type mismatch for argument ") + + string(buf) + + string(" in application in code.\n") + + string("1. the application: ")+e->toString() + + string("\n2. the head's type: ")+tp->toString() +#ifdef USE_FLAT_APP + + string("\n3. the argument: ")+e->kids[i+1]->toString() +#else + + string("\n3. the argument: ")+args[i]->toString() +#endif + + string("\n4. computed type: ")+argtps[i]->toString() + + string("\n5. expected type: ") + +cur->kids[1]->toString()); + } + + //if (cur->kids[2]->free_in((SymExpr *)cur->kids[0])) + if( cur->get_free_in() ){ + cur->calc_free_in(); + //are you sure? + if( cur->get_free_in() ) + report_error(string("A dependently typed function is being applied in") + +string(" code.\n1. the application: ")+e->toString() + +string("\n2. the head's type: ")+tp->toString()); + //ok, reset the mark + cur->setexmark(); + } + + i++; + cur = (CExpr *)cur->kids[2]; + } + if (i < iend) + report_error(string("A function is being fully applied to too many ") + +string("arguments in code.\n") + +string("1. the application: ")+e->toString() + +string("\n2. the head's type: ")+tp->toString()); + + + return cur; + } + //is this right? + case MPZ: + return statType; + break; + case MPQ: + return statType; + break; + case DO: + check_code(e->kids[0]); + return check_code(e->kids[1]); + + case LET: { + SymSExpr * var = (SymSExpr *)e->kids[0]; + + Expr *tp1 = check_code(e->kids[1]); + +#ifdef USE_HASH_MAPS + Expr *prevtp = symbol_types[var->s]; + symbol_types[var->s] = tp1; +#else + pair prev = + symbols->insert(var->s.c_str(), pair(NULL,tp1)); +#endif + + Expr *tp2 = check_code(e->kids[2]); + +#ifdef USE_HASH_MAPS + symbol_types[var->s] = prevtp; +#else + symbols->insert(var->s.c_str(), prev); +#endif + + return tp2; + } + + case ADD: + case MUL: + case DIV: + { + Expr *tp0 = check_code(e->kids[0]); + Expr *tp1 = check_code(e->kids[1]); + + if (tp0 != statMpz && tp0 != statMpq ) + report_error(string("Argument to mp_[arith] does not have type \"mpz\" or \"mpq\".\n") + +string("1. the argument: ")+e->kids[0]->toString() + +string("\n1. its type: ")+tp0->toString()); + + if (tp0 != tp1) + report_error(string("Arguments to mp_[arith] have differing types.\n") + +string("1. argument 1: ")+e->kids[0]->toString() + +string("\n1. its type: ")+tp0->toString() + +string("2. argument 2: ")+e->kids[1]->toString() + +string("\n2. its type: ")+tp1->toString()); + + return tp0; + } + + case NEG: { + Expr *tp0 = check_code(e->kids[0]); + if (tp0 != statMpz && tp0 != statMpq ) + report_error(string("Argument to mp_neg does not have type \"mpz\" or \"mpq\".\n") + +string("1. the argument: ")+e->kids[0]->toString() + +string("\n1. its type: ")+tp0->toString()); + + return tp0; + } + + case IFNEG: + case IFZERO: { + Expr *tp0 = check_code(e->kids[0]); + if (tp0 != statMpz && tp0 != statMpq) + report_error(string("Argument to mp_if does not have type \"mpz\" or \"mpq\".\n") + +string("1. the argument: ")+e->kids[0]->toString() + +string("\n1. its type: ")+tp0->toString()); + + SymSExpr *tp1 = (SymSExpr *)check_code(e->kids[1]); + SymSExpr *tp2 = (SymSExpr *)check_code(e->kids[2]); + if (tp1->getclass() != SYMS_EXPR || tp1->val || tp1 != tp2) + report_error(string("\"mp_if\" used with expressions that do not ") + +string("have equal simple datatypes\nfor their types.\n") + +string("0. 0'th expression: ")+e->kids[0]->toString() + +string("\n1. first expression: ")+e->kids[1]->toString() + +string("\n2. second expression: ")+e->kids[2]->toString() + +string("\n3. first expression's type: ")+tp1->toString() + +string("\n4. second expression's type: ")+tp2->toString()); + return tp1; + } + + case FAIL: { + Expr *tp = check_code(e->kids[0]); + if (tp != statType) + report_error(string("\"fail\" is used with an expression which is ") + +string("not a type.\n1. the expression :") + +e->kids[0]->toString() + +string("\n2. its type: ")+tp->toString()); + return e->kids[0]; + } + case MARKVAR: { + SymSExpr *tp = (SymSExpr *)check_code(e->kids[1]); + + Expr* tptp = NULL; + + if (tp->getclass() == SYMS_EXPR && !tp->val){ +#ifdef USE_HASH_MAPS + tptp = symbol_types[tp->s]; +#else + tptp = symbols->get(tp->s.c_str()).second; +#endif + } + + if (!tptp->isType( statType )){ + string errstr = (string("\"markvar\" is used with an expression which ") + +string("cannot be a lambda-bound variable.\n") + +string("1. the expression :") + +e->kids[1]->toString() + +string("\n2. its type: ")+tp->toString()); + report_error(errstr); + } + + return tp; + } + + case IFMARKED: + { + SymSExpr *tp = (SymSExpr *)check_code(e->kids[1]); + + Expr* tptp = NULL; + + if (tp->getclass() == SYMS_EXPR && !tp->val){ +#ifdef USE_HASH_MAPS + tptp = symbol_types[tp->s]; +#else + tptp = symbols->get(tp->s.c_str()).second; +#endif + } + + if (!tptp->isType( statType ) ){ + string errstr = (string("\"ifmarked\" is used with an expression which ") + +string("cannot be a lambda-bound variable.\n") + +string("1. the expression :") + +e->kids[1]->toString() + +string("\n2. its type: ")+tp->toString()); + report_error(errstr); + } + + SymSExpr *tp1 = (SymSExpr *)check_code(e->kids[2]); + SymSExpr *tp2 = (SymSExpr *)check_code(e->kids[3]); + if (tp1->getclass() != SYMS_EXPR || tp1->val || tp1 != tp2) + report_error(string("\"ifmarked\" used with expressions that do not ") + +string("have equal simple datatypes\nfor their types.\n") + +string("0. 0'th expression: ")+e->kids[1]->toString() + +string("\n1. first expression: ")+e->kids[2]->toString() + +string("\n2. second expression: ")+e->kids[3]->toString() + +string("\n3. first expression's type: ")+tp1->toString() + +string("\n4. second expression's type: ")+tp2->toString()); + return tp1; + } + case COMPARE: + { + SymSExpr *tp0 = (SymSExpr *)check_code(e->kids[0]); + if (tp0->getclass() != SYMS_EXPR || tp0->val){ + string errstr0 = (string("\"compare\" is used with a first expression which ") + +string("cannot be a lambda-bound variable.\n") + +string("1. the expression :") + +e->kids[0]->toString() + +string("\n2. its type: ")+tp0->toString()); + report_error(errstr0); + } + + SymSExpr *tp1 = (SymSExpr *)check_code(e->kids[1]); + + if (tp1->getclass() != SYMS_EXPR || tp1->val){ + string errstr1 = (string("\"compare\" is used with a second expression which ") + +string("cannot be a lambda-bound variable.\n") + +string("1. the expression :") + +e->kids[1]->toString() + +string("\n2. its type: ")+tp1->toString()); + report_error(errstr1); + } + + SymSExpr *tp2 = (SymSExpr *)check_code(e->kids[2]); + SymSExpr *tp3 = (SymSExpr *)check_code(e->kids[3]); + if (tp2->getclass() != SYMS_EXPR || tp2->val || tp2 != tp3) + report_error(string("\"compare\" used with expressions that do not ") + +string("have equal simple datatypes\nfor their types.\n") + +string("\n1. first expression: ")+e->kids[2]->toString() + +string("\n2. second expression: ")+e->kids[3]->toString() + +string("\n3. first expression's type: ")+tp2->toString() + +string("\n4. second expression's type: ")+tp3->toString()); + return tp2; + } + case MATCH: + { + SymSExpr *scruttp = (SymSExpr *)check_code(e->kids[0]); + Expr *tptp = NULL; + if (scruttp->getclass() == SYMS_EXPR && !scruttp->val){ +#ifdef USE_HASH_MAPS + tptp = symbol_types[scruttp->s]; +#else + tptp = symbols->get(scruttp->s.c_str()).second; +#endif + } + if (!tptp->isType( statType )){ + string errstr = (string("The scrutinee of a match is not ") + +string("a plain piece of data.\n") + +string("1. the scrutinee: ") + +e->kids[0]->toString() + +string("\n2. its type: ")+scruttp->toString()); + report_error(errstr); + } + + int i = 1; + Expr **cur = &e->kids[i]; + Expr *mtp = NULL; + Expr *c_or_default; + CExpr *c; + while ((c_or_default = *cur++)) { + Expr *tp = NULL; + CExpr *pat = NULL; + if (c_or_default->getop() != CASE) + // this is the default of the MATCH + tp = check_code(c_or_default); + else { + // this is a CASE of the MATCH + c = (CExpr *)c_or_default; + pat = (CExpr *)c->kids[0]; // might be just a SYMS_EXPR + if (pat->getclass() == SYMS_EXPR) + tp = check_code(c->kids[1]); + else { + // extend type context and then check the body of the case +#ifdef USE_HASH_MAPS + vectorprevs; +#else + vector >prevs; +#endif + vector vars; + SymSExpr *ctor = (SymSExpr *)pat->collect_args(vars); +#ifdef USE_HASH_MAPS + CExpr *ctortp = (CExpr *)symbol_types[ctor->s]; +#else + CExpr *ctortp = (CExpr *)symbols->get(ctor->s.c_str()).second; +#endif + CExpr *curtp = ctortp; + for (int i = 0, iend = vars.size(); i < iend; i++) { + if ( curtp->followDefs()->getop() != PI) + report_error(string("Too many arguments to a constructor in") + +string(" a pattern.\n1. the pattern: ") + +pat->toString() + +string("\n2. the head's type: " + +ctortp->toString())); +#ifdef USE_HASH_MAPS + prevs.push_back(symbol_types[((SymSExpr *)vars[i])->s]); + symbol_types[((SymSExpr *)vars[i])] = curtp->followDefs()->kids[1]; +#else + prevs.push_back + (symbols->insert(((SymSExpr *)vars[i])->s.c_str(), + pair(NULL, + ((CExpr *)(curtp->followDefs()))->kids[1]))); +#endif + curtp = (CExpr *)((CExpr *)(curtp->followDefs()))->kids[2]; + } + + tp = check_code(c->kids[1]); + + for (int i = 0, iend = prevs.size(); i < iend; i++) { +#ifdef USE_HASH_MAPS + symbol_types[((SymSExpr *)vars[i])->s] = prevs[i]; +#else + symbols->insert(((SymSExpr *)vars[i])->s.c_str(), prevs[i]); +#endif + } + } + } + + // check that the type for the body of this case -- or the default value -- + // matches the type for the previous case if we had one. + + if (!mtp) + mtp = tp; + else + if (mtp != tp) + report_error(string("Types for bodies of match cases or the default differ.") + +string("\n1. type for first case's body: ") + +mtp->toString() + +(pat == NULL ? string("\n2. type for the default") + : (string("\n2. type for the body of case for ") + +pat->toString())) + +string(": ")+tp->toString()); + + } + + return mtp; + } + } // end switch + + report_error("Type checking an unrecognized form of code (internal error)."); + return NULL; +} + +bool dbg_prog; +bool run_scc; +int dbg_prog_indent_lvl = 0; + +void dbg_prog_indent(std::ostream &os) { + for (int i = 0; i < dbg_prog_indent_lvl; i++) + os << " "; +} + +Expr *run_code(Expr *_e) { + start_run_code: + CExpr *e = (CExpr *)_e; + if( e ) + { + //std::cout << ". "; + //e->print( std::cout ); + //std::cout << std::endl; + //std::cout << e->getop() << " " << e->getclass() << std::endl; + } + switch (e->getop()) { + case NOT_CEXPR: + switch(e->getclass()) { + case INT_EXPR: + case RAT_EXPR: + e->inc(); + return e; + case HOLE_EXPR: { + Expr *tmp = e->followDefs(); + if (tmp == e) + report_error("Encountered an unfilled hole running code."); + tmp->inc(); + return tmp; + } + case SYMS_EXPR: + case SYM_EXPR: { + Expr *tmp = e->followDefs(); + //std::cout << "follow def = "; + //tmp->print( std::cout ); + //std::cout << std::endl; + if (tmp == e) { + e->inc(); + return e; + } + tmp->inc(); + return tmp; + } + } + case FAIL: + return NULL; + case DO: { + Expr *tmp = run_code(e->kids[0]); + if (!tmp) + return NULL; + tmp->dec(); + _e = e->kids[1]; + goto start_run_code; + } + case LET: { + Expr *r0 = run_code(e->kids[1]); + if (!r0) + return NULL; + SymExpr *var = (SymExpr *)e->kids[0]; + Expr *prev = var->val; + var->val = r0; + Expr *r1 = run_code(e->kids[2]); + var->val = prev; + r0->dec(); + return r1; + } + case ADD: + case MUL: + case DIV: + { + Expr *r1 = run_code(e->kids[0]); + if (!r1) + return NULL; + Expr *r2 = run_code(e->kids[1]); + if (!r2) + return NULL; + if( r1->getclass()==INT_EXPR && r2->getclass()==INT_EXPR ) + { + mpz_t r; + mpz_init(r); + if( e->getop()==ADD ) + mpz_add(r, ((IntExpr *)r1)->n, ((IntExpr *)r2)->n); + else if( e->getop()==MUL ) + mpz_mul(r, ((IntExpr *)r1)->n, ((IntExpr *)r2)->n); + else if( e->getop()==DIV ) + mpz_cdiv_q(r, ((IntExpr *)r1)->n, ((IntExpr *)r2)->n); + r1->dec(); + r2->dec(); + return new IntExpr(r); + } + else if( r1->getclass()==RAT_EXPR && r2->getclass()==RAT_EXPR ) + { + mpq_t q; + mpq_init(q); + if( e->getop()==ADD ) + mpq_add(q, ((RatExpr *)r1)->n, ((RatExpr *)r2)->n); + else if( e->getop()==MUL ) + mpq_mul(q, ((RatExpr *)r1)->n, ((RatExpr *)r2)->n); + else if( e->getop()==DIV ) + mpq_div(q, ((RatExpr *)r1)->n, ((RatExpr *)r2)->n); + r1->dec(); + r2->dec(); + return new RatExpr(q); + } + else + { + //std::cout << "An arithmetic operation failed. " << r1->getclass() << " " << r2->getclass() << std::endl; + r1->dec(); + r2->dec(); + return NULL; + } + } + case NEG: { + Expr *r1 = run_code(e->kids[0]); + if (!r1) + return NULL; + if (r1->getclass() == INT_EXPR) { + mpz_t r; + mpz_init(r); + mpz_neg(r, ((IntExpr *)r1)->n); + r1->dec(); + return new IntExpr(r); + } + else if( r1->getclass() == RAT_EXPR ) { + mpq_t q; + mpq_init(q); + mpq_neg(q, ((RatExpr *)r1)->n); + r1->dec(); + return new RatExpr(q); + } + else + { + std::cout << "An arithmetic negation failed. " << r1->getclass() << std::endl; + //((SymSExpr*)r1)->val->print( std::cout ); + std::cout << ((SymSExpr*)r1)->val << std::endl; + r1->dec(); + return NULL; + } + } + case IFNEG: + case IFZERO:{ + Expr *r1 = run_code(e->kids[0]); + if (!r1) + return NULL; + + bool cond; + if( r1->getclass() == INT_EXPR ){ + if( e->getop() == IFNEG ) + cond = mpz_sgn( ((IntExpr *)r1)->n )<0; + else if( e->getop() == IFZERO ) + cond = mpz_sgn( ((IntExpr *)r1)->n )==0; + }else if( r1->getclass() == RAT_EXPR ){ + if( e->getop() == IFNEG ) + cond = mpq_sgn( ((RatExpr *)r1)->n )<0; + else if( e->getop() == IFZERO ) + cond = mpq_sgn( ((RatExpr *)r1)->n )==0; + } + else + { + std::cout << "An arithmetic if-expression failed. " << r1->getclass() << std::endl; + r1->dec(); + return NULL; + } + r1->dec(); + + + if( cond ) + _e = e->kids[1]; + else + _e = e->kids[2]; + goto start_run_code; + } + case IFMARKED: { + Expr *r1 = run_code(e->kids[1]); + if (!r1) + return NULL; + if(r1->getclass() != SYM_EXPR && r1->getclass() != SYMS_EXPR ){ + r1->dec(); + return NULL; + } +#ifndef MARKVAR_32 + if (r1->getexmark()) { +#else + if(((SymExpr*)r1)->getmark( ((IntExpr*)e->kids[0])->get_num() ) ){ +#endif + r1->dec(); + _e = e->kids[2]; + goto start_run_code; + } + // else + r1->dec(); + _e = e->kids[3]; + goto start_run_code; + } + case COMPARE: + { + Expr *r1 = run_code(e->kids[0]); + if (!r1) + return NULL; + if (r1->getclass() != SYM_EXPR && r1->getclass() != SYMS_EXPR) { + r1->dec(); + return NULL; + } + Expr *r2 = run_code(e->kids[1]); + if (!r2) + return NULL; + if (r2->getclass() != SYM_EXPR && r2->getclass() != SYMS_EXPR) { + r2->dec(); + return NULL; + } + if( r1dec(); + _e = e->kids[2]; + goto start_run_code; + } + //else + r2->dec(); + _e = e->kids[3]; + goto start_run_code; + } + case MARKVAR: { + Expr *r1 = run_code(e->kids[1]); + if (!r1) + return NULL; + if (r1->getclass() != SYM_EXPR && r1->getclass() != SYMS_EXPR) { + r1->dec(); + return NULL; + } +#ifndef MARKVAR_32 + if (r1->getexmark()) + r1->clearexmark(); + else + r1->setexmark(); +#else + if(((SymExpr*)r1)->getmark( ((IntExpr*)e->kids[0])->get_num() ) ) + ((SymExpr*)r1)->clearmark( ((IntExpr*)e->kids[0])->get_num() ); + else + ((SymExpr*)r1)->setmark( ((IntExpr*)e->kids[0])->get_num() ); +#endif + return r1; + } + case MATCH: { + Expr *scrut = run_code(e->kids[0]); + if (!scrut) + return 0; + vector args; + Expr *hd = scrut->collect_args(args); + Expr **cases = &e->kids[1]; + CExpr *c; + Expr *c_or_default; + while ((c_or_default = *cases++)) { + + if (c_or_default->getop() != CASE){ + //std::cout << "run the default " << std::endl; + //c_or_default->print( std::cout ); + // this is the default of the MATCH + return run_code(c_or_default); + } + + // this is a CASE of the MATCH + CExpr *c = (CExpr *)c_or_default; + Expr *p = c->kids[0]; + if (hd == p->get_head()) { + vector vars; + p->collect_args(vars); + int jend = args.size(); + vector old_vals(jend); + for (int j = 0; j < jend; j++) { + SymExpr *var = (SymExpr *)vars[j]; + old_vals[j] = var->val; + var->val = args[j]; + args[j]->inc(); + } + scrut->dec(); + Expr *ret = run_code(c->kids[1] /* the body of the case */); + for (int j = 0; j < jend; j++) { + ((SymExpr *)vars[j])->val = old_vals[j]; + args[j]->dec(); + } + return ret; + } + } + break; + } + case APP: { + Expr *tmp = e->whr(); + if (e != tmp) { + _e = tmp; + goto start_run_code; + } + + // e is in weak head normal form + + vector args; + Expr *hd = e->collect_args(args); + for (int i = 0, iend = args.size(); i < iend; i++) + if (!(args[i] = run_code(args[i]))) { + for (int j = 0; j < i; j++) + args[j]->dec(); + return NULL; + } + if (hd->getop() != PROG) { + hd->inc(); + Expr *tmp = Expr::build_app(hd,args); + return tmp; + } + + CExpr *prog = (CExpr *)hd; + Expr **cur = ((CExpr *)prog->kids[1])->kids; + vector old_vals; + SymExpr *var; + int i = 0; + + if( run_scc && e->get_head( false )->getclass()==SYMS_EXPR ) + { + //std::cout << "running " << ((SymSExpr*)e->get_head( false ))->s.c_str() << " with " << (int)args.size() << " arguments" << std::endl; +//#ifndef USE_FLAT_APP +// for( int a=0; a<(int)args.size(); a++ ) +// { +// args[a] = CExpr::convert_to_flat_app( args[a] ); +// } +//#endif + Expr *ret = run_compiled_scc( e->get_head( false ), args ); + for (int i = 0, iend = args.size(); i < iend; i++) { + args[i]->dec(); + } +//#ifndef USE_FLAT_APP +// ret = CExpr::convert_to_tree_app( ret ); +//#endif + //ret->inc(); + return ret; + } + else + { + while((var = (SymExpr *)*cur++)) { + old_vals.push_back(var->val); + var->val = args[i++]; + } + + if (dbg_prog) { + dbg_prog_indent(cout); + cout << "["; + e->print(cout); + cout << "\n"; + } + dbg_prog_indent_lvl++; + + Expr *ret = run_code(prog->kids[2]); + + dbg_prog_indent_lvl--; + if (dbg_prog) { + dbg_prog_indent(cout); + cout << "= "; + if (ret) + ret->print(cout); + else + cout << "fail"; + cout << "]\n"; + } + + cur = ((CExpr *)prog->kids[1])->kids; + i = 0; + while((var = (SymExpr *)*cur++)) { + args[i]->dec(); + var->val = old_vals[i++]; + } + return ret; + } + } + } // end switch + return NULL; +} + +int read_index() +{ + int index = 1; + string v; + char c; + while (isdigit(c = our_getc())) + v.push_back(c); + our_ungetc(c); + if( v.length()>0 ) + { + index = atoi( v.c_str() ); + } + return index; +} \ No newline at end of file diff --git a/proofs/lfsc_checker/code.h b/proofs/lfsc_checker/code.h new file mode 100644 index 000000000..9d00a6378 --- /dev/null +++ b/proofs/lfsc_checker/code.h @@ -0,0 +1,15 @@ +#ifndef SC2_CODE_H +#define SC2_CODE_H + +#include "expr.h" + +Expr *read_code(); +Expr *check_code(Expr *); // compute the type for the given code +Expr *run_code(Expr *); + +int read_index(); + +extern bool dbg_prog; +extern bool run_scc; + +#endif diff --git a/proofs/lfsc_checker/configure.ac b/proofs/lfsc_checker/configure.ac new file mode 100644 index 000000000..245b0ea65 --- /dev/null +++ b/proofs/lfsc_checker/configure.ac @@ -0,0 +1,47 @@ +# -*- Autoconf -*- +# Process this file with autoconf to produce a configure script. + +AC_PREREQ([2.68]) +AC_INIT([lfsc-checker], [1.0], [cvc-bugs@cs.nyu.edu]) +AC_CONFIG_SRCDIR([libwriter.h]) +AC_CONFIG_AUX_DIR([config]) +AC_CONFIG_MACRO_DIR([config]) +AC_CONFIG_HEADERS([config.h]) +AM_INIT_AUTOMAKE([1.11 foreign no-define tar-pax]) +LT_INIT + +AC_CANONICAL_BUILD +AC_CANONICAL_HOST +AC_CANONICAL_TARGET + +m4_ifdef([AM_SILENT_RULES],[AM_SILENT_RULES([yes])]) + +# on by default +AM_MAINTAINER_MODE([enable]) + +# turn off static lib building by default +AC_ENABLE_SHARED +AC_DISABLE_STATIC + +# Checks for programs. +AC_PROG_CXX +AC_PROG_CC + +# Checks for libraries. +# FIXME: Replace `main' with a function in `-lgmp': +AC_CHECK_LIB([gmp], [__gmpz_init]) + +# Checks for header files. +AC_CHECK_HEADERS([stdlib.h string.h]) + +# Checks for typedefs, structures, and compiler characteristics. +AC_HEADER_STDBOOL +AC_C_INLINE +AC_TYPE_SIZE_T + +# Checks for library functions. +AC_FUNC_MALLOC +AC_CHECK_FUNCS([strdup]) + +AC_CONFIG_FILES([Makefile]) +AC_OUTPUT diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp new file mode 100644 index 000000000..7ffc6469a --- /dev/null +++ b/proofs/lfsc_checker/expr.cpp @@ -0,0 +1,966 @@ +#include "expr.h" +#include +#include +#ifdef _MSC_VER +#include +#endif +#include "check.h" + +using namespace std; + +int HoleExpr::next_id = 0; +int Expr::markedCount = 0; + +C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_CC(CExpr,kids,32768); + +//C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_CC(IntCExpr,_n,32768); + +#define USE_HOLE_PATH_COMPRESSION + +void Expr::debug() { + print(cout); + /* + cout << "\nAt " << this << "\n"; + cout << "marked = " << getmark() << "\n"; + */ + cout << "\n"; + cout.flush(); +} + +bool destroy_progs = false; + +#define destroydec(rr) \ + do { \ + Expr *r = rr; \ + int ref = r->data >> 9; \ + ref = ref - 1; \ + r->debugrefcnt(ref,DEC); \ + if (ref == 0) { \ + _e = r; \ + goto start_destroy; \ + } \ + else \ + r->data = (ref << 9) | (r->data & 511); \ + } while(0) + + +void Expr::destroy(Expr *_e, bool dec_kids) { + start_destroy: + switch (_e->getclass()) { + case INT_EXPR: + delete (IntExpr *)_e; + break; + case SYMS_EXPR: { + SymSExpr *e = (SymSExpr *)_e; + if (e->val && e->val->getop() != PROG) { + Expr *tmp = e->val; + delete e; + destroydec(tmp); + } + else + delete e; + break; + } + case SYM_EXPR: { + SymExpr *e = (SymExpr *)_e; + if (e->val && e->val->getop() != PROG) { + Expr *tmp = e->val; + delete e; + destroydec(tmp); + } + else + delete e; + break; + } + case HOLE_EXPR: { + HoleExpr *e = (HoleExpr *)_e; + if (e->val) { + Expr *tmp = e->val; + delete e; + destroydec(tmp); + } + else + delete e; + break; + } + case CEXPR: { + CExpr *e = (CExpr *)_e; + if (dec_kids) { + Expr **cur = e->kids; + Expr *tmp; + while((tmp = *cur++)) { + if (*cur) + tmp->dec(); + else { + delete e; + destroydec(tmp); + break; + } + } + } + else + delete e; + break; + } + } +} + +Expr *Expr::clone() { + switch (getclass()) { + case INT_EXPR: + case RAT_EXPR: + inc(); + return this; + case SYMS_EXPR: + case SYM_EXPR: { + SymExpr *e = (SymExpr *)this; + if (e->val) + if (e->val->getop() != PROG) + return e->val->clone(); + e->inc(); + return e; + } + case HOLE_EXPR: { + HoleExpr *e = (HoleExpr *)this; + if (e->val) + return e->val->clone(); + e->inc(); + return e; + } + case CEXPR: { + CExpr *e = (CExpr *)this; + int op = e->getop(); + switch(op) { + case LAM: { +#ifdef DEBUG_SYM_NAMES + SymSExpr *var = (SymSExpr *)e->kids[0]; + SymSExpr *newvar = new SymSExpr(*var,SYMS_EXPR); +#else + SymExpr *var = (SymExpr *)e->kids[0]; + SymExpr *newvar = new SymExpr(*var); +#endif + Expr *prev = var->val; + var->val = newvar; + Expr *bod = e->kids[1]->clone(); + var->val = prev; + return new CExpr(LAM,newvar,bod); + } + case PI: { +#ifdef DEBUG_SYM_NAMES + SymSExpr *var = (SymSExpr *)e->kids[0]; + SymSExpr *newvar = new SymSExpr(*var,SYMS_EXPR); +#else + SymExpr *var = (SymExpr *)e->kids[0]; + SymExpr *newvar = new SymExpr(*var); +#endif + Expr *tp = e->kids[1]->clone(); + Expr *prev = var->val; + var->val = newvar; + Expr *bod = e->kids[2]->clone(); + var->val = prev; + Expr* ret = new CExpr(PI,newvar,tp,bod); + if( data&256 ) + ret->data |=256; + return ret; + } + default: { + Expr **cur = e->kids; + Expr *tmp; + int size = 0; + while((*cur++)) + size++; + Expr **kids = new Expr*[size+1]; + kids[size]=0; + cur = e->kids; + bool diff_kid = false; + int i = 0; + while((tmp = *cur++)) { + Expr *c = tmp->clone(); + diff_kid |= (c != tmp); + kids[i++] = c; + } + if (diff_kid) + return new CExpr(op, true /* dummy */, kids); + for (int i = 0, iend = size; i != iend; i++) + kids[i]->dec(); + delete[] kids; + e->inc(); + return e; + } + } + } + } + return 0; // should never be reached +} + + +Expr* Expr::build_app(Expr *hd, const std::vector &args, int start) { +#ifndef USE_FLAT_APP + Expr *ret = hd; + for (int i = start, iend = args.size(); i < iend; i++) + ret = new CExpr(APP,ret,args[i]); + return ret; +#else + if( start>=(int)args.size() ) + return hd; + else + { + CExpr *ret = new CExpr( APP ); + ret->kids = new Expr* [args.size()-start+2]; + ret->kids[0] = hd; + for (int i = start, iend = args.size(); i < iend; i++) + ret->kids[i-start+1] = args[i]; + ret->kids[args.size()-start+1] = NULL; + return ret; + } +#endif +} + +Expr* Expr::make_app(Expr* e1, Expr* e2 ) +{ + //std::cout << "make app from "; + //e1->print( std::cout ); + //std::cout << " "; + //e2->print( std::cout ); + //std::cout << std::endl; + CExpr *ret; + if( e1->getclass()==CEXPR ){ + int counter = 0; + while( ((CExpr*)e1)->kids[counter] ){ + counter++; + } + ret = new CExpr( APP ); + ret->kids = new Expr* [counter+2]; + counter = 0; + while( ((CExpr*)e1)->kids[counter] ){ + ret->kids[counter] = ((CExpr*)e1)->kids[counter]; + counter++; + } + ret->kids[counter] = e2; + ret->kids[counter+1] = NULL; + }else{ + ret = new CExpr( APP, e1, e2 ); + } + //ret->print( std::cout ); + //std::cout << std::endl; + return ret; +} + +int Expr::cargCount = 0; + +Expr *Expr::collect_args(std::vector &args, bool follow_defs) { + //cargCount++; + //if( cargCount%1000==0) + //std::cout << cargCount << std::endl; +#ifndef USE_FLAT_APP + CExpr *e = (CExpr *)this; + args.reserve(16); + while( e->getop() == APP ) { + args.push_back(e->kids[1]); + e = (CExpr *)e->kids[0]; + if (follow_defs) + e = (CExpr *)e->followDefs(); + } + std::reverse(args.begin(),args.end()); + return e; +#else + CExpr *e = (CExpr *)this; + args.reserve(16); + if( e->getop()==APP ){ + int counter = 1; + while( e->kids[counter] ) { + args.push_back(e->kids[counter]); + counter++; + } + e = (CExpr*)e->kids[0]; + } + if (follow_defs) + return e->followDefs(); + else + return e; +#endif +} + +Expr *Expr::get_head(bool follow_defs) { + CExpr *e = (CExpr *)this; + while( e->getop() == APP ) { + e = (CExpr *)e->kids[0]; + if (follow_defs) + e = (CExpr *)e->followDefs(); + } + return e; +} + +Expr *Expr::get_body(int op, bool follow_defs) { + CExpr *e = (CExpr *)this; + while( e->getop() == op ) { + e = (CExpr *)e->kids[2]; + if (follow_defs) + e = (CExpr *)e->followDefs(); + } + return e; +} + +// if the return value is different from this, then it is a new reference +Expr *CExpr::whr() { + vector args; + if (get_head()->getop() == LAM) { + CExpr *head = (CExpr *)collect_args(args, true); + Expr *cloned_head; + if (head->cloned()) { + // we must clone + head = (CExpr *)head->clone(); + cloned_head = head; + } + else { + head->setcloned(); + cloned_head = 0; + } + int i = 0; + int iend = args.size(); + + /* we will end up incrementing the ref count for all the args, + since each is either pointed to by a var (following a + beta-reduction), or else just an argument in the new + application we build below. */ + + do { + Expr *tmp = args[i++]->followDefs(); + ((SymExpr *)head->kids[0])->val = tmp; + tmp->inc(); + head = (CExpr *)head->kids[1]; + } while(head->getop() == LAM && i < iend); + for (; i < iend; i++) + args[i]->inc(); + head->inc(); + if (cloned_head) + cloned_head->dec(); + return build_app(head,args,i); + } + else + return this; +} + +Expr* CExpr::convert_to_tree_app( Expr* e ) +{ + if( e->getop()==APP ) + { + std::vector< Expr* > kds; + int counter = 1; + while( ((CExpr*)e)->kids[counter] ) + { + kds.push_back( convert_to_tree_app( ((CExpr*)e)->kids[counter] ) ); + counter++; + } + Expr* app = Expr::build_app( e->get_head(), kds ); + //app->inc(); + return app; + } + else + { + return e; + } +} + +Expr* CExpr::convert_to_flat_app( Expr* e ) +{ + if( e->getop()==APP ) + { + std::vector< Expr* > args; + Expr* hd = ((CExpr*)e)->collect_args( args ); + CExpr* nce = new CExpr( APP ); + nce->kids = new Expr *[(int)args.size()+2]; + nce->kids[0] = hd; + for( int a=0; a<(int)args.size(); a++ ) + { + nce->kids[a+1] = convert_to_flat_app( args[a] ); + } + nce->kids[(int)args.size()+1] = 0; + nce->inc(); + return nce; + } + else + { + return e; + } +} + +bool Expr::defeq(Expr *e) { + + /* we handle a few special cases up front, where this Expr might + equal e, even though they have different opclass (i.e., different + structure). */ + + if (this == e) + return true; + int op1 = getop(); + int op2 = e->getop(); + switch (op1) { + case ASCRIBE: + return ((CExpr *)this)->kids[0]->defeq(e); + case APP: { + Expr *tmp = ((CExpr *)this)->whr(); + if (tmp != this) { + bool b = tmp->defeq(e); + tmp->dec(); + return b; + } + if (get_head()->getclass() == HOLE_EXPR) { + vector args; + Expr *head = collect_args(args, true); + Expr *t = e; + t->inc(); + for (int i = 0, iend = args.size(); i < iend; i++) { + // don't worry about SYMS_EXPR's, since we should not be in code here. + if (args[i]->getclass() != SYM_EXPR || args[i]->getexmark()) + /* we cannot fill the hole in this case. Either this is not + a variable or we are using a variable again. */ + return false; + SymExpr *v = (SymExpr *)args[i]; + + // we may have been mapping from expected var v to a computed var + Expr *tmp = (v->val ? v->val : v); + + tmp->inc(); + t = new CExpr(LAM, tmp, t); + args[i]->setexmark(); + } + for (int i = 0, iend = args.size(); i < iend; i++) + args[i]->clearexmark(); +#ifdef DEBUG_HOLES + cout << "Filling hole "; + head->debug(); + cout << "with "; + t->debug(); +#endif + ((HoleExpr *)head)->val = t; + return true; + } + break; + } + case NOT_CEXPR: + switch (getclass()) { + case HOLE_EXPR: { + HoleExpr *h = (HoleExpr *)this; + if (h->val) + return h->val->defeq(e); +#ifdef DEBUG_HOLES + cout << "Filling hole "; + h->debug(); + cout << "with "; + e->debug(); +#endif +#ifdef USE_HOLE_PATH_COMPRESSION + Expr *tmp = e->followDefs(); +#else + Expr *tmp = e; +#endif + h->val = tmp; + tmp->inc(); + return true; + } + case SYMS_EXPR: + case SYM_EXPR: { + SymExpr *s = (SymExpr *)this; + if (s->val) + return s->val->defeq(e); + break; + } + } + break; + } + + switch (op2) { + case ASCRIBE: + return defeq(((CExpr *)e)->kids[0]); + case APP: { + Expr *tmp = ((CExpr *)e)->whr(); + if (tmp != e) { + bool b = defeq(tmp); + tmp->dec(); + return b; + } + break; + } + case NOT_CEXPR: + switch (e->getclass()) { + case HOLE_EXPR: { + HoleExpr *h = (HoleExpr *)e; + if (h->val) + return defeq(h->val); + +#ifdef DEBUG_HOLES + cout << "Filling hole "; + h->debug(); + cout << "with "; + debug(); +#endif +#ifdef USE_HOLE_PATH_COMPRESSION + Expr *tmp = followDefs(); +#else + Expr *tmp = this; +#endif + h->val = tmp; + tmp->inc(); + return true; + } + case SYMS_EXPR: + case SYM_EXPR: { + SymExpr *s = (SymExpr *)e; + if (s->val) + return defeq(s->val); + break; + } + } + break; + } + + /* at this point, e1 and e2 must have the same opclass if they are + to be equal. */ + + if (op1 != op2) + return false; + + if (op1 == NOT_CEXPR) { + switch(getclass()) { + case INT_EXPR: { + IntExpr *i1 = (IntExpr *)this; + IntExpr *i2 = (IntExpr *)e; + return (mpz_cmp(i1->n,i2->n) == 0); + } + case RAT_EXPR: { + RatExpr *r1 = (RatExpr *)this; + RatExpr *r2 = (RatExpr *)e; + return (mpq_cmp(r1->n,r2->n) == 0); + } + case SYMS_EXPR: + case SYM_EXPR: + return (this == e); + } + } + + /* Now op1 and op2 must both be CExprs, and must have the same op to be + equal. */ + + CExpr *e1 = (CExpr *)this; + CExpr *e2 = (CExpr *)e; + + int last = 1; + switch (op1) { + case PI: + if (!e1->kids[1]->defeq(e2->kids[1])) + return false; + last++; + // fall through to LAM case + case LAM: { + + /* It is critical that we point e1's var. (v1) back to e2's (call + it v2). The reason this is critical is that we assume any + holes are in e1. So we could end up with (_ v1) = t. We wish + to fill _ in this case with (\ v2 t). If v2 pointed to v1, we + could not return (\ v1 t), because the fact that v2 points to + v1 would then be lost. + */ + SymExpr *v1 = (SymExpr *)e1->kids[0]; + Expr *prev_v1_val = v1->val; + v1->val = e2->kids[0]->followDefs(); + bool bodies_equal = e1->kids[last]->defeq(e2->kids[last]); + v1->val = prev_v1_val; + return bodies_equal; + } + case APP: +#ifndef USE_FLAT_APP + return (e1->kids[0]->defeq(e2->kids[0]) && + e1->kids[1]->defeq(e2->kids[1])); +#else + { + int counter = 0; + while( e1->kids[counter] ){ + if( !e2->kids[counter] || !e1->kids[counter]->defeq( e2->kids[counter] ) ) + return false; + counter++; + } + return e2->kids[counter]==NULL; + } +#endif + case TYPE: + case KIND: + case MPZ: + // already checked that both exprs have the same opclass. + return true; + } // switch(op1) + + return false; // never reached. +} + +int Expr::fiCounter = 0; + +bool Expr::free_in(Expr *x) { + //fiCounter++; + //if( fiCounter%1==0 ) + // std::cout << fiCounter << std::endl; + switch(getop()) { + case NOT_CEXPR: + switch (getclass()) { + case HOLE_EXPR: { + HoleExpr *h = (HoleExpr *)this; + if (h->val) + return h->val->free_in(x); + return (h == x); + } + case SYMS_EXPR: + case SYM_EXPR: { + SymExpr *s = (SymExpr *)this; + if (s->val && s->val->getclass() == HOLE_EXPR) + /* we do not need to follow the "val" pointer except in this + one case, when x is a hole (which we do not bother to check + here) */ + return s->val->free_in(x); + return (s == x); + } + case INT_EXPR: + return false; + } + break; + case LAM: + case PI: + if (x == ((CExpr *)this)->kids[0]) + return false; + // fall through + default: { + // must be a CExpr + CExpr *e = (CExpr *)this; + Expr *tmp; + Expr **cur = e->kids; + while ((tmp = *cur++)) + if (tmp->free_in(x)) + return true; + return false; + } + } + return false; // should not be reached +} + +void Expr::calc_free_in(){ + data &= ~256; + data |= 256*((CExpr *)this)->kids[2]->free_in( ((CExpr *)this)->kids[0] ); +} + +string Expr::toString() { + ostringstream oss; + print(oss); + return oss.str(); +} + +static void print_kids(ostream &os, Expr **kids) { + Expr *tmp; + while ((tmp = *kids++)) { + os << " "; + tmp->print(os); + } +} + +static void print_vector(ostream &os, const vector &v) { + for(int i = 0, iend = v.size(); i < iend; i++) { + os << " "; + v[i]->print(os); + } +} + +void Expr::print(ostream &os) { + CExpr *e = (CExpr *)this; // for CEXPR cases + + //std::cout << e->getop() << " "; + /* +#ifdef DEBUG_REFCNT + os << "<"; + char tmp[10]; + sprintf(tmp,"%d",getrefcnt()); + os << tmp << "> "; +#endif +*/ + + switch(getop()) { + case NOT_CEXPR: { + switch(getclass()) { + case INT_EXPR: + { + IntExpr *e = (IntExpr *)this; + if (mpz_sgn(e->n) < 0) { + os << "(~ "; + mpz_t tmp; + mpz_init(tmp); + mpz_neg(tmp,e->n); + char *s = mpz_get_str(0,10,tmp); + os << s; + free(s); + mpz_clear(tmp); + os << ")"; + //os << "mpz"; + } + else { + char *s = mpz_get_str(0,10,e->n); + os << s; + free(s); + //os << "mpz"; + } + break; + } + case RAT_EXPR: + { + RatExpr *e = (RatExpr *)this; + char *s = mpq_get_str(0,10,e->n); + os << s; + if (mpq_sgn(e->n) < 0) { + os << "(~ "; + mpq_t tmp; + mpq_init(tmp); + mpq_neg(tmp,e->n); + char *s = mpq_get_str(0,10,tmp); + os << s; + free(s); + mpq_clear(tmp); + os << ")"; + } + else { + char *s = mpq_get_str(0,10,e->n); + os << s; + free(s); + } + break; + } +#ifndef DEBUG_SYM_NAMES + case SYM_EXPR: + { + SymExpr *e = (SymExpr *)this; + if (e->val) { + if (e->val->getop() == PROG) { + os << e; +#ifdef DEBUG_SYMS + os << "[PROG]"; +#endif + }else{ +#ifdef DEBUG_SYMS + os << e; + os << "[SYM "; +#endif + e->val->print(os); +#ifdef DEBUG_SYMS + os << "]"; +#endif + } + } + else + os << e; + break; + } +#else + case SYM_EXPR: /* if we are debugging sym names, then + SYM_EXPRs are really SymSExprs. */ +#endif + case SYMS_EXPR: { + SymSExpr *e = (SymSExpr *)this; + if (e->val) { + if (e->val->getop() == PROG) { + os << e->s; +#ifdef DEBUG_SYMS + os << "[PROG]"; +#endif + }else{ +#ifdef DEBUG_SYMS + os << e->s; + os << "[SYM "; +#endif + e->val->print(os); +#ifdef DEBUG_SYMS + os << "]"; +#endif + } + } + else + os << e->s; + break; + } + case HOLE_EXPR: + { + HoleExpr *e = (HoleExpr *)this; + if (e->val) { +#ifdef DEBUG_SYMS + os << "_" << "[HOLE "; +#endif + e->val->print(os); +#ifdef DEBUG_SYMS + os << "]"; +#endif + }else { + os << "_"; +#ifdef DEBUG_HOLE_NAMES + char tmp[100]; + sprintf(tmp,"%d",e->id); + os << "[ " << tmp << "]"; +#else + os << "[ " << e << "]"; +#endif + } + break; + } + default: + os << "; unrecognized form of expr"; + break; + } + break; + } // case NOT_CEXPR + case APP: { + os << "("; + vector args; + Expr *head = collect_args(args, false /* follow_defs */); + head->print(os); + print_vector(os, args); + os << ")"; + break; + } + case LAM: + os << "(\\"; + print_kids(os, e->kids); + os << ")"; + break; + case PI: + os << "(!"; + print_kids(os, e->kids); + os << ")"; + break; + case TYPE: + os << "type"; + break; + case KIND: + os << "kind"; + break; + case MPZ: + os << "mpz"; + break; + case MPQ: + os << "mpq"; + break; + case ADD: + os << "(mp_add"; + print_kids(os,e->kids); + os << ")"; + break; + case MUL: + os << "(mp_mul"; + print_kids(os,e->kids); + os << ")"; + break; + case DIV: + os << "(mp_div"; + print_kids(os,e->kids); + os << ")"; + break; + case NEG: + os << "(mp_neg"; + print_kids(os,e->kids); + os << ")"; + break; + case IFNEG: + os << "(ifneg"; + print_kids(os,e->kids); + os << ")"; + break; + case IFZERO: + os << "(ifzero"; + print_kids(os,e->kids); + os << ")"; + break; + case RUN: + os << "(run"; + print_kids(os,e->kids); + os << ")"; + break; + case PROG: + os << "(prog"; + print_kids(os,e->kids); + os << ")"; + break; + case PROGVARS: + os << "("; + print_kids(os,e->kids); + os << ")"; + break; + case MATCH: + os << "(match"; + print_kids(os,e->kids); + os << ")"; + break; + case CASE: + os << "("; + print_kids(os,e->kids); + os << ")"; + break; + case LET: + os << "(let"; + print_kids(os,e->kids); + os << ")"; + break; + case DO: + os << "(do"; + print_kids(os,e->kids); + os << ")"; + break; + case IFMARKED: + os << "(ifmarked"; + print_kids(os,e->kids); + os << ")"; + break; + case COMPARE: + os << "(compare"; + print_kids(os,e->kids); + os << ")"; + break; + case MARKVAR: + os << "(markvar"; + print_kids(os,e->kids); + os << ")"; + break; + case FAIL: + os << "(fail "; + print_kids(os, e->kids); + os << ")"; + break; + case ASCRIBE: + os << "(:"; + print_kids(os, e->kids); + os << ")"; + break; + default: + os << "; unrecognized form of expr(2) " << getop() << " " << getclass(); + } // switch(getop()) +} + +bool Expr::isType( Expr* statType ){ + Expr* typ = this; + while( typ!=statType ){ + if( typ->getop()==PI ){ + typ = ((CExpr*)typ)->kids[2]; + }else{ + return false; + } + } + return true; +} + +int SymExpr::symmCount = 0; +#ifdef MARKVAR_32 +int SymExpr::mark() +{ + if( mark_map.find( this )== mark_map.end() ) + { + symmCount++; + mark_map[this] = 0; + } + return mark_map[this]; +} +void SymExpr::smark( int m ) +{ + mark_map[this] = m; +} +#endif \ No newline at end of file diff --git a/proofs/lfsc_checker/expr.h b/proofs/lfsc_checker/expr.h new file mode 100644 index 000000000..32a62ab33 --- /dev/null +++ b/proofs/lfsc_checker/expr.h @@ -0,0 +1,367 @@ +#ifndef sc2__expr_h +#define sc2__expr_h + +#include "gmp.h" +#include +#include +#include +#include +#include "chunking_memory_management.h" + +#define USE_FLAT_APP +#define MARKVAR_32 +#define DEBUG_SYM_NAMES +//#define DEBUG_SYMS + +// Expr class +enum { CEXPR = 0, + INT_EXPR, + RAT_EXPR, + HOLE_EXPR, + SYM_EXPR, + SYMS_EXPR }; + +// operators for CExprs +enum { NOT_CEXPR = 0, // for INT_EXPR, HOLE_EXPR, SYM_EXPR, SYMS_EXPR + APP, + PI, + LAM, + TYPE, + KIND, + ASCRIBE, + MPZ, + MPQ, + + PROG, + PROGVARS, + MATCH, + CASE, + PAT, + DO, + ADD, + MUL, + DIV, + NEG, + IFNEG, + IFZERO, + LET, + RUN, + FAIL, + MARKVAR, + IFMARKED, + COMPARE +}; + +class SymExpr; + +class Expr { +protected: + /* bits 0-2: Expr class + bits 3-7: operator + bit 8: a flag for already cloned, free_in calculation + bits 9-31: ref count*/ + int data; + + void destroy(bool dec_kids); + + enum { INC, DEC, CREATE }; + void debugrefcnt(int ref, int what) { +#ifdef DEBUG_REFCNT + std::cout << "["; + debug(); + switch(what) { + case INC: + std::cout << " inc to "; + break; + case DEC: + std::cout << " dec to "; + break; + case CREATE: + std::cout << " creating]\n"; + return; + } + char tmp[10]; + sprintf(tmp,"%d",ref); + std::cout << tmp << "]\n"; +#else + (void)ref; + (void)what; +#endif + } + + Expr(int _class, int _op) + : data(1 << 9 /* refcount 1, not cloned */| (_op << 3) | _class) + { } + +public: + static int markedCount; + inline Expr* followDefs(); + inline int getclass() const { return data & 7; } + int getexmark() const { return data & 256; } + void setexmark() { data |= 256; } + void clearexmark() { data &= ~256; } + inline int getop() const { return (data >> 3) & 31; } + int cloned() const { return data & 256; } + void setcloned() { data |= 256; } + + inline int getrefcnt() { return data >> 9; } + inline void inc() { + int ref = getrefcnt(); + //static int iCounter = 0; + //iCounter++; + //if( iCounter%10000==0 ){ + // //print( std::cout ); + // std::cout << " " << ref << std::endl; + //} + ref = ref<4194303 ? ref + 1 : ref; + debugrefcnt(ref,INC); + data = (ref << 9) | (data & 511); + } + static void destroy(Expr *, bool); + inline void dec(bool dec_kids = true) { + int ref = getrefcnt(); + ref = ref - 1; + debugrefcnt(ref,DEC); + if (ref == 0) + destroy(this,dec_kids); + else + data = (ref << 9) | (data & 511); + } + + //must pass statType (the expr representing "type") to this function + bool isType( Expr* statType ); + + inline bool isDatatype() { + return getclass() == SYMS_EXPR || getop() == MPZ || getop() == MPQ; + } + inline bool isArithTerm() { + return getop() == ADD || getop() == NEG; + } + + static Expr *build_app(Expr *hd, const std::vector &args, + int start = 0); + + static Expr *make_app(Expr* e1, Expr* e2 ); + + /* if this is an APP, return the head, and store the args in args. + If follow_defs is true, we proceed through defined heads; + otherwise not. */ + Expr *collect_args(std::vector &args, bool follow_defs = true); + + Expr *get_head(bool follow_defs = true); + + Expr *get_body(int op = PI, bool follow_defs = true); + + std::string toString(); + + void print(std::ostream &); + void debug(); + + /* check whether or not this expr is alpha equivalent to e. If this + expr contains unfilled holes, fill them as we go. We do not fill + holes in e. We do not take responsibility for the reference to + this nor the reference to e. */ + bool defeq(Expr *e); + + /* return a clone of this expr. All abstractions are really duplicated + in memory. Other expressions may not actually be duplicated in + memory, but their refcounts will be incremented. */ + Expr *clone(); + + // x can be a SymExpr or a HoleExpr. + bool free_in(Expr *x); + bool get_free_in() { return data & 256; } + void calc_free_in(); + + static int cargCount; + static int fiCounter; +}; + +class CExpr : public Expr { +public: + C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_H(CExpr,kids); + + Expr **kids; + ~CExpr() { + delete[] kids; + } + CExpr(int _op) : Expr(CEXPR, _op), kids() { + kids = new Expr *[1]; + kids[0] = 0; + debugrefcnt(1,CREATE); + } + CExpr(int _op, Expr *e1) : Expr(CEXPR, _op), kids() { + kids = new Expr *[2]; + kids[0] = e1; + kids[1] = 0; + debugrefcnt(1,CREATE); + } + CExpr(int _op, Expr *e1, Expr *e2) + : Expr(CEXPR, _op), kids() { + kids = new Expr *[3]; + kids[0] = e1; + kids[1] = e2; + kids[2] = 0; + debugrefcnt(1,CREATE); + } + CExpr(int _op, Expr *e1, Expr *e2, Expr *e3) + : Expr(CEXPR, _op), kids() { + kids = new Expr *[4]; + kids[0] = e1; + kids[1] = e2; + kids[2] = e3; + kids[3] = 0; + debugrefcnt(1,CREATE); + } + CExpr(int _op, Expr *e1, Expr *e2, Expr *e3, Expr *e4) + : Expr(CEXPR, _op), kids() { + kids = new Expr *[5]; + kids[0] = e1; + kids[1] = e2; + kids[2] = e3; + kids[3] = e4; + kids[4] = 0; + debugrefcnt(1,CREATE); + } + CExpr(int _op, const std::vector &_kids) + : Expr(CEXPR, _op), kids() { + int i, iend = _kids.size(); + kids = new Expr *[iend + 1]; + for (i = 0; i < iend; i++) + kids[i] = _kids[i]; + kids[i] = 0; + debugrefcnt(1,CREATE); + } + + // _kids must be null-terminated. + CExpr(int _op, bool dummy, Expr **_kids) : Expr(CEXPR, _op), kids(_kids) { + (void)dummy; + debugrefcnt(1,CREATE); + } + + Expr *whr(); + + static Expr* convert_to_tree_app( Expr* ce ); + static Expr* convert_to_flat_app( Expr* ce ); +}; + +class IntExpr : public Expr { + public: + mpz_t n; + ~IntExpr() { + mpz_clear(n); + } + IntExpr(mpz_t _n) : Expr(INT_EXPR, 0), n() { + mpz_init_set(n,_n); + debugrefcnt(1,CREATE); + } + IntExpr(signed long int _n ) : Expr(INT_EXPR, 0), n() { + mpz_init_set_si( n, _n ); + } + + unsigned long int get_num() { return mpz_get_ui( n ); } +}; + +class RatExpr : public Expr { + public: + mpq_t n; + ~RatExpr() { + mpq_clear(n); + } + RatExpr(mpq_t _n) : Expr(RAT_EXPR, 0), n() { + mpq_init( n ); + mpq_set(n,_n); + debugrefcnt(1,CREATE); + mpq_canonicalize( n ); + } + RatExpr(signed long int _n1, unsigned long int _n2 ) : Expr(RAT_EXPR, 0), n() { + mpq_init( n ); + mpq_set_si( n, _n1, _n2 ); + mpq_canonicalize( n ); + } +}; + +class SymExpr : public Expr { + public: + Expr *val; // may be set by beta-reduction and clone(). + static int symmCount; + + SymExpr(std::string _s, int theclass = SYM_EXPR) + : Expr(theclass, 0), val(0) + { + (void)_s; + if (theclass == SYM_EXPR) + debugrefcnt(1,CREATE); + } + SymExpr(const SymExpr &e, int theclass = SYM_EXPR) + : Expr(theclass, 0), val(0) + { + (void)e; + if (theclass == SYM_EXPR) + debugrefcnt(1,CREATE); + } +#ifdef MARKVAR_32 +private: + int mark(); + void smark( int m ); +public: + int getmark( int i = 0 ) { return (mark() >> i)&1; } + void setmark( int i = 0 ) { smark( mark() | (1 << i) ); } + void clearmark( int i = 0 ) { smark( mark() & ~(1 << i) ); } +#endif +}; + +class SymSExpr : public SymExpr { + public: + std::string s; + SymSExpr(std::string _s, int theclass = SYMS_EXPR) + : SymExpr(_s, theclass), s(_s) + { + debugrefcnt(1,CREATE); + } + SymSExpr(const SymSExpr &e, int theclass = SYMS_EXPR) + : SymExpr(e, theclass), s(e.s) + { + debugrefcnt(1,CREATE); + } +}; + +class HoleExpr : public Expr { + static int next_id; +public: +#ifdef DEBUG_HOLE_NAMES + int id; +#endif + HoleExpr() + : Expr(HOLE_EXPR, 0), val(0) + { +#ifdef DEBUG_HOLE_NAMES + id = next_id++; +#endif + debugrefcnt(1,CREATE); + } + Expr *val; // may be set during subst(), defeq(), and clone(). +}; + +inline Expr * Expr::followDefs() { + switch(getclass()) { + case HOLE_EXPR: { + HoleExpr *h = (HoleExpr *)this; + if (h->val) + return h->val->followDefs(); + break; + } + case SYMS_EXPR: + case SYM_EXPR: { + SymExpr *h = (SymExpr *)this; + if (h->val) + return h->val->followDefs(); + break; + } + } + + return this; +} + +#endif + diff --git a/proofs/lfsc_checker/libwriter.cpp b/proofs/lfsc_checker/libwriter.cpp new file mode 100644 index 000000000..49e9bbaad --- /dev/null +++ b/proofs/lfsc_checker/libwriter.cpp @@ -0,0 +1,238 @@ +#include "libwriter.h" +#include +#include +#include + +void libwriter::get_var_name( const std::string& n, std::string& nn ) { + nn = std::string( n.c_str() ); + for( int i = 0; i <(int)n.length(); i++ ){ + char c = n[i]; + if (c <= 47) + c += 65; + else if (c >= 58 && c <= 64) + c += 97-58; + if ((c >= 91 && c <= 94) || c == 96) + c += 104-91; + else if (c >= 123) + c -= 4; + nn[i] = c; + } +} + +void libwriter::write_file() +{ + //std::cout << "write lib" << std::endl; + std::ostringstream os_enum; + std::ostringstream os_print; + std::ostringstream os_constructor_h; + std::ostringstream os_constructor_c; + + for ( int a=0; a<(int)syms.size(); a++ ) { + //std::cout << "sym #" << (a+1) << ": "; + //std::cout << ((SymSExpr*)syms[a])->s.c_str() << std::endl; + //defs[a]->print( std::cout ); + //std::cout << std::endl; + + if( defs[a]->getclass()==CEXPR ){ + //calculate which arguments are required for input + std::vector< Expr* > args; + std::vector< bool > argsNeed; + std::vector< Expr* > argTypes; + CExpr* c = ((CExpr*)defs[a]); + while( c->getop()==PI ){ + //std::cout << c->kids[0] << std::endl; + if( ((CExpr*)c->kids[1])->getop()!=RUN ){ + args.push_back( c->kids[0] ); + argsNeed.push_back( true ); + argTypes.push_back( c->kids[1] ); + } + for( int b=0; b<(int)args.size(); b++ ){ + if( argsNeed[b] ){ + if( ((CExpr*)c->kids[1])->getop()==RUN ){ + if( ((CExpr*)c->kids[1])->kids[1]->free_in( args[b] ) ){ + argsNeed[b] = false; + } + }else{ + if( c->kids[1]->free_in( args[b] ) ){ + argsNeed[b] = false; + } + } + } + } + c = (CExpr*)(c->kids[2]); + } + + //record if this declares a judgement + if( ((CExpr*)defs[a])->getop()==PI && c->getop()==TYPE ){ + //std::cout << "This is a judgement" << std::endl; + judgements.push_back( syms[a] ); + //record if this declares a proof rule + }else if( c->getclass()==CEXPR && std::find( judgements.begin(), judgements.end(), c->kids[0] )!=judgements.end() ){ + std::cout << "Handle rule: " << ((SymSExpr*)syms[a])->s.c_str() << std::endl; + //std::cout << "These are required to input:" << std::endl; + //for( int b=0; b<(int)args.size(); b++ ){ + // if( argsNeed[b] ){ + // std::cout << ((SymSExpr*)args[b])->s.c_str() << std::endl; + // } + //} + os_enum << " rule_" << ((SymSExpr*)syms[a])->s.c_str() << "," << std::endl; + + os_print << " case rule_" << ((SymSExpr*)syms[a])->s.c_str() << ": os << \""; + os_print << ((SymSExpr*)syms[a])->s.c_str() << "\";break;" << std::endl; + + std::ostringstream os_args; + os_args << "("; + bool firstTime = true; + for( int b=0; b<(int)args.size(); b++ ){ + if( argsNeed[b] ){ + if( !firstTime ) + os_args << ","; + std::string str; + get_var_name( ((SymSExpr*)args[b])->s, str ); + os_args << " LFSCProof* " << str.c_str(); + firstTime = false; + } + } + if( !firstTime ){ + os_args << " "; + } + os_args << ")"; + + os_constructor_h << " static LFSCProof* make_" << ((SymSExpr*)syms[a])->s.c_str(); + os_constructor_h << os_args.str().c_str() << ";" << std::endl; + + os_constructor_c << "LFSCProof* LFSCProof::make_" << ((SymSExpr*)syms[a])->s.c_str(); + os_constructor_c << os_args.str().c_str() << "{" << std::endl; + os_constructor_c << " LFSCProof **kids = new LFSCProof *[" << (int)args.size()+1 << "];" << std::endl; + for( int b=0; b<(int)args.size(); b++ ){ + os_constructor_c << " kids[" << b << "] = "; + if( argsNeed[b] ){ + std::string str; + get_var_name( ((SymSExpr*)args[b])->s, str ); + os_constructor_c << str.c_str(); + }else{ + os_constructor_c << "hole"; + } + os_constructor_c << ";" << std::endl; + } + os_constructor_c << " kids[" << (int)args.size() << "] = 0;" << std::endl; + os_constructor_c << " return new LFSCProofC( rule_" << ((SymSExpr*)syms[a])->s.c_str() << ", kids );" << std::endl; + os_constructor_c << "}" << std::endl << std::endl; + } + } + + //write the header + static std::string filename( "lfsc_proof" ); + std::fstream fsh; + std::string fnameh( filename ); + fnameh.append(".h"); + fsh.open( fnameh.c_str(), std::ios::out ); + + fsh << "#ifndef LFSC_PROOF_LIB_H" << std::endl; + fsh << "#define LFSC_PROOF_LIB_H" << std::endl; + fsh << std::endl; + fsh << "#include " << std::endl; + fsh << std::endl; + fsh << "class LFSCProof{" << std::endl; + fsh << "protected:" << std::endl; + fsh << " enum{" << std::endl; + fsh << os_enum.str().c_str(); + fsh << " };" << std::endl; + fsh << " static LFSCProof* hole;" << std::endl; + fsh << " LFSCProof(){}" << std::endl; + fsh << "public:" << std::endl; + fsh << " virtual ~LFSCProof(){}" << std::endl; + fsh << " static void init();" << std::endl; + fsh << std::endl; + fsh << " //functions to build LFSC proofs" << std::endl; + fsh << os_constructor_h.str().c_str(); + fsh << std::endl; + fsh << " virtual void set_child( int i, LFSCProof* e ) {}" << std::endl; + fsh << " virtual void print( std::ostream& os ){}" << std::endl; + fsh << "};" << std::endl; + fsh << std::endl; + fsh << "class LFSCProofC : public LFSCProof{" << std::endl; + fsh << " short id;" << std::endl; + fsh << " LFSCProof **kids;" << std::endl; + fsh << "public:" << std::endl; + fsh << " LFSCProofC( short d_id, LFSCProof **d_kids ) : id( d_id ), kids( d_kids ){}" << std::endl; + fsh << " void set_child( int i, LFSCProof* e ) { kids[i] = e; }" << std::endl; + fsh << " void print( std::ostream& os );" << std::endl; + fsh << "};" << std::endl; + fsh << std::endl; + fsh << "class LFSCProofSym : public LFSCProof{" << std::endl; + fsh << "private:" << std::endl; + fsh << " std::string s;" << std::endl; + fsh << " LFSCProofSym( std::string ss ) : s( ss ){}" << std::endl; + fsh << "public:" << std::endl; + fsh << " static LFSCProofSym* make( std::string ss ) { return new LFSCProofSym( ss ); }" << std::endl; + fsh << " static LFSCProofSym* make( const char* ss ) { return new LFSCProofSym( std::string( ss ) ); }" << std::endl; + fsh << " ~LFSCProofSym(){}" << std::endl; + fsh << " void print( std::ostream& os ) { os << s.c_str(); }" << std::endl; + fsh << "};" << std::endl; + fsh << std::endl; + fsh << "class LFSCProofLam : public LFSCProof{" << std::endl; + fsh << " LFSCProofSym* var;" << std::endl; + fsh << " LFSCProof* body;" << std::endl; + fsh << " LFSCProof* typ;" << std::endl; + fsh << " LFSCProofLam( LFSCProofSym* d_var, LFSCProof* d_body, LFSCProof* d_typ ) : var( d_var ), body( d_body ), typ( d_typ ){}" << std::endl; + fsh << "public:" << std::endl; + fsh << " static LFSCProof* make( LFSCProofSym* d_var, LFSCProof* d_body, LFSCProof* d_typ = NULL ) {" << std::endl; + fsh << " return new LFSCProofLam( d_var, d_body, d_typ );" << std::endl; + fsh << " }" << std::endl; + fsh << " ~LFSCProofLam(){}" << std::endl; + fsh << std::endl; + fsh << " void print( std::ostream& os );" << std::endl; + fsh << "};" << std::endl; + fsh << std::endl; + fsh << "#endif" << std::endl; + + //write the cpp + std::fstream fsc; + std::string fnamec( filename ); + fnamec.append(".cpp"); + fsc.open( fnamec.c_str(), std::ios::out ); + + fsc << "#include \"lfsc_proof.h\"" << std::endl; + fsc << std::endl; + fsc << "LFSCProof* LFSCProof::hole = NULL;" << std::endl; + fsc << std::endl; + fsc << "void LFSCProof::init(){" << std::endl; + fsc << " hole = LFSCProofSym::make( \"_\" );" << std::endl; + fsc << "}" << std::endl; + fsc << std::endl; + fsc << "void LFSCProofC::print( std::ostream& os ){" << std::endl; + fsc << " os << \"(\";" << std::endl; + fsc << " switch( id ){" << std::endl; + fsc << os_print.str().c_str(); + fsc << " }" << std::endl; + fsc << " int counter = 0;" << std::endl; + fsc << " while( kids[counter] ){" << std::endl; + fsc << " os << \" \";" << std::endl; + fsc << " kids[counter]->print( os );" << std::endl; + fsc << " counter++;" << std::endl; + fsc << " }" << std::endl; + fsc << " os << \")\";" << std::endl; + fsc << "}" << std::endl; + fsc << std::endl; + fsc << "void LFSCProofLam::print( std::ostream& os ){" << std::endl; + fsc << " os << \"(\";" << std::endl; + fsc << " if( typ ){" << std::endl; + fsc << " os << \"% \";" << std::endl; + fsc << " }else{" << std::endl; + fsc << " os << \"\\\\ \";" << std::endl; + fsc << " }" << std::endl; + fsc << " var->print( os );" << std::endl; + fsc << " if( typ ){" << std::endl; + fsc << " os << \" \";" << std::endl; + fsc << " typ->print( os );" << std::endl; + fsc << " }" << std::endl; + fsc << " os << std::endl;" << std::endl; + fsc << " body->print( os );" << std::endl; + fsc << " os << \")\";" << std::endl; + fsc << "}" << std::endl; + fsc << std::endl; + fsc << os_constructor_c.str().c_str(); + fsc << std::endl; + } +} diff --git a/proofs/lfsc_checker/libwriter.h b/proofs/lfsc_checker/libwriter.h new file mode 100644 index 000000000..093cf541b --- /dev/null +++ b/proofs/lfsc_checker/libwriter.h @@ -0,0 +1,28 @@ +#ifndef LIB_WRITER_H +#define LIB_WRITER_H + +#include "expr.h" +#include + +class libwriter +{ +private: + std::vector< Expr* > syms; + std::vector< Expr* > defs; + + std::vector< Expr* > judgements; + //get the variable name + void get_var_name( const std::string& n, std::string& nn ); +public: + libwriter(){} + virtual ~libwriter(){} + + void add_symbol( Expr* s, Expr* t ) { + syms.push_back( s ); + defs.push_back( t ); + } + + void write_file(); +}; + +#endif diff --git a/proofs/lfsc_checker/main.cpp b/proofs/lfsc_checker/main.cpp new file mode 100644 index 000000000..80f36e69f --- /dev/null +++ b/proofs/lfsc_checker/main.cpp @@ -0,0 +1,139 @@ +#include "expr.h" +#include "check.h" +#include +#include "sccwriter.h" +#include "libwriter.h" +#include + +using namespace std; + +args a; + +static void parse_args(int argc, char **argv, args &a) +{ + char *arg0 = *argv; + + /* skip 0'th argument */ + argv++; + argc--; + + while (argc) { + + if ((strncmp("-h", *argv, 2) == 0) || + (strncmp("--h", *argv, 3) == 0)) { + cout << "Usage: " << arg0 << " [options] infile1 ...infile_n\n"; + cout << "If no infiles are named on the command line, input is read\n" + << "from stdin. Specifying the infile \"stdin\" will also read\n" + << "from stdin. Options are:\n\n"; + cout << "--show-runs: print debugging information for runs of side condition code\n"; + cout << "--compile-scc: compile side condition code\n"; + cout << "--compile-scc-debug: compile debug versions of side condition code\n"; + cout << "--run-scc: use compiled side condition code\n"; + exit(0); + } + else if(strcmp("--show-runs", *argv) == 0) { + argc--; argv++; + a.show_runs = true; + } + else if(strcmp("--no-tail-calls", *argv) == 0) { + // this is just for debugging. + argc--; argv++; + a.no_tail_calls = true; + } + else if( strcmp("--compile-scc", *argv) == 0 ){ + argc--; argv++; + a.compile_scc = true; + a.compile_scc_debug = false; + } + else if( strcmp("--compile-scc-debug", *argv) == 0 ) + { + argc--; argv++; + a.compile_scc = true; + a.compile_scc_debug = true; + } + else if( strcmp("--compile-lib", *argv) == 0 ) + { + argc--; argv++; + a.compile_lib = true; + } + else if( strcmp("--run-scc", *argv) == 0 ){ + argc--; argv++; + a.run_scc = true; + } + else if( strcmp("--use-nested-app", *argv) == 0 ){ + argc--; argv++; + a.use_nested_app = true; //not implemented yet + }else { + a.files.push_back(*argv); + argc--; argv++; + } + } +} + +void sighandler(int /* signum */) { + cerr << "\nInterrupted. sc is aborting.\n"; + exit(1); +} + +int main(int argc, char **argv) { + + a.show_runs = false; + a.no_tail_calls = false; + a.compile_scc = false; + a.run_scc = false; + a.use_nested_app = false; + + signal(SIGINT, sighandler); + + parse_args(argc, argv, a); + + init(); + + check_time = (int)clock(); + + if (a.files.size()) { + sccwriter* scw = NULL; + libwriter* lw = NULL; + if( a.compile_scc ){ + scw = new sccwriter( a.compile_scc_debug ? opt_write_call_debug : 0 ); + } + if( a.compile_lib ){ + lw = new libwriter; + } + /* process the files named */ + int i = 0, iend = a.files.size(); + for (; i < iend; i++) { + const char *filename = a.files[i].c_str(); + check_file(filename, a, scw, lw); + } + if( scw ){ + scw->write_file(); + delete scw; + } + if( lw ){ +#ifdef DEBUG_SYM_NAMES + lw->write_file(); + delete lw; +#else + std::cout << "ERROR libwriter: Must compile LFSC with DEBUG_SYM_NAMES flag (see Expr.h)" << std::endl; +#endif + } + } + else + check_file("stdin", a); + + //std::cout << "time = " << (int)clock() - t << std::endl; + //while(1){} + +#ifdef DEBUG + cout << "Clearing globals.\n"; + cout.flush(); + + cleanup(); + a.files.clear(); +#endif + + std::cout << "time = " << (int)clock() - check_time << std::endl; + std::cout << "sym count = " << SymExpr::symmCount << std::endl; + std::cout << "marked count = " << Expr::markedCount << std::endl; +} diff --git a/proofs/lfsc_checker/position.h b/proofs/lfsc_checker/position.h new file mode 100644 index 000000000..a5c51ffc6 --- /dev/null +++ b/proofs/lfsc_checker/position.h @@ -0,0 +1,30 @@ +#ifndef sc2__position_h +#define sc2__position_h + +#include +#include + +class Position { +public: + const char *filename; + int linenum; + int colnum; + + Position(const char *_f, int l, int c) : filename(_f), linenum(l), colnum(c) + {} + void print(std::ostream &os) { + os << filename; + if (colnum == -1) { + char tmp[1024]; + sprintf(tmp, ", line %d, end of column: ", linenum); + os << tmp; + } + else { + char tmp[1024]; + sprintf(tmp, ", line %d, column %d: ", linenum, colnum); + os << tmp; + } + } +}; + +#endif diff --git a/proofs/lfsc_checker/print_smt2.cpp b/proofs/lfsc_checker/print_smt2.cpp new file mode 100644 index 000000000..bf068c248 --- /dev/null +++ b/proofs/lfsc_checker/print_smt2.cpp @@ -0,0 +1,122 @@ +#include "print_smt2.h" + +#ifdef PRINT_SMT2 + +void print_smt2( Expr* p, std::ostream& s, short mode ) +{ + switch( p->getclass() ) + { + case CEXPR: + { + switch( p->getop() ) + { + case APP: + { + std::vector args; + Expr *head = p->collect_args(args, false); + short newMode = get_mode( head ); + if( is_smt2_poly_formula( head ) ) + { + s << "("; + head->print( s ); + s << " "; + print_smt2( args[1], s, newMode ); + s << " "; + print_smt2( args[2], s, newMode ); + s << ")"; + } + else if( ( mode==2 || mode==3 ) && mode==newMode ) + { + print_smt2( args[0], s, newMode ); + s << " "; + print_smt2( args[1], s, newMode ); + } + else if( newMode==1 ) + { + if( mode!=1 || newMode!=mode ){ + s << "("; + } + print_smt2( args[2], s, newMode ); + s << " "; + print_smt2( args[3], s, 0 ); + if( mode!=1 || newMode!=mode ){ + s << ")"; + } + } + else + { + s << "("; + switch( newMode ) + { + case 4: s << "=>";break; + default: head->print( s );break; + } + s << " "; + for( int a=0; a<(int)args.size(); a++ ){ + print_smt2( args[a], s, newMode ); + if( a!=args.size()-1 ) + s << " "; + } + s << ")"; + } + } + break; + default: + std::cout << "Unhandled op " << p->getop() << std::endl; + break; + } + } + break; + case HOLE_EXPR: + { + HoleExpr *e = (HoleExpr *)p; + if( e->val ){ + print_smt2( e->val, s, mode ); + }else{ + s << "_"; + } + } + break; + case SYMS_EXPR: + case SYM_EXPR: + if( ((SymExpr*)p)->val ) + print_smt2( ((SymExpr*)p)->val, s, mode ); + else + p->print( s ); + break; + default: + std::cout << "Unhandled class " << p->getclass() << std::endl; + break; + } +} + +bool is_smt2_poly_formula( Expr* e ) +{ + if( e->getclass()==SYMS_EXPR ) + { + SymSExpr* s = (SymSExpr*)e; + static std::string eq("="); + static std::string distinct("distinct"); + return s->s==eq || s->s==distinct; + }else{ + return false; + } +} + +short get_mode( Expr* e ) +{ + if( e->getclass()==SYMS_EXPR ){ + SymSExpr* s = (SymSExpr*)e; + static std::string applys("apply"); + if ( s->s==applys ) return 1; + static std::string ands("and"); + if ( s->s==ands ) return 2; + static std::string ors("or"); + if ( s->s==ors ) return 3; + static std::string impls("impl"); + if ( s->s==impls ) return 4; + } + return 0; +} + +#endif diff --git a/proofs/lfsc_checker/print_smt2.h b/proofs/lfsc_checker/print_smt2.h new file mode 100644 index 000000000..c70b1dfa4 --- /dev/null +++ b/proofs/lfsc_checker/print_smt2.h @@ -0,0 +1,17 @@ +#ifndef PRINT_SMT2_H +#define PRINT_SMT2_H + +#define PRINT_SMT2 + +#include "expr.h" + +#ifdef PRINT_SMT2 +void print_smt2( Expr* p, std::ostream& s, short mode = 0 ); + +bool is_smt2_poly_formula( Expr* p ); +short get_mode( Expr* p ); + +#endif + + +#endif diff --git a/proofs/lfsc_checker/scccode.cpp b/proofs/lfsc_checker/scccode.cpp new file mode 100644 index 000000000..cff762a08 --- /dev/null +++ b/proofs/lfsc_checker/scccode.cpp @@ -0,0 +1,609 @@ +#include "scccode.h" + +Expr* e_pos; +Expr* e_neg; +Expr* e_tt; +Expr* e_ff; +Expr* e_cln; +Expr* e_clc; +Expr* e_concat; +Expr* e_clr; +Expr* e_litvar; +Expr* e_litpol; +Expr* e_notb; +Expr* e_iffb; +Expr* e_clear_mark; +Expr* e_append; +Expr* e_simplify_clause_h; +Expr* e_simplify_clause; + +void init_compiled_scc(){ + e_pos = symbols->get("pos").first; + e_neg = symbols->get("neg").first; + e_tt = symbols->get("tt").first; + e_ff = symbols->get("ff").first; + e_cln = symbols->get("cln").first; + e_clc = symbols->get("clc").first; + e_concat = symbols->get("concat").first; + e_clr = symbols->get("clr").first; + e_litvar = progs["litvar"]; + e_litpol = progs["litpol"]; + e_notb = progs["notb"]; + e_iffb = progs["iffb"]; + e_clear_mark = progs["clear_mark"]; + e_append = progs["append"]; + e_simplify_clause_h = progs["simplify_clause_h"]; + e_simplify_clause = progs["simplify_clause"]; +} + +Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args ){ + if( p==e_litvar ){ + return f_litvar( args[0] ); + }else if( p==e_litpol ){ + return f_litpol( args[0] ); + }else if( p==e_notb ){ + return f_notb( args[0] ); + }else if( p==e_iffb ){ + return f_iffb( args[0], args[1] ); + }else if( p==e_clear_mark ){ + return f_clear_mark( args[0] ); + }else if( p==e_append ){ + return f_append( args[0], args[1] ); + }else if( p==e_simplify_clause_h ){ + return f_simplify_clause_h( args[0], args[1] ); + }else if( p==e_simplify_clause ){ + return f_simplify_clause( args[0] ); + }else{ + return NULL; + } +} + +Expr* f_litvar( Expr* l ){ + Expr* e0; + l->inc(); + Expr* e1 = l->followDefs()->get_head(); + Expr* e2; + e2 = e_pos; + e2->inc(); + Expr* e3; + e3 = e_neg; + e3->inc(); + if( e1==e2 ){ + Expr* x = ((CExpr*)l->followDefs())->kids[1]; + e0 = x; + e0->inc(); + }else if( e1==e3 ){ + Expr* x = ((CExpr*)l->followDefs())->kids[1]; + e0 = x; + e0->inc(); + }else{ + std::cout << "Could not find match for expression in function f_litvar "; + e1->print( std::cout ); + std::cout << std::endl; + exit( 1 ); + } + l->dec(); + e2->dec(); + e3->dec(); + return e0; +} + +Expr* f_litpol( Expr* l ){ + Expr* e0; + l->inc(); + Expr* e1 = l->followDefs()->get_head(); + Expr* e2; + e2 = e_pos; + e2->inc(); + Expr* e3; + e3 = e_neg; + e3->inc(); + if( e1==e2 ){ + Expr* x = ((CExpr*)l->followDefs())->kids[1]; + e0 = e_tt; + e0->inc(); + }else if( e1==e3 ){ + Expr* x = ((CExpr*)l->followDefs())->kids[1]; + e0 = e_ff; + e0->inc(); + }else{ + std::cout << "Could not find match for expression in function f_litpol "; + e1->print( std::cout ); + std::cout << std::endl; + exit( 1 ); + } + l->dec(); + e2->dec(); + e3->dec(); + return e0; +} + +Expr* f_notb( Expr* b ){ + Expr* e0; + b->inc(); + Expr* e1 = b->followDefs()->get_head(); + Expr* e2; + e2 = e_ff; + e2->inc(); + Expr* e3; + e3 = e_tt; + e3->inc(); + if( e1==e2 ){ + e0 = e_tt; + e0->inc(); + }else if( e1==e3 ){ + e0 = e_ff; + e0->inc(); + }else{ + std::cout << "Could not find match for expression in function f_notb "; + e1->print( std::cout ); + std::cout << std::endl; + exit( 1 ); + } + b->dec(); + e2->dec(); + e3->dec(); + return e0; +} + +Expr* f_iffb( Expr* b1, Expr* b2 ){ + Expr* e0; + b1->inc(); + Expr* e1 = b1->followDefs()->get_head(); + Expr* e2; + e2 = e_tt; + e2->inc(); + Expr* e3; + e3 = e_ff; + e3->inc(); + if( e1==e2 ){ + e0 = b2; + e0->inc(); + }else if( e1==e3 ){ + b2->inc(); + e0 = f_notb( b2 ); + b2->dec(); + }else{ + std::cout << "Could not find match for expression in function f_iffb "; + e1->print( std::cout ); + std::cout << std::endl; + exit( 1 ); + } + b1->dec(); + e2->dec(); + e3->dec(); + return e0; +} + +Expr* f_clear_mark( Expr* v ){ + Expr* e0; + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(0)){ + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(0)) + ((SymExpr*)v->followDefs())->clearmark(0); + else + ((SymExpr*)v->followDefs())->setmark(0); + e0 = v; + e0->inc(); + v->dec(); + }else{ + e0 = v; + e0->inc(); + } + v->dec(); + return e0; +} + +Expr* f_append( Expr* c1, Expr* c2 ){ + Expr* e0; + c1->inc(); + Expr* e1 = c1->followDefs()->get_head(); + Expr* e2; + e2 = e_cln; + e2->inc(); + Expr* e3; + e3 = e_clc; + e3->inc(); + if( e1==e2 ){ + e0 = c2; + e0->inc(); + }else if( e1==e3 ){ + Expr* l = ((CExpr*)c1->followDefs())->kids[1]; + Expr* c1h = ((CExpr*)c1->followDefs())->kids[2]; + l->inc(); + Expr* e4; + c1h->inc(); + c2->inc(); + e4 = f_append( c1h, c2 ); + c1h->dec(); + c2->dec(); + static Expr* e5; + e5 = e_clc; + e5->inc(); + e0 = new CExpr( APP, e5, l, e4 ); + }else{ + std::cout << "Could not find match for expression in function f_append "; + e1->print( std::cout ); + std::cout << std::endl; + exit( 1 ); + } + c1->dec(); + e2->dec(); + e3->dec(); + return e0; +} + +Expr* f_simplify_clause_h( Expr* pol, Expr* c ){ + Expr* e0; + c->inc(); + Expr* e1 = c->followDefs()->get_head(); + Expr* e2; + e2 = e_cln; + e2->inc(); + Expr* e3; + e3 = e_clc; + e3->inc(); + Expr* e4; + e4 = e_concat; + e4->inc(); + Expr* e5; + e5 = e_clr; + e5->inc(); + if( e1==e2 ){ + e0 = e_cln; + e0->inc(); + }else if( e1==e3 ){ + Expr* l = ((CExpr*)c->followDefs())->kids[1]; + Expr* c1 = ((CExpr*)c->followDefs())->kids[2]; + Expr* v; + l->inc(); + v = f_litvar( l ); + l->dec(); + Expr* e6; + Expr* e7; + l->inc(); + e7 = f_litpol( l ); + l->dec(); + pol->inc(); + e6 = f_iffb( e7, pol ); + e7->dec(); + pol->dec(); + Expr* e8 = e6->followDefs()->get_head(); + Expr* e9; + e9 = e_tt; + e9->inc(); + Expr* e10; + e10 = e_ff; + e10->inc(); + if( e8==e9 ){ + Expr* m; + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(0)){ + m = e_tt; + m->inc(); + }else{ + Expr* e11; + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(0)) + ((SymExpr*)v->followDefs())->clearmark(0); + else + ((SymExpr*)v->followDefs())->setmark(0); + e11 = v; + e11->inc(); + v->dec(); + e11->dec(); + m = e_ff; + m->inc(); + } + v->dec(); + Expr* ch; + pol->inc(); + c1->inc(); + ch = f_simplify_clause_h( pol, c1 ); + pol->dec(); + c1->dec(); + m->inc(); + Expr* e12 = m->followDefs()->get_head(); + Expr* e13; + e13 = e_tt; + e13->inc(); + Expr* e14; + e14 = e_ff; + e14->inc(); + if( e12==e13 ){ + Expr* e15; + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(1)){ + e15 = v; + e15->inc(); + }else{ + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(1)) + ((SymExpr*)v->followDefs())->clearmark(1); + else + ((SymExpr*)v->followDefs())->setmark(1); + e15 = v; + e15->inc(); + v->dec(); + } + v->dec(); + e15->dec(); + e0 = ch; + e0->inc(); + }else if( e12==e14 ){ + Expr* e16; + Expr* e17; + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(1)){ + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(1)) + ((SymExpr*)v->followDefs())->clearmark(1); + else + ((SymExpr*)v->followDefs())->setmark(1); + e17 = v; + e17->inc(); + v->dec(); + }else{ + e17 = v; + e17->inc(); + } + v->dec(); + e17->dec(); + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(0)) + ((SymExpr*)v->followDefs())->clearmark(0); + else + ((SymExpr*)v->followDefs())->setmark(0); + e16 = v; + e16->inc(); + v->dec(); + e16->dec(); + l->inc(); + ch->inc(); + static Expr* e18; + e18 = e_clc; + e18->inc(); + e0 = new CExpr( APP, e18, l, ch ); + }else{ + std::cout << "Could not find match for expression in function f_simplify_clause_h "; + e12->print( std::cout ); + std::cout << std::endl; + exit( 1 ); + } + m->dec(); + e13->dec(); + e14->dec(); + ch->dec(); + m->dec(); + }else if( e8==e10 ){ + l->inc(); + Expr* e19; + pol->inc(); + c1->inc(); + e19 = f_simplify_clause_h( pol, c1 ); + pol->dec(); + c1->dec(); + static Expr* e20; + e20 = e_clc; + e20->inc(); + e0 = new CExpr( APP, e20, l, e19 ); + }else{ + std::cout << "Could not find match for expression in function f_simplify_clause_h "; + e8->print( std::cout ); + std::cout << std::endl; + exit( 1 ); + } + e6->dec(); + e9->dec(); + e10->dec(); + v->dec(); + }else if( e1==e4 ){ + Expr* c1 = ((CExpr*)c->followDefs())->kids[1]; + Expr* c2 = ((CExpr*)c->followDefs())->kids[2]; + pol->inc(); + Expr* e21 = pol->followDefs()->get_head(); + Expr* e22; + e22 = e_ff; + e22->inc(); + Expr* e23; + e23 = e_tt; + e23->inc(); + if( e21==e22 ){ + Expr* e24; + pol->inc(); + c1->inc(); + e24 = f_simplify_clause_h( pol, c1 ); + pol->dec(); + c1->dec(); + Expr* e25; + pol->inc(); + c2->inc(); + e25 = f_simplify_clause_h( pol, c2 ); + pol->dec(); + c2->dec(); + static Expr* e26; + e26 = e_concat; + e26->inc(); + e0 = new CExpr( APP, e26, e24, e25 ); + }else if( e21==e23 ){ + Expr* e27; + pol->inc(); + c1->inc(); + e27 = f_simplify_clause_h( pol, c1 ); + pol->dec(); + c1->dec(); + Expr* e28; + pol->inc(); + c2->inc(); + e28 = f_simplify_clause_h( pol, c2 ); + pol->dec(); + c2->dec(); + e0 = f_append( e27, e28 ); + e27->dec(); + e28->dec(); + }else{ + std::cout << "Could not find match for expression in function f_simplify_clause_h "; + e21->print( std::cout ); + std::cout << std::endl; + exit( 1 ); + } + pol->dec(); + e22->dec(); + e23->dec(); + }else if( e1==e5 ){ + Expr* l = ((CExpr*)c->followDefs())->kids[1]; + Expr* c1 = ((CExpr*)c->followDefs())->kids[2]; + Expr* e29; + Expr* e30; + l->inc(); + e30 = f_litpol( l ); + l->dec(); + pol->inc(); + e29 = f_iffb( e30, pol ); + e30->dec(); + pol->dec(); + Expr* e31 = e29->followDefs()->get_head(); + Expr* e32; + e32 = e_ff; + e32->inc(); + Expr* e33; + e33 = e_tt; + e33->inc(); + if( e31==e32 ){ + l->inc(); + Expr* e34; + pol->inc(); + c1->inc(); + e34 = f_simplify_clause_h( pol, c1 ); + pol->dec(); + c1->dec(); + static Expr* e35; + e35 = e_clr; + e35->inc(); + e0 = new CExpr( APP, e35, l, e34 ); + }else if( e31==e33 ){ + Expr* v; + l->inc(); + v = f_litvar( l ); + l->dec(); + Expr* m; + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(0)){ + m = e_tt; + m->inc(); + }else{ + Expr* e36; + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(0)) + ((SymExpr*)v->followDefs())->clearmark(0); + else + ((SymExpr*)v->followDefs())->setmark(0); + e36 = v; + e36->inc(); + v->dec(); + e36->dec(); + m = e_ff; + m->inc(); + } + v->dec(); + Expr* ch; + pol->inc(); + c1->inc(); + ch = f_simplify_clause_h( pol, c1 ); + pol->dec(); + c1->dec(); + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(1)){ + m->inc(); + Expr* e37 = m->followDefs()->get_head(); + Expr* e38; + e38 = e_tt; + e38->inc(); + Expr* e39; + e39 = e_ff; + e39->inc(); + if( e37==e38 ){ + e0 = ch; + e0->inc(); + }else if( e37==e39 ){ + Expr* e40; + Expr* e41; + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(1)) + ((SymExpr*)v->followDefs())->clearmark(1); + else + ((SymExpr*)v->followDefs())->setmark(1); + e41 = v; + e41->inc(); + v->dec(); + e41->dec(); + v->inc(); + if ( ((SymExpr*)v->followDefs())->getmark(0)) + ((SymExpr*)v->followDefs())->clearmark(0); + else + ((SymExpr*)v->followDefs())->setmark(0); + e40 = v; + e40->inc(); + v->dec(); + e40->dec(); + e0 = ch; + e0->inc(); + }else{ + std::cout << "Could not find match for expression in function f_simplify_clause_h "; + e37->print( std::cout ); + std::cout << std::endl; + exit( 1 ); + } + m->dec(); + e38->dec(); + e39->dec(); + }else{ + e0 = NULL; + } + v->dec(); + ch->dec(); + m->dec(); + v->dec(); + }else{ + std::cout << "Could not find match for expression in function f_simplify_clause_h "; + e31->print( std::cout ); + std::cout << std::endl; + exit( 1 ); + } + e29->dec(); + e32->dec(); + e33->dec(); + }else{ + std::cout << "Could not find match for expression in function f_simplify_clause_h "; + e1->print( std::cout ); + std::cout << std::endl; + exit( 1 ); + } + c->dec(); + e2->dec(); + e3->dec(); + e4->dec(); + e5->dec(); + return e0; +} + +Expr* f_simplify_clause( Expr* c ){ + Expr* e0; + static Expr* e1; + e1 = e_tt; + e1->inc(); + Expr* e2; + static Expr* e3; + e3 = e_ff; + e3->inc(); + c->inc(); + e2 = f_simplify_clause_h( e3, c ); + e3->dec(); + c->dec(); + e0 = f_simplify_clause_h( e1, e2 ); + e1->dec(); + e2->dec(); + return e0; +} + diff --git a/proofs/lfsc_checker/scccode.h b/proofs/lfsc_checker/scccode.h new file mode 100644 index 000000000..6f5efc8b5 --- /dev/null +++ b/proofs/lfsc_checker/scccode.h @@ -0,0 +1,27 @@ +#ifndef SCC_CODE_H +#define SCC_CODE_H + +#include "check.h" + +void init_compiled_scc(); + +Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args ); + +inline Expr* f_litvar( Expr* l ); + +inline Expr* f_litpol( Expr* l ); + +inline Expr* f_notb( Expr* b ); + +inline Expr* f_iffb( Expr* b1, Expr* b2 ); + +inline Expr* f_clear_mark( Expr* v ); + +inline Expr* f_append( Expr* c1, Expr* c2 ); + +inline Expr* f_simplify_clause_h( Expr* pol, Expr* c ); + +inline Expr* f_simplify_clause( Expr* c ); + +#endif + diff --git a/proofs/lfsc_checker/sccwriter.cpp b/proofs/lfsc_checker/sccwriter.cpp new file mode 100644 index 000000000..d11a96b19 --- /dev/null +++ b/proofs/lfsc_checker/sccwriter.cpp @@ -0,0 +1,977 @@ +#include "sccwriter.h" + +#include +#include + +int sccwriter::exprCount = 0; +int sccwriter::strCount = 0; +int sccwriter::argsCount = 0; +int sccwriter::rnumCount = 0; + +int sccwriter::get_prog_index( const std::string& str ) +{ + for( int a=0; a<(int)progNames.size(); a++ ){ + if( progNames[a]==str ){ + return a; + } + } + return -1; +} + +int sccwriter::get_prog_index_by_expr( Expr* e ) +{ + for( int a=0; a<(int)progPtrs.size(); a++ ){ + if( progPtrs[a]==e ){ + return a; + } + } + return -1; +} + +bool sccwriter::is_var( const std::string& str ) +{ + for( int a=0; a<(int)vars.size(); a++ ){ + if( vars[a]==str ){ + return true; + } + } + return false; +} + +void sccwriter::add_global_sym( const std::string& str ) +{ + for( int a=0; a<(int)globalSyms.size(); a++ ){ + if( globalSyms[a]==str ){ + return; + } + } + globalSyms.push_back( str ); +} + +void sccwriter::indent( std::ostream& os, int ind ) +{ + for( int a=0; akids[1]; + int counter = 0; + //write each argument + while( progvars->kids[counter] ) + { + if( counter!=0 ) + { + os << ", "; + } + os << "Expr* "; + write_variable( ((SymSExpr*)progvars->kids[counter])->s, os ); + //add to vars if options are set to do so + if( opts&opt_write_add_args ) + { + vars.push_back( ((SymSExpr*)progvars->kids[counter])->s ); + } + counter++; + } + os << " )"; + if( opts&opt_write_call_debug ) + { + os << "{" << std::endl; + indent( os, 1 ); + os << "std::cout << \"Call function " << fname.c_str() << " with arguments \";" << std::endl; + counter = 0; + while( progvars->kids[counter] ) + { + if( counter!=0 ) + { + indent( os, 1 ); + os << "std::cout << \", \";" << std::endl; + } + indent( os, 1 ); + write_variable( ((SymSExpr*)progvars->kids[counter])->s, os ); + os << "->print( std::cout );" << std::endl; + counter++; + } + indent( os, 1 ); + os << "std::cout << std::endl;" << std::endl; + } +} + +void sccwriter::get_function_name( const std::string& pname, std::string& fname ) +{ + fname = std::string( "f_" ); + fname.append( pname ); +} + +void sccwriter::write_variable( const std::string& n, std::ostream& os ) +{ + std::string nn; + get_var_name( n, nn ); + os << nn.c_str(); +} + +void sccwriter::get_var_name( const std::string& n, std::string& nn ) { + nn = std::string( n.c_str() ); + for( int i = 0; i <(int)n.length(); i++ ){ + char c = n[i]; + if (c <= 47) + c += 65; + else if (c >= 58 && c <= 64) + c += 97-58; + if ((c >= 91 && c <= 94) || c == 96) + c += 104-91; + else if (c >= 123) + c -= 4; + nn[i] = c; + } +} + +void sccwriter::write_file() +{ + static std::string filename( "scccode" ); + + //writer the h file + std::fstream fsh; + std::string fnameh( filename ); + fnameh.append(".h"); + fsh.open( fnameh.c_str(), std::ios::out ); + //write the header in h + fsh << "#ifndef SCC_CODE_H" << std::endl; + fsh << "#define SCC_CODE_H" << std::endl << std::endl; + //include necessary files in h file + fsh << "#include \"check.h\"" << std::endl << std::endl; + //write the init function + fsh << "void init_compiled_scc();" << std::endl << std::endl; + //write the entry function + fsh << "Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args );" << std::endl << std::endl; + //write the side condition code functions + for( int n=0; n<(int)progs.size(); n++ ) + { + //write the header in the h file + fsh << "inline "; + write_function_header( fsh, n ); + fsh << ";" << std::endl << std::endl; + } + fsh << "#endif" << std::endl << std::endl; + fsh.close(); + + + //writer the cpp code + std::fstream fsc; + std::string fnamec( filename ); + fnamec.append(".cpp"); + fsc.open( fnamec.c_str(), std::ios::out ); + //include the h file in the cpp + fsc << "#include \"scccode.h\"" << std::endl << std::endl; + std::ostringstream fsc_funcs; + //write the side condition code functions + for( currProgram=0; currProgram<(int)progs.size(); currProgram++ ) + { + //reset naming counters + vars.clear(); + exprCount = 0; + strCount = 0; + argsCount = 0; + rnumCount = 0; + + //for debugging + std::cout << "program #" << currProgram << " " << progNames[currProgram].c_str() << std::endl; + + //write the function header + write_function_header( fsc_funcs, currProgram, opt_write_add_args|options ); + if( (options&opt_write_call_debug)==0 ) + { + fsc_funcs << "{" << std::endl; + } + //write the code + //std::vector< std::string > cleanVec; + //write_code( get_prog( n )->kids[2], fsc, 1, "return ", cleanVec ); + //debug_write_code( progs[n].second->kids[2], fsc, 1 ); + std::string expr; + write_expr( get_prog( currProgram )->kids[2], fsc_funcs, 1, expr ); + indent( fsc_funcs, 1 ); + fsc_funcs << "return " << expr.c_str() << ";" << std::endl; + fsc_funcs << "}" << std::endl << std::endl; + } + //write the predefined symbols necessary - symbols and progs + for( int a=0; a<(int)globalSyms.size(); a++ ) + { + fsc << "Expr* e_" << globalSyms[a].c_str() << ";" << std::endl; + } + for( int a=0; a<(int)progs.size(); a++ ) + { + fsc << "Expr* e_" << progNames[a].c_str() << ";" << std::endl; + } + fsc << std::endl; + //write the init function - initialize symbols and progs + fsc << "void init_compiled_scc(){" << std::endl; + for( int a=0; a<(int)globalSyms.size(); a++ ) + { + indent( fsc, 1 ); + fsc << "e_" << globalSyms[a].c_str() << " = symbols->get(\"" << globalSyms[a].c_str() << "\").first;" << std::endl; + } + for( int a=0; a<(int)progs.size(); a++ ) + { + indent( fsc, 1 ); + fsc << "e_" << progNames[a].c_str() << " = progs[\"" << progNames[a].c_str() << "\"];" << std::endl; + } + fsc << "}" << std::endl << std::endl; + fsc << "Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args ){" << std::endl; + //for( int n=0; n<(int)progs.size(); n++ ){ + // indent( fsc, 1 ); + // fsc << "static std::string s_" << progNames[n].c_str() << " = std::string( \"" << progNames[n].c_str() << "\" );" << std::endl; + //} + for( int n=0; n<(int)progs.size(); n++ ){ + indent( fsc, 1 ); + if( n!=0 ){ + fsc << "}else "; + } + //for each function, test to see if the string matches the name of the function + fsc << "if( p==e_" << progNames[n].c_str() << " ){" << std::endl; + indent( fsc, 2 ); + std::string fname; + get_function_name( progNames[n], fname ); + //map the function to the proper function + fsc << "return " << fname.c_str() << "( "; + //write the arguments to the function from args + CExpr* progvars = (CExpr*)get_prog( n )->kids[1]; + int counter = 0; + bool firstTime = true; + while( progvars->kids[counter] ) + { + if( !firstTime ) + { + fsc << ", "; + } + fsc << "args[" << counter << "]"; + firstTime = false; + counter++; + } + fsc << " );" << std::endl; + } + indent( fsc, 1 ); + fsc << "}else{" << std::endl; + indent( fsc, 2 ); + //return null in the case the function could not be found + fsc << "return NULL;" << std::endl; + indent( fsc, 1 ); + fsc << "}" << std::endl; + fsc << "}" << std::endl << std::endl; + fsc << fsc_funcs.str().c_str(); + + fsc.close(); +} + +void sccwriter::write_code( Expr* code, std::ostream& os, int ind, const char* retModStr, int opts ) +{ + std::string retModString; + std::string incString; + if ( retModStr ) + { + retModString = std::string( retModStr ); + retModString.append( " = " ); + incString = std::string( retModStr ); + incString.append( "->inc();" ); + } + switch( code->getclass() ) + { + case INT_EXPR: + { + indent( os, ind ); + os << retModString.c_str(); + os << "new IntExpr( " << mpz_get_si( ((IntExpr*)code)->n ) << " );" << std::endl; + indent( os, ind ); + os << incString.c_str() << std::endl; + } + break; + case RAT_EXPR: + { + mpz_t num, den; + mpz_init(num); + mpz_init(den); + mpq_get_num( num, ((RatExpr*)code)->n ); + mpq_get_den( den, ((RatExpr*)code)->n ); + indent( os, ind ); + os << retModString.c_str(); + os << "new RatExpr( " << mpz_get_si( num ) << ", " << mpz_get_si( den ) << " );" << std::endl; + indent( os, ind ); + os << incString.c_str() << std::endl; + } + break; + case SYMS_EXPR: + { + //if it is a variable, simply write it to buffer + if( is_var( ((SymSExpr*)code)->s ) ) + { + indent( os, ind ); + os << retModString.c_str(); + write_variable( ((SymSExpr*)code)->s.c_str(), os ); + os << ";" << std::endl; + } + else //else must look at symbol lookup table + { + std::string var; + get_var_name( ((SymSExpr*)code)->s, var ); + indent( os, ind ); + os << retModString.c_str() << "e_" << var.c_str() << ";" << std::endl; + add_global_sym( var ); + } + indent( os, ind ); + os << incString.c_str() << std::endl; + } + break; + default: + switch( code->getop() ) + { + case APP: + { + //collect the arguments + std::vector< Expr* > argVector; + code->collect_args( argVector ); + //write the arguments + std::vector< std::string > args; + for( int a=0; a<(int)argVector.size(); a++ ) + { + std::string expr; + write_expr( argVector[a], os, ind, expr ); + args.push_back( expr ); + } + //write_args( (CExpr*)code, os, ind, 1, args ); + Expr* hd = code->get_head(); + //map to a program in the case that it is a program + if( hd->getop()==PROG && get_prog_index_by_expr( hd )!=-1 ) + { + indent( os, ind ); + os << retModString << "f_" << progNames[ get_prog_index_by_expr( hd ) ].c_str() << "( "; + for( int a=0; a<(int)args.size(); a++ ) + { + os << args[a].c_str(); + if( a!=(int)( args.size()-1 ) ){ + os << ", "; + } + } + os << " );" << std::endl; + for( int a=0; a<(int)args.size(); a++ ) + { + write_dec( args[a], os, ind ); + } + } + else + { +#ifdef USE_FLAT_APP + std::string expr; + write_expr( hd, os, ind, expr ); + indent( os, ind ); + os << retModString << "new CExpr( APP, "; + os << expr.c_str() << ", "; + for( int a=0; a<(int)args.size(); a++ ) + { + os << args[a].c_str(); + if( a!=(int)( args.size()-1 ) ){ + os << ", "; + } + } + os << " );" << std::endl; +#else + std::string expr; + write_expr( hd, os, ind, expr ); + indent( os, ind ); + os << retModString; + for( int a=0; a<(int)args.size(); a++ ) + { + os << "new CExpr( APP, "; + } + os << expr.c_str() << ", "; + for( int a=0; a<(int)args.size(); a++ ) + { + os << args[a].c_str(); + os << " )"; + if( a!=(int)( args.size()-1 ) ){ + os << ", "; + } + } + os << ";" << std::endl; +#endif + //indent( os, ind ); + //os << expr.c_str() << "->dec();" << std::endl; + } + } + break; + case MATCH: + { + //calculate the value for the expression + std::string expr; + write_expr( ((CExpr*)code)->kids[0], os, ind, expr ); + //get the head + std::ostringstream sshd; + sshd << "e" << exprCount; + exprCount++; + indent( os, ind ); + os << "Expr* " << sshd.str().c_str() << " = " << expr.c_str() << "->followDefs()->get_head();" << std::endl; + //write the arguments + std::vector< std::string > args; + write_args( (CExpr*)code, os, ind, 1, args ); + bool encounterDefault = false; + //now make an if statement corresponding to the match + int a = 0; + while( ((CExpr*)code)->kids[a+1] ) + { + indent( os, ind ); + if( a!=0 ){ + os << "}else"; + } + if( ((CExpr*)code)->kids[a+1]->getop()!=CASE ){ + encounterDefault = true; + os << "{" << std::endl; + //write the body of the case + write_code( ((CExpr*)code)->kids[a+1], os, ind+1, retModStr ); + indent( os, ind ); + os << "}" << std::endl; + }else{ + if( a!=0 ) + os << " "; + os << "if( " << sshd.str().c_str() << "==" << args[a].c_str() << " ){" << std::endl; + //collect args from the variable in the code + std::ostringstream ssargs; + ssargs << "args" << argsCount; + argsCount++; +#ifndef USE_FLAT_APP + indent( os, ind+1 ); + os << "std::vector< Expr* > " << ssargs.str().c_str() << ";" << std::endl; + indent( os, ind+1 ); + os << expr.c_str() << "->followDefs()->collect_args( " << ssargs.str().c_str() << " );" << std::endl; +#endif + //set the variables defined in the pattern equal to the arguments + std::vector< Expr* > caseArgs; + ((CExpr*)((CExpr*)code)->kids[a+1])->kids[0]->collect_args( caseArgs ); + for( int b=0; b<(int)caseArgs.size(); b++ ) + { + indent( os, ind+1 ); + os << "Expr* "; + write_variable( ((SymSExpr*)caseArgs[b])->s.c_str(), os ); +#ifdef USE_FLAT_APP + os << " = ((CExpr*)" << expr.c_str() << "->followDefs())->kids[" << b+1 << "];" << std::endl; +#else + os << " = " << ssargs.str().c_str() << "[" << b << "];" << std::endl; +#endif + vars.push_back( ((SymSExpr*)caseArgs[b])->s ); + } + //write the body of the case + write_code( ((CExpr*)code)->kids[a+1], os, ind+1, retModStr, opt_write_case_body ); + } + a++; + } + if( !encounterDefault ) + { + indent( os, ind ); + os << "}else{" << std::endl; + indent( os, ind + 1 ); + os << "std::cout << \"Could not find match for expression in function f_"; + os << progNames[currProgram].c_str() << " \";" << std::endl; + indent( os, ind + 1 ); + os << sshd.str().c_str() << "->print( std::cout );" << std::endl; + indent( os, ind + 1 ); + os << "std::cout << std::endl;" << std::endl; + indent( os, ind + 1 ); + os << "exit( 1 );" << std::endl; + indent( os, ind ); + os << "}" << std::endl; + } + write_dec( expr, os, ind ); + for( int a=0; a<(int)args.size(); a++ ) + { + write_dec( args[a], os, ind ); + } + } + break; + case CASE: + if( opts&opt_write_case_body ) + { + write_code( ((CExpr*)code)->kids[1], os, ind, retModStr ); + } + else + { + write_code( ((CExpr*)code)->kids[0]->get_head(), os, ind, retModStr ); + } + break; + case DO: + { + //write each of the children in sequence + int counter = 0; + while( ((CExpr*)code)->kids[counter] ) + { + if( ((CExpr*)code)->kids[counter+1]==NULL ) + { + write_code( ((CExpr*)code)->kids[counter], os, ind, retModStr ); + } + else + { + std::string expr; + write_expr( ((CExpr*)code)->kids[counter], os, ind, expr ); + //clean up memory + write_dec( expr, os, ind ); + } + counter++; + } + } + break; + case LET: + { + indent( os, ind ); + os << "Expr* "; + write_variable( ((SymSExpr*)((CExpr*)code)->kids[0])->s, os ); + os << ";" << std::endl; + std::ostringstream ss; + write_variable( ((SymSExpr*)((CExpr*)code)->kids[0])->s, ss ); + write_code( ((CExpr*)code)->kids[1], os, ind, ss.str().c_str() ); + //add it to the variables + vars.push_back( ((SymSExpr*)((CExpr*)code)->kids[0])->s ); + write_code( ((CExpr*)code)->kids[2], os, ind, retModStr ); + //clean up memory + indent( os, ind ); + write_variable( ((SymSExpr*)((CExpr*)code)->kids[0])->s, os ); + os << "->dec();" << std::endl; + } + break; + case FAIL: + { + indent( os, ind ); + os << retModString.c_str() << "NULL;" << std::endl; + } + break; +#ifndef MARKVAR_32 + case MARKVAR: + { + //calculate the value for the expression + std::string expr; + write_expr( ((CExpr*)code)->kids[0], os, ind, expr, opt_write_check_sym_expr ); + //set the mark on the expression + indent( os, ind ); + os << "if (" << expr.c_str() << "->followDefs()->getmark())" << std::endl; + indent( os, ind+1 ); + os << expr.c_str() << "->followDefs()->clearmark();" << std::endl; + indent( os, ind ); + os << "else" << std::endl; + indent( os, ind+1 ); + os << expr.c_str() << "->followDefs()->setmark();" << std::endl; + //write the return if necessary + if( retModStr!=NULL ){ + indent( os, ind ); + os << retModString.c_str() << expr.c_str() << ";" << std::endl; + indent( os, ind ); + os << incString.c_str() << std::endl; + } + write_dec( expr, os, ind ); + } + break; + case IFMARKED: + { + //calculate the value for the expression + std::string expr; + write_expr( ((CExpr*)code)->kids[0], os, ind, expr, opt_write_check_sym_expr ); + //if mark is set, write code for kids[1] + indent( os, ind ); + os << "if (" << expr.c_str() << "->followDefs()->getmark()){" << std::endl; + write_code( ((CExpr*)code)->kids[1], os, ind+1, retModStr ); + //else write code for kids[2] + indent( os, ind ); + os << "}else{" << std::endl; + write_code( ((CExpr*)code)->kids[2], os, ind+1, retModStr ); + indent( os, ind ); + os << "}" << std::endl; + //clean up memory + write_dec( expr, os, ind ); + } + break; +#else + case MARKVAR: + { + //calculate the value for the expression + std::string expr; + write_expr( ((CExpr*)code)->kids[1], os, ind, expr, opt_write_check_sym_expr ); + //set the mark on the expression + indent( os, ind ); + os << "if ( ((SymExpr*)" << expr.c_str() << "->followDefs())->getmark("; + os << ((IntExpr*)((CExpr*)code)->kids[0])->get_num() << "))" << std::endl; + indent( os, ind+1 ); + os << "((SymExpr*)" << expr.c_str() << "->followDefs())->clearmark("; + os << ((IntExpr*)((CExpr*)code)->kids[0])->get_num() << ");" << std::endl; + indent( os, ind ); + os << "else" << std::endl; + indent( os, ind+1 ); + os << "((SymExpr*)" << expr.c_str() << "->followDefs())->setmark("; + os << ((IntExpr*)((CExpr*)code)->kids[0])->get_num() << ");" << std::endl; + //write the return if necessary + if( retModStr!=NULL ){ + indent( os, ind ); + os << retModString.c_str() << expr.c_str() << ";" << std::endl; + indent( os, ind ); + os << incString.c_str() << std::endl; + } + write_dec( expr, os, ind ); + } + break; + case COMPARE: + { + std::string expr1, expr2; + write_expr( ((CExpr*)code)->kids[0], os, ind, expr1, opt_write_check_sym_expr ); + write_expr( ((CExpr*)code)->kids[1], os, ind, expr2, opt_write_check_sym_expr ); + indent( os, ind ); + os << "if( ((SymExpr*)" << expr1.c_str() << ")->followDefs() < ((SymExpr*)" << expr2.c_str() << ")->followDefs() ){" << std::endl; + write_code( ((CExpr*)code)->kids[2], os, ind+1, retModStr ); + indent( os, ind ); + os << "}else{" << std::endl; + write_code( ((CExpr*)code)->kids[3], os, ind+1, retModStr ); + indent( os, ind ); + os << "}" << std::endl; + //clean up memory + write_dec( expr1, os, ind ); + write_dec( expr2, os, ind ); + } + break; + case IFMARKED: + { + //calculate the value for the expression + std::string expr; + write_expr( ((CExpr*)code)->kids[1], os, ind, expr, opt_write_check_sym_expr ); + //if mark is set, write code for kids[1] + indent( os, ind ); + os << "if ( ((SymExpr*)" << expr.c_str() << "->followDefs())->getmark("; + os << ((IntExpr*)((CExpr*)code)->kids[0])->get_num() << ")){" << std::endl; + write_code( ((CExpr*)code)->kids[2], os, ind+1, retModStr ); + //else write code for kids[2] + indent( os, ind ); + os << "}else{" << std::endl; + write_code( ((CExpr*)code)->kids[3], os, ind+1, retModStr ); + indent( os, ind ); + os << "}" << std::endl; + //clean up memory + write_dec( expr, os, ind ); + } + break; +#endif + case ADD: + case MUL: + case DIV: + { + //calculate the value for the first expression + std::string expr1; + write_expr( ((CExpr*)code)->kids[0], os, ind, expr1 ); + //calculate the value for the second expression + std::string expr2; + write_expr( ((CExpr*)code)->kids[1], os, ind, expr2 ); + std::ostringstream ss; + ss << "rnum" << rnumCount; + rnumCount++; + indent( os, ind ); + os << "if( " << expr1.c_str() << "->followDefs()->getclass()==INT_EXPR ){" << std::endl; + indent( os, ind+1 ); + os << "mpz_t " << ss.str().c_str() << ";" << std::endl; + indent( os, ind+1 ); + os << "mpz_init(" << ss.str().c_str() << ");" << std::endl; + indent( os, ind+1 ); + os << "mpz_"; + if( code->getop()==ADD ) + os << "add"; + else + os << "mul"; + os << "( " << ss.str().c_str() << ", ((IntExpr*)" << expr1.c_str() << "->followDefs())->n, ((IntExpr*)" << expr2.c_str() << "->followDefs())->n);" << std::endl; + indent( os, ind+1 ); + os << retModString.c_str() << "new IntExpr(" << ss.str().c_str() << ");" << std::endl; + indent( os, ind ); + os << "}else if( " << expr1.c_str() << "->followDefs()->getclass()==RAT_EXPR ){" << std::endl; + indent( os, ind+1 ); + os << "mpq_t " << ss.str().c_str() << ";" << std::endl; + indent( os, ind+1 ); + os << "mpq_init(" << ss.str().c_str() << ");" << std::endl; + indent( os, ind+1 ); + os << "mpq_"; + if( code->getop()==ADD ) + os << "add"; + else if( code->getop()==MUL ) + os << "mul"; + else + os << "div"; + os << "( " << ss.str().c_str() << ", ((RatExpr*)" << expr1.c_str() << "->followDefs())->n, ((RatExpr*)" << expr2.c_str() << "->followDefs())->n);" << std::endl; + indent( os, ind+1 ); + os << retModString.c_str() << "new RatExpr(" << ss.str().c_str() << ");" << std::endl; + indent( os, ind ); + os << "}" << std::endl; + //clean up memory + write_dec( expr1, os, ind ); + write_dec( expr2, os, ind ); + } + break; + case NEG: + { + //calculate the value for the first expression + std::string expr1; + write_expr( ((CExpr*)code)->kids[0], os, ind, expr1 ); + std::ostringstream ss; + ss << "rnum" << rnumCount; + rnumCount++; + indent( os, ind ); + os << "if( " << expr1.c_str() << "->followDefs()->getclass()==INT_EXPR ){" << std::endl; + indent( os, ind+1 ); + os << "mpz_t " << ss.str().c_str() << ";" << std::endl; + indent( os, ind+1 ); + os << "mpz_init(" << ss.str().c_str() << ");" << std::endl; + indent( os, ind+1 ); + os << "mpz_neg( " << ss.str().c_str() << ", ((IntExpr*)" << expr1.c_str() << "->followDefs())->n );" << std::endl; + indent( os, ind+1 ); + os << retModString.c_str() << "new IntExpr(" << ss.str().c_str() << ");" << std::endl; + indent( os, ind ); + os << "}else if( " << expr1.c_str() << "->followDefs()->getclass()==RAT_EXPR ){" << std::endl; + indent( os, ind+1 ); + os << "mpq_t " << ss.str().c_str() << ";" << std::endl; + indent( os, ind+1 ); + os << "mpq_init(" << ss.str().c_str() << ");" << std::endl; + indent( os, ind+1 ); + os << "mpq_neg( " << ss.str().c_str() << ", ((RatExpr*)" << expr1.c_str() << "->followDefs())->n );" << std::endl; + indent( os, ind+1 ); + os << retModString.c_str() << "new RatExpr(" << ss.str().c_str() << ");" << std::endl; + indent( os, ind ); + os << "}" << std::endl; + //clean up memory + write_dec( expr1, os, ind ); + } + break; + case IFNEG: + case IFZERO: + { + std::string expr1; + write_expr( ((CExpr*)code)->kids[0], os, ind, expr1 ); + indent( os, ind ); + os << "if( " << expr1.c_str() << "->followDefs()->getclass()==INT_EXPR ){" << std::endl; + indent( os, ind+1 ); + os << "if( mpz_sgn( ((IntExpr *)" << expr1.c_str() << "->followDefs())->n ) "; + if( code->getop()==IFNEG ) + os << "<"; + else + os << "=="; + os << " 0 ){" << std::endl; + write_code( ((CExpr*)code)->kids[1], os, ind+2, retModStr ); + indent( os, ind+1 ); + os << "}else{" << std::endl; + write_code( ((CExpr*)code)->kids[2], os, ind+2, retModStr ); + indent( os, ind+1 ); + os << "}" << std::endl; + indent( os, ind ); + os << "}else if( " << expr1.c_str() << "->followDefs()->getclass()==RAT_EXPR ){" << std::endl; + indent( os, ind+1 ); + os << "if( mpq_sgn( ((RatExpr *)" << expr1.c_str() << "->followDefs())->n ) "; + if( code->getop()==IFNEG ) + os << "<"; + else + os << "=="; + os << " 0 ){" << std::endl; + write_code( ((CExpr*)code)->kids[1], os, ind+2, retModStr ); + indent( os, ind+1 ); + os << "}else{" << std::endl; + write_code( ((CExpr*)code)->kids[2], os, ind+2, retModStr ); + indent( os, ind+1 ); + os << "}" << std::endl; + indent( os, ind ); + os << "}" << std::endl; + //clean up memory + write_dec( expr1, os, ind ); + } + break; + case RUN:/*?*/break; + case PI:/*?*/break; + case LAM:/*?*/break; + case TYPE:/*?*/break; + case KIND:/*?*/break; + case ASCRIBE:/*?*/break; + case MPZ:/*?*/break; + case PROG:/*?*/break; + case PROGVARS:/*?*/break; + case PAT:/*?*/break; + } + break; + } +} + +void sccwriter::write_args( CExpr* code, std::ostream& os, int ind, int childCounter, + std::vector< std::string >& args, int opts ) +{ + bool encounterCase = false; + while( code->kids[childCounter] && + (!encounterCase || code->kids[childCounter]->getop()==CASE ) ) + { + encounterCase = encounterCase || code->kids[childCounter]->getop()==CASE; + if( code->kids[childCounter]->getclass()==SYMS_EXPR ) + { + args.push_back( ((SymSExpr*)code->kids[childCounter])->s ); + } + else + { + //calculate the value for the argument + std::string expr; + write_expr( code->kids[childCounter], os, ind, expr, opts ); + args.push_back( expr ); + } + childCounter++; + } +} + +void sccwriter::write_expr( Expr* code, std::ostream& os, int ind, std::string& expr, int opts ) +{ + if( code->getclass()==SYMS_EXPR && is_var( ((SymSExpr*)code)->s ) ) + { + get_var_name( ((SymSExpr*)code)->s, expr ); + indent( os, ind ); + os << expr.c_str() << "->inc();" << std::endl; + } + else + { + std::ostringstream ss; + ss << "e" << exprCount; + exprCount++; + //declare the expression + indent( os, ind ); + if( code->getclass()==SYMS_EXPR && !is_var( ((SymSExpr*)code)->s ) ) + { + os << "static "; + } + os << "Expr* " << ss.str().c_str() << ";" << std::endl; + //write the expression + std::ostringstream ss2; + ss2 << ss.str().c_str(); + write_code( code, os, ind, ss2.str().c_str(), opts ); + + //if is not a sym expression, then decrement the expression and return null + if( opts&opt_write_check_sym_expr ) + { + indent( os, ind ); + os << "if (" << expr.c_str() << "->getclass() != SYM_EXPR) {" << std::endl; + indent( os, ind+1 ); + os << "exit( 1 );" << std::endl; + indent( os, ind ); + os << "}" << std::endl; + } + + expr = std::string( ss.str().c_str() ); + vars.push_back( expr ); + } + //increment the counter for memory management + //indent( os, ind ); + //os << expr.c_str() << "->inc();" << std::endl; +} + +void sccwriter::write_dec( const std::string& expr, std::ostream& os, int ind ) +{ + bool wd = true; + if( wd ) + { + indent( os, ind ); + os << expr.c_str() << "->dec();" << std::endl; + } +} + +void sccwriter::debug_write_code( Expr* code, std::ostream& os, int ind ) +{ + indent( os, ind ); + switch( code->getclass() ) + { + case INT_EXPR: + os << "int_expr"; + break; + case HOLE_EXPR: + os << "hole_expr"; + break; + case SYM_EXPR: + os << "sym_expr"; + break; + case SYMS_EXPR: + os << "syms_expr: " << ((SymSExpr*)code)->s.c_str(); + break; + default: + switch( code->getop() ) + { + case APP: + os << "app"; + break; + case PI: + os << "pi"; + break; + case LAM: + os << "lam"; + break; + case TYPE: + os << "type"; + break; + case KIND: + os << "kind"; + break; + case ASCRIBE: + os << "ascribe"; + break; + case MPZ: + os << "mpz"; + break; + case PROG: + os << "prog"; + break; + case PROGVARS: + os << "progvars"; + break; + case MATCH: + os << "match"; + break; + case CASE: + os << "case"; + break; + case PAT: + os << "pat"; + break; + case DO: + os << "do"; + break; + case ADD: + os << "add"; + break; + case NEG: + os << "neg"; + break; + case LET: + os << "let"; + break; + case RUN: + os << "run"; + break; + case FAIL: + os << "fail"; + break; + case MARKVAR: + os << "markvar"; + break; + case IFMARKED: + os << "ifmarked"; + break; + case COMPARE: + os << "compare"; + break; + default: + os << "???"; + break; + } + } + os << std::endl; + if( code->getop()!=0 ) + { + CExpr* ce = (CExpr*)code; + int counter = 0; + while( ce->kids[counter] ){ + debug_write_code( ce->kids[counter], os, ind+1 ); + counter++; + } + } +} diff --git a/proofs/lfsc_checker/sccwriter.h b/proofs/lfsc_checker/sccwriter.h new file mode 100644 index 000000000..f8922934f --- /dev/null +++ b/proofs/lfsc_checker/sccwriter.h @@ -0,0 +1,86 @@ +#ifndef SCC_WRITER_H +#define SCC_WRITER_H + +#include "expr.h" +#include +#include "check.h" + +enum +{ + opt_write_case_body = 0x00000001, + opt_write_check_sym_expr = 0x00000002, + opt_write_add_args = 0x000000004, + opt_write_no_inc = 0x00000008, + + opt_write_call_debug = 0x00000010, + opt_write_nested_app = 0x00000020, +}; + +class sccwriter +{ +private: + //options + int options; + //programs to write to file + symmap progs; + //list of indicies in progs + std::vector< Expr* > progPtrs; + std::vector< std::string > progNames; + int currProgram; + //current variables in the scope + std::vector< std::string > vars; + //global variables stored for lookups + std::vector< std::string > globalSyms; + //symbols that must be dec'ed + std::vector< std::string > decSyms; + //get program + CExpr* get_prog( int n ) { return (CExpr*)progs[ progNames[n] ]; } + //get index for string + int get_prog_index_by_expr( Expr* e ); + int get_prog_index( const std::string& str ); + //is variable in current scope + bool is_var( const std::string& str ); + //add global sym + void add_global_sym( const std::string& str ); + //expression count + static int exprCount; + //string count + static int strCount; + //args count + static int argsCount; + //num count + static int rnumCount; + //indent + static void indent( std::ostream& os, int ind ); + //write function header + void write_function_header( std::ostream& os, int index, int opts = 0 ); + void write_code( Expr* code, std::ostream& os, int ind, const char* retModStr, int opts = 0 ); + //write all children starting at child counter to stream, store in Expr* e_...e_; + void write_args( CExpr* code, std::ostream& os, int ind, int childCounter, std::vector< std::string >& args, int opts = 0 ); + //write expression - store result of code into e_ for some Expr* e_; + void write_expr( Expr* code, std::ostream& os, int ind, std::string& expr, int opts = 0 ); + //write variable + void write_variable( const std::string& n, std::ostream& os ); + //get function name + void get_function_name( const std::string& pname, std::string& fname ); + //get the variable name + void get_var_name( const std::string& n, std::string& nn ); + //write dec + void write_dec( const std::string& expr, std::ostream& os, int ind ); +public: + sccwriter( int opts = 0 ) : options( opts ){} + virtual ~sccwriter(){} + + void add_scc( const std::string& pname, Expr* exp ) { + //progs.push_back( std::pair< std::string, CExpr* >( pname, exp ) ); + progs[pname] = exp; + progPtrs.push_back( exp ); + progNames.push_back( pname ); + } + + void write_file(); + //write code + static void debug_write_code( Expr* code, std::ostream& os, int ind ); +}; + +#endif diff --git a/proofs/lfsc_checker/trie.cpp b/proofs/lfsc_checker/trie.cpp new file mode 100644 index 000000000..fedb508b0 --- /dev/null +++ b/proofs/lfsc_checker/trie.cpp @@ -0,0 +1,24 @@ +#include "trie.h" +#include + +class Simple : public Trie::Cleaner { +public: + ~Simple() {} + void clean(int p) { + (void)p; + } +}; + +template <> +Trie::Cleaner *Trie::cleaner = new Simple; + +void unit_test_trie() { + Trie t; + t.insert("a", 1); + t.insert("b", 2); + t.insert("abc", 3); + t.insert("b", 0); + std::cout << "a: " << t.get("a") << "\n"; + std::cout << "b: " << t.get("b") << "\n"; + std::cout << "abc: " << t.get("abc") << "\n"; +} diff --git a/proofs/lfsc_checker/trie.h b/proofs/lfsc_checker/trie.h new file mode 100644 index 000000000..094a9060a --- /dev/null +++ b/proofs/lfsc_checker/trie.h @@ -0,0 +1,129 @@ +#ifndef sc2__trie_h +#define sc2__trie_h + +#include +#include +#include + +template +class Trie { +protected: + char *str; + Data d; + bool using_next; + std::vector *> next; + + // s is assumed to be non-empty (and non-null) + Data insert_next(const char *s, const Data &x) { + unsigned c = s[0]; + if (c >= next.size()) { + using_next = true; + next.resize(c+1); + next[c] = new Trie; + } + else if (!next[c]) + next[c] = new Trie; + + return next[c]->insert(&s[1], x); + } + + // s is assumed to be non-empty (and non-null) + Data get_next(const char *s) { + unsigned c = s[0]; + if (c >= next.size()) + return Data(); + Trie *n = next[c]; + if (!n) + return Data(); + return n->get(&s[1]); + } + +public: + Trie() : str(), d(), using_next(false), next() { } + + ~Trie(); + + class Cleaner { + public: + virtual ~Cleaner() {} + virtual void clean(Data d) = 0; + }; + + static Cleaner *cleaner; + + bool eqstr(const char *s1, const char *s2) { + while (*s1 && *s2) { + if (*s1++ != *s2++) + return false; + } + return (*s1 == *s2); + } + + Data get(const char *s) { + if (!s[0] && (!str || !str[0])) + return d; + if (str && eqstr(str,s)) + return d; + if (using_next) + return get_next(s); + return Data(); + } + + Data insert(const char *s, const Data &x) { + if (s[0] == 0) { + // we need to insert x right here. + if (str) { + if (str[0] == 0) { + // we need to replace d with x + Data old = d; + d = x; + return old; + } + // we need to push str into next. + (void)insert_next(str,d); + free(str); + } + str = strdup(s); + d = x; + return Data(); + } + + if (str) { + // cannot store x here + if (str[0] != 0) { + insert_next(str,d); + free(str); + str = 0; + d = Data(); + } + return insert_next(s,x); + } + + if (using_next) + // also cannot store x here + return insert_next(s,x); + + // we can insert x here as an optimization + str = strdup(s); + d = x; + return Data(); + } + +}; + +template +Trie::~Trie() +{ + cleaner->clean(d); + for (int i = 0, iend = next.size(); i < iend; i++) { + Trie *t = next[i]; + if (t) + delete t; + } + if (str) + free(str); +} + +extern void unit_test_trie(); + +#endif diff --git a/src/Makefile.am b/src/Makefile.am index 3637cb089..18382a8ab 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -16,7 +16,7 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -D __STDC_LIMIT_MACROS \ -D __STDC_FORMAT_MACROS \ - -I@builddir@ -I@srcdir@/include -I@srcdir@ + -I@builddir@ -I@srcdir@/include -I@srcdir@ -I@top_srcdir@/proofs/lfsc_checker AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(FLAG_VISIBILITY_HIDDEN) SUBDIRS = lib options expr util prop/minisat prop/bvminisat . parser compat bindings main @@ -104,6 +104,7 @@ libcvc4_la_SOURCES = \ prop/sat_solver_registry.cpp \ prop/options_handlers.h \ smt/smt_engine.cpp \ + smt/smt_engine_check_proof.cpp \ smt/smt_engine.h \ smt/model_postprocessor.cpp \ smt/model_postprocessor.h \ @@ -393,6 +394,10 @@ libcvc4_la_LIBADD = \ @builddir@/expr/libexpr.la \ @builddir@/prop/minisat/libminisat.la \ @builddir@/prop/bvminisat/libbvminisat.la +if CVC4_PROOF +libcvc4_la_LIBADD += \ + @top_builddir@/proofs/lfsc_checker/liblfsc_checker.la +endif if CVC4_NEEDS_REPLACEMENT_FUNCTIONS libcvc4_la_LIBADD += \ diff --git a/src/smt/options b/src/smt/options index 05a138f60..69b5102de 100644 --- a/src/smt/options +++ b/src/smt/options @@ -22,6 +22,8 @@ option expandDefinitions expand-definitions bool :default false always expand symbol definitions in output common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h" support the get-value and get-model commands +option checkProofs check-proofs --check-proofs bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" + after UNSAT/VALID, machine-check the generated proof option checkModels check-models --check-models bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions option dumpModels --dump-models bool :default false diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0fadca424..1f83bb547 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3358,6 +3358,12 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc checkModel(/* hard failure iff */ ! r.isUnknown()); } } + // Check that UNSAT results generate a proof correctly. + if(options::checkProofs()) { + if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { + checkProof(); + } + } return r; }/* SmtEngine::checkSat() */ @@ -3428,6 +3434,12 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept checkModel(/* hard failure iff */ ! r.isUnknown()); } } + // Check that UNSAT results generate a proof correctly. + if(options::checkProofs()) { + if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { + checkProof(); + } + } return r; }/* SmtEngine::query() */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 9655297b3..0781ac1c0 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -248,6 +248,11 @@ class CVC4_PUBLIC SmtEngine { */ smt::SmtEnginePrivate* d_private; + /** + * Check that a generated Proof (via getProof()) checks. + */ + void checkProof(); + /** * Check that a generated Model (via getModel()) actually satisfies * all user assertions. diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp new file mode 100644 index 000000000..e4de1029b --- /dev/null +++ b/src/smt/smt_engine_check_proof.cpp @@ -0,0 +1,36 @@ +/********************* */ +/*! \file smt_engine_check_proof.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "smt/smt_engine.h" +#include "check.h" + +using namespace CVC4; +using namespace std; + +void SmtEngine::checkProof() { + +#ifdef CVC4_PROOF + + //TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime); + +#else /* CVC4_PROOF */ + + Unreachable("This version of CVC4 was built without proof support; cannot check proofs."); + +#endif /* CVC4_PROOF */ + +} -- 2.30.2