uclid-org / uclid Goto Github PK

UCLID5: formal modeling, verification, and synthesis of computational systems

License: Other

Scala 93.73% C# 0.23% Emacs Lisp 0.32% Shell 0.85% Python 0.07% Makefile 0.03% TeX 4.57% Vim Script 0.20%

uclid's Introduction

About

UCLID5 is an integrated modeling, verification and synthesis tool. UCLID5 is an evolution of the earlier UCLID modeling and verification system. The UCLID project was one of the first to develop satisfiability modulo theories (SMT) solvers and SMT-based verification methods. Here is the original UCLID paper that appeared at CAV 2002:

Randal E. Bryant, Shuvendu K. Lahiri, and Sanjit A. Seshia. Modeling and Verifying Systems using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. [HTML] Proceedings of the 14th International Conference on Computer-Aided Verification (CAV), pp. 78–92, LNCS 2404, July 2002.

If you use UCLID5 in your work, please cite the following papers:

Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora, and Sanjit A. Seshia. UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis. [HTML]34th International Conference on Computer Aided Verification (CAV 2022), Haifa, Israel. July 2022.

Sanjit A. Seshia and Pramod Subramanyan. UCLID5: Integrating Modeling, Verification, Synthesis and Learning. [HTML] Proceedings of the 16th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2018), Beijing, China. October 2018.

For questions and feeback please contact elizabeth.polgreen [at] ed.ac.uk.

Contact us

For bug reports, first preference is for you to file a GitHub issue. For help using UCLID5 in your work, please email [email protected]

UCLID5 Tutorial/Publication

The tutorial has a gentle introduction to using UCLID5.

Versions

Get the latest release, or get the latest development version git clone https://github.com/uclid-ord/uclid.

Installation

Prerequisites:

To use the prebuilt binaries, UCLID5 requires:

Z3 version 4.12.2 with the Java bindings
OpenJDK version 8,9,10 or 11

To compile from source, UCLID5 requires all of the above plus:

SBT version 1.0 or greater.

The following are optional requirements but several CI tests will fail without them:

(optional) CVC5 version 0.0.4 is the SyGuS-IF compliant solver used for synthesis tests in the CI.
(optional) Delphi is used for verification modulo oracles tests in the CI.

Installation of prerequisites on Linux

Java 11

Install instructions for OpenJDK are available at https://openjdk.java.net/install/

SBT (only required to build from source)

Install instructions for SBT are available at http://www.scala-sbt.org/1.0/docs/Setup.html

External solvers

For easy install of prerequisite solvers on Linux, run the following scripts from the root directory of the UCLID5 source repository. These scripts set up Z3/CVC5/Delphi for use with uclid5. This script will download Z3 version 4.12.2./CVC5 1.0.3/Delphi binaries from GitHub.

    $ source get-z3-linux.sh
    $ source get-cvc5-linux.sh #(optional but some CI synthesis tests will fail without CVC5)
    $ source get-delphi-linux.sh #(optional but some CI synthesis tests will fail without Delphi)

These scripts download the binaries for Z3, CVC5 and Delphi respectively and set up your PATH and LD_LIBRARY_PATH accordingly. You may wish to permanently add the following lines to your bash_profile:

    export PATH=$PATH:/path/to/uclid/z3/bin:/path/to/uclid/cvc5/bin:/path/to/uclid/delphi/bin:/path/to/uclid/oracles
    export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/path/to/uclid/z3/bin

Alternatively, Z3, CVC5, and Delphi can all be built from source, and instructions can be found on their respective git repositories. If you prefer to build Z3 from source, make sure the Z3/Java interface is enabled in your build (currently by passing --java to the mk_make.py script).

Installation of prerequisites on Mac

Java 11

We recommend using openJDK 11 on MacOS, and provide instructions for installing this with homebrew (further instructions are available at https://openjdk.org/install/):

brew install openjdk@11

If the above step does not work and you are running an old version of macOS, try:

brew update
brew tap homebrew/cask-versions
brew cask install java11

Make sure Java 11 is the default by adding the following lines to your dotfiles. For bash this is usually .bash_profile and for zsh this is usually .zshrc.

export JAVA_11_HOME=$(/usr/libexec/java_home -v11)
alias java11='export JAVA_HOME=$JAVA_11_HOME'
java11

SBT (only required to build from source)

brew install sbt

External solvers

For easy install of prerequisites on macOS, run the following scripts from the root directory of the UCLID5 source repository. These scripts set up Z3/CVC5/Delphi for use with uclid5. This script will download Z3 version 4.12.2./CVC5 1.0.3/Delphi binaries from GitHub.

    $ source get-z3-macos.sh
    $ source get-cvc5-macos.sh #(optional but some CI synthesis tests will fail without CVC5)
    $ source get-delphi-macos.sh #(optional but some CI synthesis tests will fail without Delphi)

These scripts add the downloaded binaries to your PATH and LD_LIBRARY_PATH accordingly. You may wish to permanently add the following lines to your bash_profile:

    export PATH=$PATH:/path/to/uclid/z3/bin:/path/to/uclid/cvc5/bin:/path/to/uclid/delphi/bin:/path/to/uclid/oracles

Due to System Integrity Protection, introduced in OS X El Capitan, Java ignores the user set DYLD_LIBRARY_PATH. Depending on the version of MacOS you are using, you may need to fix this issue by copying the JNI dynamic link libraries to Java/Library/Extensions and the non-JNI dynamic link libraries to /usr/local/lib as follows (if you build Z3 from source these files are found in the build directory):

    cp /path/to/uclid/z3/bin/libz3.dylib /usr/local/lib
    cp /path/to/uclid/z3/bin/libz3java.dylib /Library/Java/Extensions

Using the Pre-built binaries

Get the latest release. The uclid binary is located in the bin/ subdirectory

Compiling uclid5 from source

Run the following command in the root directory of the UCLID5 repository (note that it is not necessary to run sbt update if you already have the correct dependencies installed as per https://github.com/uclid-org/uclid/blob/master/build.sbt. However, running it will do no harm.):

$ sbt update clean compile "set fork:=true" test

If compilation and tests pass (or if the only failing tests are due to CVC5 and Delphi not being found), you can build a universal package.

$ sbt universal:packageBin

This will create uclid/target/universal/uclid-0.9.5.zip, which contains the uclid binary in the bin/ subdirectory. Unzip this file, and add it to your path.

$ unzip uclid-0.9.5.zip
$ cd uclid-0.9.5
$ export PATH=$PATH:$PWD/bin

Running UCLID

Now you can run uclid using the 'uclid' command. For example:

$ uclid examples/tutorial/ex1.1-fib-model.ucl

Some useful commands to know:

To print the SMT files use the -g flag, e.g., uclid examples/tutorial/ex1.1-fib-model.ucl -g "filename" will print the SMT file to SMT files with the prefix filename.
To run UCLID5 with another solver use the -s flag, e.g., uclid examples/tutorial/ex1.1-fib-model.ucl -s "cvc5 --lang smt2 --produce-models" will use CVC5 as the back-end solver.

Directory Structure

This repository consists of the following sub-directories.

examples : This contains example uclid5 models. See examples/tutorial for the examples from the tutorial.
lib: Libraries on which uclid5 depends (Z3).
project: Build scripts.
src/main/scala: uclid5 source.
src/test/scala: uclid5 test suite.
test: test programs for uclid5.
tutorial: uclid5 tutorial (with LaTeX source)
vim: vim syntax highlighting for uclid5.

Related Tools

chiselucl allows Chisel models to be converted into UCLID5.

uclid's People

Contributors

Stargazers

Watchers

uclid's Issues

parsing of record field names that collide with variable names

Hello there,

I am implementing an automated translator to Uclid5 from another verification language. One of the automated translations produced an unexpected outcome and I ~minimized it to the following:

module main {
  type t = record {
    x : integer
  };
  var x : t;

  procedure foo()
    modifies x;
  {
    if (x.x == x.x) {
    }
  }
}

Uclid5 0.9.5 has the following to say about this input:

$ uclid foo.ucl
Type error at line 10: Argument to select operator must be of type record or instance.
    if (x.x == x.x) {
        ^
Type error at line 10: Argument to select operator must be of type record or instance.
    if (x.x == x.x) {
               ^
Parsing failed. 2 errors found.

Is this expected? In my thinking, x is a record instance. But Uclid5 does not seem to enjoy its field having the same name.

A related (?) issue I ran into is doing assignment to a field within an array of records. This is actually done within the test/record-array.ucl file in the Uclid5 repository:

arr[0].a = 10;

However, this looks invalid according to the grammar in the tutorial, and is rejected:

$ uclid test/record-array.ucl
Syntax error test/record-array.ucl, line 10: '`='' expected but `.' found.
    arr[0].a = 10;
          ^

If there's a work around for this, I'd be interested to know, as I'm currently not sure how I'll translate expressions like this.

chaining of multiply needs parentheses

This doesn't parse, but should and needs fixing:
a*b*c

This does parse (i.e., the issue is only with multiply):
a+b+c

And so does this (the work around):
(a*b)*c

Enum variants in modules not recognized without importing type in main module

If an enum variant is referenced within a next block or procedure within a module, a "Type error ... Unknown identifier [variant name]" error is reported erroneously if the enum type is not imported in main.

Minimal example

module m1 {
    type op_t = enum { ADD, SUB };
    type non_enum_t = integer;

    // var g_inst : op_t; // Uncommenting this line fixes the issue

    init { } 

    next {
        var inst : op_t;
        var n : non_enum_t;
        inst = ADD;
        n = 100;
    }   
}

module main {
    // type op_t = m1.op_t; // Uncommenting this line ALSO fixes the issue

    instance i : m1 (); 
        
    next {
        next (i);
    }

    control { } 
}

Running this file causes the error on latest master (e244310). The workaround, as suggested by the comments in the above example, is to import the enum type in the main module being run.

More details

The type error is still reported if the enum type is defined in another external module (for example, if type op_t were defined in some other module m0, and imported in m1).
Declaring a global variable in m1 with the type of the enum in question also fixes the error somehow (see code example above).

enum pass bugs

The enum->numeric pass needs fixing.

Soundness bug:
uclid -e test/test-enum-1.ucl produces different results to uclid test/test-enum-1.ucl

Assertion failure:
uclid examples/cpu_induction.ucl -e throws an assertion error.

My guess is that the latter is to do with enums from different modules not being imported correctly. The former, I don't know.

RewriteRecordSelect conflicts with printing individual fields in counterexamples

The RewriteRecordSelect pass prepends _rec_ to each record field: https://github.com/uclid-org/uclid/blob/3f1bb32fb9a0c30f83a7737eaf2c90844bc7ed98/src/main/scala/uclid/lang/RewriteRecordSelect.scala.

module main {
    type cache_t = record { valid : boolean, value : integer };
    var cache   : cache_t;
    init {
        cache.valid = true;
        cache.value = 10;
    }
    next { }
    invariant trivial1  : cache.value == 20;
    control {
        v = bmc(1);
        check;
        print_results;
        v.print_cex_json(cache.value);
    }
}

However, when printing individual fields in print_cex, this rewriting does not take place (e.g. MWE above), resulting in the error below:

Type error at line 21: Field 'value' does not exist in record {_rec_valid : boolean, _rec_value : integer}.
        v.print_cex_json(cache.value);

TODO: printing of enums in synth functions

Currently, enum types are printed using internal names when we print synthesis functions.

e.g., for test-synthesis-9.ucl we print

define h (x: _type_enum_1_, y: _type_enum_1_): boolean = (t1 == x);

The correct translation for _type_enum_1_ should be enumT1.

Asserts don't fire in if block in next block

module main {
  // Part 1: System description.
  var a, b : integer;
  var kill : boolean;

  init {
    a = 0;
    b = 1;
    kill = false;
  }
  next {
    if ( ! kill ) {
      assert ( a <= b );
      call ( a', b' ) = fib ( a, b );
    }
  }

  procedure fib ( a : integer, b : integer )
    returns ( c: integer, d : integer )
    modifies kill;
  {
    if ( a == 5 ) {
      c = 100;
      d = 0;
      kill = true;
    }
    else {
      c = b;
      d = a + b;
    }
  }

  // Part 2: System specification.
  invariant a_le_b: a <= b;

  // Part 3: Proof script.
  control {
    unroll (10);
    check;
    print_results;
  }
}

This is a modified version of ex1.1, wherein when a == 5, the fibonacci sequence generation is killed and 'a, b' are set to their final values '100, 0'.

As expected the invariant on line 34 fails on step 6. However the assert on line 13 does not fire on steps 7-10 as expected.

If we move the assert outside the if block, it fires as expected on steps 7-10.

I originally found the issue on a much larger file in which an assert in the default case of a case statement (with a large number of cases) in an if block in a next block did not fire as expected.

I am on the latest dev version of uclid.

upgrade SBT

We need to upgrade to sbt 1.5 if we want to support apple silicon.
sbt/sbt#6187

Read Me file to Setup UCLID on Mac

Add a step-by-step guide to setup UCLID on Mac would be helpful for others.

@FedericoAureliano had shared this which worked for most part:

Install Java 11
1. `brew update`
2. `brew tap homebrew/cask-versions`
3. `brew cask install java11`

Make sure Java 11 is the defualt. For example, if you’re using bash, put this in your .bash_profile
`export JAVA_11_HOME=$(/usr/libexec/java_home -v11)
alias java11='export JAVA_HOME=$JAVA_11_HOME'
java11`

INSTALL Z3
1. clone z3 and go into the directory
2. `mkdir build; cd build`
3. `cmake -G "Unix Makefiles" -DCMAKE_BUILD_TYPE=Release -DZ3_BUILD_JAVA_BINDINGS=TRUE -DZ3_INSTALL_JAVA_BINDINGS=TRUE ../`
4. `make -j4`

Make sure the z3 java libraries are in the right place
1. `sudo cp <buildfolderInZ3>*z3*.dylib /Library/Java/Extensions/.`

Install sbt
1. `brew install sbt`

install UCLID
1. clone uclid, cd into the directory
2. `sbt update clean compile`
3. `sbt universal:packageBin`
4. `unzip <target/universal>/uclid-0.9.5.zip; cd uclid-0.9.5; export PATH=$PATH:$PWD/bin`

synthesis test 7

Test-synthesis-7 seems to time out, we should check the encoding is as expected:

/** This is an example to test UCLID5's invariant synthesis.
  */

module main
{
  synthesis function h(x : integer, y : integer) : boolean;
  var x, y, z : integer;
  
  init {
    assume (x == 0);
    assume (y == 1);
    assume (z == 2);
  }
  
  next {
    /*
    x' = x + 1;
    y' = x + y;
    z' = y + z;
    */
    havoc x;
    havoc y;
    havoc z;
    assume (x' == x + 1);
    assume (y' == x + y);
    assume (z' == y + z);
    assert (z >= 0);
  }
  
  invariant always_positive: (z >= 0) && h(z, y);
  
  control {
    induction;
    check;
    print_results;
  }
}

incorrect result in hyperproperty verification in case of havoc stmts

The following program should pass all assertions but it fails due to bug in modular product transformation of havoc statements.

module main 
{
    procedure foo(x : integer) returns (y: integer)
    ensures (x.1 > 5 && x.2 > 5 && x.1 == x.2) ==> (y.1 == y.2);
    {
        y = 0;
        if (x <= 5) {
        havoc y;
        }
    } 


    control
    {
        v = verify(foo);
        check;
        v.print_cex(x, y);
        print_results;
    }
}`

```

How to estimate running time for a large model?

I have a large uclid model (about 129K lines), and I want to estimate how long it will take to do bmc on it for at least 10K steps. When I unroll this large model for 2 steps with a simple property, uclid runs for around 10 minutes. Thus it is hard to predict how long it might take for 10K steps. Assuming a constant time for each step, it might take 70 days.

However, if I remove all the unreachable blocks within say 25 steps to reduce the model to ~1K lines, uclid can unroll upto 25 steps in 24 mins:

From the image, it appears that, for this model, time increases exponentially with the number of steps. So, my initial estimate of 70 days might be an underestimation. However, since I do not know exactly how uclid works under the hood, I am not sure whether I can just multiply the estimate from the above graph with the factor of size (~130). Can uclid be optimized in some way so that the effect of the size of the model is less severe?

Can uclid provide more detailed timing information about its runs that helps in estimating the time it might take for a large model? It would be even better if it could give status updates when it is running for a long time, and maybe even provide an estimated time of completion. In the absence of features like these, could you provide some guidance about how to estimate the running time for large models?

I am modeling memory as var mem : [bv32]bv8, and the exponential increase in time seems to be tied to the number of stores encountered during unrolling. Stores are modeled as mem [addr] = exp. Is there an alternative way of modeling memory that could avoid this exponential increase in time?

PS: I noticed that my running times increased drastically when I did not havoc all the variables in the init block, but I did not find anything in the tutorial that suggested that this was mandatory or recommended.

Not removing first assertion from solver affects results of subsequent verification queries

This is a soundness bug that can be reproduced on UCLID master at the current head commit 18dd349.

The first assertion that UCLID adds to the solver is never removed, and so is included in all subsequent verification queries. Because of the variable renaming, the results of subsequent verification queries remain unaffected almost all the time. The one corner case where results are affected is if the first thing added to the solver is an unsatisfiable assumption, which is equivalent to assert false. This can make all subsequent verification queries spuriously pass.

E.g., in this example, verify(shouldpass) should pass because the assumption blocks all paths to the assertion, but verify(shouldfail) should fail. However, because the first thing added to the solver is the blocking assumption, which is never removed, verify(shouldfail) passes.

module main {

    procedure shouldpass()
    {
        var v: integer;
        v = 0;
        assume(v>0);
        assert(v==1); // unreachable
    }

    procedure shouldfail()
    {
        var x: integer;
        x=0;
        assert(x==1);
    }

    control {
        v = verify(shouldpass); // should pass, the assertion is unreachable
        verify(shouldfail); // should fail
        check;
        print_results;
    }
}

I have submitted a PR with a test for this, but I don't know what the fix should be
https://github.com/uclid-org/uclid/blob/2b1e8a8614379147296c11900b4260ad85c7817b/test/test-conflicting-assumptions.ucl

[smt] negative BitVectorLit value

I was just going through the uclid.smt patches that I have lying around and I found one that might be interesting to the broader community.
It deals with a negative value in the BitVectorLit class [src].
The way the current serialization code is written is not compatible with value < 0:

override def toString = "(_ bv" + value.toString + " " + width.toString +")"

If value is negative this yields an invalid SMTLib expression.

My quick way of fixing this was to add an assert:

  Utils.assert(value >= 0, s"Value $value is negative. Negative BitVector literals are not supported.")

Another way of dealing with this would be to take the bits of the two complements integer and turn those into a string which would also yield a valid SMTLib expression.

As an example: BitVectorLit(-2, 3).toString could yield #b110 or alternatively (_ bv6 3).

bmc should not ignore non-LTL properties

We should remove the ambiguity between bmc and unroll.

Currently unroll ignores LTL properties and checks non-LTL. bmc ignores non-LTL properties and checks LTL properties.

We should make bmc check all properties and then bmc supercedes unroll.

TODO: macros

Extend parser to support more meaningful error messages for:
- recursive macros (we don't want to support this but we do want to check for cycles)
- macros in next statement
- primed assignments in macros

Additional things to support:
- We should definitely import macros when we import a module, otherwise import module becomes confusing (modules get imported as in test/test-module-import-0.ucl)
- we should maybe allow import macros via macro =module1. (as done for types in test/test-type-import.ucl), but this is less of a problem because it throws an error.
- nested macros (but not cyclic)

replace genericProofCommand

creating issue as reminder. cc @FedericoAureliano @DemetrisChr

z3 java bindings on Mac

There is a known issue with using the Z3Interface on mac, caused by the Z3 java API not finding the correct libraries.

See: Z3Prover/z3#4979

Possible workarounds:

put libz3.dylib in the directory you call uclid from
use the SMTLibInterface, by using the command line option -s "z3 -in" when you call uclid (nb: the z3 binary must be added to your $PATH for this to work)
disable SIP (we do not recommend this)

We won't fix this issue: the Z3Interface is gradually going to be deprecated and users will be pushed towards the SMTLibInterface instead

Typo in https://github.com/uclid-org/uclid/blob/master/mac-install.md

I am installing uclid on a Mac with macOS Catalina and I followed the instructions on the file https://github.com/uclid-org/uclid/blob/master/mac-install.md for installation. There is a small typo under Install Z3 heading: sudo cp <buildfolderInZ3>/libz3.dylib /usr/local/bin should be replaced by sudo cp <buildfolderInZ3>/libz3.dylib /usr/local/lib otherwise even though the build succeeded on my machine, actually running an example resulted in the following error:

Exception in thread "main" java.lang.UnsatisfiedLinkError: no libz3java in java.library.path: /Users/aayan/Library/Java/Extensions:/Library/Java/Extensions:/Network/Library/Java/Extensions:/System/Library/Java/Extensions:/usr/lib/java:.
at java.base/java.lang.ClassLoader.loadLibrary(ClassLoader.java:2447)
at java.base/java.lang.Runtime.loadLibrary0(Runtime.java:809)
at java.base/java.lang.System.loadLibrary(System.java:1893)
at com.microsoft.z3.Native.(Native.java:14)
at com.microsoft.z3.Context.(Context.java:73)
at uclid.smt.Z3Interface.(Z3Interface.scala:158)
at uclid.UclidMain$.execute(UclidMain.scala:383)
at uclid.UclidMain$.main(UclidMain.scala:147)
at uclid.UclidMain$.main(UclidMain.scala:60)
at uclid.UclidMain.main(UclidMain.scala)

Variables sometimes fail to update in counterexamples

The counterexample produced for the below code should not be a reachable state, since the step variable is incremented on every cycle in the next block. However, the counterexample has the value of step at 1 on consecutive cycles despite this.

Code

module main {

    var x : integer;
    var step : integer;

    init {
        x = 0;
        step = 0;
    }

    next {
        x' = 1;
        step' = step + 1;
        assert ((step == 1) ==> (x == 0)); // should fail
    }

    // invariant x_zero : (step == 1) ==> (x == 0);

    control {
        vobj = bmc_noLTL(3);
        check;
        print_results;
        vobj.print_cex();
    }
}

Output

$ uclid no_update.ucl
Successfully instantiated 1 module(s).
2 assertions passed.
1 assertions failed.
0 assertions indeterminate.
  PASSED -> vobj [Step #1] assertion @ no_update.ucl, line 14
  PASSED -> vobj [Step #3] assertion @ no_update.ucl, line 14
  FAILED -> vobj [Step #2] assertion @ no_update.ucl, line 14
CEX for vobj [Step #2] assertion @ no_update.ucl, line 14
=================================
Step #0
  step : 0
  x : 0
=================================
=================================
Step #1
  step : 1
  x : 1
=================================
=================================
Step #2
  step : 1
  x : 1
=================================
Finished execution for module: main.

Incorrect Java version check in the uclid shell script

Running the 0.9.5 release on Debian unstable/Sid, with openjdk 8 and 10 installed, I get the following message:
"
The java installation you have is not up to date
requires at least version 1.6+, you have
version 10.0.1
"
Disabling
elif [[ ! "$java_version" > "1.6" ]]; then
makes everything work again. The java_version definition and/or comparison are probably broken.

Record literals not type-checking properly

In some situations, instantiating a record with tuple literal syntax (mentioned as a possible workaround in #99) causes runtime errors. I've found two separate errors (plus a third that I can't seem to reproduce), but I'm grouping them in one issue since I would imagine they have a similar root cause.

Issue 1

Reading properties of variables initialized with record syntax results in java.util.NoSuchElementException: None.get.

Minimal example

module main {
    type rec_t = record { f1 : integer, f2 : bv32 };

    var state : rec_t;

    init {
        state = { 100, 100bv32 };
    }   

    next {
        assert (state.f1 != 200);
    }   

    control {
        bmc_noLTL(5);
        check
    }   
}

Running this on latest master (e244310) produces the following stack trace:

Exception in thread "main" java.util.NoSuchElementException: None.get
	at scala.None$.get(Option.scala:529)
	at scala.None$.get(Option.scala:527)
	at uclid.smt.RecordSelectOp.resultType(SMTLanguage.scala:622)
	at uclid.smt.OperatorApplication.<init>(SMTLanguage.scala:849)
	at uclid.smt.Converter$._exprToSMT(Converter.scala:288)
	at uclid.smt.Converter$.toSMT$1(Converter.scala:248)
	at uclid.smt.Converter$.$anonfun$_exprToSMT$1(Converter.scala:249)
	at scala.collection.immutable.List.map(List.scala:286)
	at uclid.smt.Converter$.toSMTs$1(Converter.scala:249)
	at uclid.smt.Converter$._exprToSMT(Converter.scala:287)
	at uclid.smt.Converter$.exprToSMT(Converter.scala:319)
	at uclid.SymbolicSimulator.evaluate(SymbolicSimulator.scala:1804)
	at uclid.SymbolicSimulator.simulateStmt(SymbolicSimulator.scala:1660)
	at uclid.SymbolicSimulator.$anonfun$simulateStmt$1(SymbolicSimulator.scala:1592)
	at scala.collection.LinearSeqOptimized.foldLeft(LinearSeqOptimized.scala:126)
	at scala.collection.LinearSeqOptimized.foldLeft$(LinearSeqOptimized.scala:122)
	at scala.collection.immutable.List.foldLeft(List.scala:89)
	at uclid.SymbolicSimulator.simulateStmtList$1(SymbolicSimulator.scala:1592)
	at uclid.SymbolicSimulator.simulateStmt(SymbolicSimulator.scala:1715)
	at uclid.SymbolicSimulator.simulateModuleNext(SymbolicSimulator.scala:1582)
	at uclid.SymbolicSimulator.$anonfun$symbolicSimulate$1(SymbolicSimulator.scala:1124)
	at scala.collection.immutable.Range.foreach$mVc$sp(Range.scala:158)
	at uclid.SymbolicSimulator.symbolicSimulate(SymbolicSimulator.scala:1120)
	at uclid.SymbolicSimulator.prove$1(SymbolicSimulator.scala:228)
	at uclid.SymbolicSimulator.$anonfun$execute$6(SymbolicSimulator.scala:246)
	at uclid.SymbolicSimulator.$anonfun$execute$6$adapted(SymbolicSimulator.scala:236)
	at scala.collection.immutable.List.foreach(List.scala:392)
	at uclid.SymbolicSimulator.execute(SymbolicSimulator.scala:236)
	at uclid.UclidMain$.execute(UclidMain.scala:430)
	at uclid.UclidMain$.executeCommands(UclidMain.scala:482)
	at uclid.UclidMain$.$anonfun$main$1(UclidMain.scala:171)
	at scala.collection.immutable.List.foreach(List.scala:392)
	at uclid.UclidMain$.main(UclidMain.scala:171)
	at uclid.UclidMain$.main(UclidMain.scala:62)
	at uclid.UclidMain.main(UclidMain.scala)

Issue 2

Assigning a record literal to a global variable causes an assertion error within uclid.

Minimal example

module main {
    type rec_t = record { f1 : integer, f2 : bv32 };

    var state : rec_t;

    init { } 

    next {
        state' = { 100, 100bv32 };
    }   

    control {
        bmc_noLTL(5);
        check;
    }   
}

Running this file with uclid -X gives the following output:

Successfully instantiated 1 module(s).
[Assertion Failure]: Operands to '=' must of the same type. Got: record [f1 : Int, f2 : (_ BitVec 32)] tuple [Int, (_ BitVec 32)]
uclid.Utils$AssertionError: Operands to '=' must of the same type. Got: record [f1 : Int, f2 : (_ BitVec 32)] tuple [Int, (_ BitVec 32)]
	at uclid.Utils$.assert(Utils.scala:54)
	at uclid.smt.Operator.checkAllArgsSameType(SMTLanguage.scala:205)
	at uclid.smt.Operator.checkAllArgsSameType$(SMTLanguage.scala:200)
	at uclid.smt.BoolResultOp.checkAllArgsSameType(SMTLanguage.scala:439)
	at uclid.smt.EqualityOp$.typeCheck(SMTLanguage.scala:516)
	at uclid.smt.OperatorApplication.<init>(SMTLanguage.scala:854)
	at uclid.SymbolicSimulator.$anonfun$renameStates$2(SymbolicSimulator.scala:1053)
	at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:273)
	at scala.collection.immutable.List.foreach(List.scala:392)
	at scala.collection.TraversableLike.map(TraversableLike.scala:273)
	at scala.collection.TraversableLike.map$(TraversableLike.scala:266)
	at scala.collection.immutable.List.map(List.scala:298)
	at uclid.SymbolicSimulator.renameStates(SymbolicSimulator.scala:1048)
	at uclid.SymbolicSimulator.$anonfun$symbolicSimulate$1(SymbolicSimulator.scala:1130)
	at scala.collection.immutable.Range.foreach$mVc$sp(Range.scala:158)
	at uclid.SymbolicSimulator.symbolicSimulate(SymbolicSimulator.scala:1120)
	at uclid.SymbolicSimulator.prove$1(SymbolicSimulator.scala:228)
	at uclid.SymbolicSimulator.$anonfun$execute$6(SymbolicSimulator.scala:246)
	at uclid.SymbolicSimulator.$anonfun$execute$6$adapted(SymbolicSimulator.scala:236)
	at scala.collection.immutable.List.foreach(List.scala:392)
	at uclid.SymbolicSimulator.execute(SymbolicSimulator.scala:236)
	at uclid.UclidMain$.execute(UclidMain.scala:430)
	at uclid.UclidMain$.executeCommands(UclidMain.scala:482)
	at uclid.UclidMain$.$anonfun$main$1(UclidMain.scala:171)
	at scala.collection.immutable.List.foreach(List.scala:392)
	at uclid.UclidMain$.main(UclidMain.scala:171)
	at uclid.UclidMain$.main(UclidMain.scala:62)
	at uclid.UclidMain.main(UclidMain.scala)

parsing check: print cex doesn't check if variable is defined

We don't check if the v is defined when v.print_cex is called. e.g.,

module main {
  init { }
  next { }

  control {
    induction;
    check;
    print_results;
   x.print_cex(); // this will parse fine but get ignored
  }

Simple liveness checks incorrectly passing

I created the following minimal module which increments a counter:

module main {
    var id: integer;

    init {
        id = 0;
    }

    next {
        id' = id + 1;
    }

    property[LTL] reaches_50: F(id == 50);

    control {
        // check the invariant.
        v = bmc(5);
        check;
        print_results;
        v.print_cex(
            id
        );
    }
}

bmc should fail because the module is unrolled for 5 timesteps which is insufficient to reach 50, which the property desires. However, UCLID says the tests passed:

Successfully instantiated 1 module(s).
12 assertions passed.
0 assertions failed.
0 assertions indeterminate.
  PASSED -> v [Step #0] property reaches_50:liveness @ task1.ucl, line 12
  PASSED -> v [Step #0] property reaches_50:safety @ task1.ucl, line 12
  PASSED -> v [Step #1] property reaches_50:liveness @ task1.ucl, line 12
  PASSED -> v [Step #1] property reaches_50:safety @ task1.ucl, line 12
  PASSED -> v [Step #2] property reaches_50:liveness @ task1.ucl, line 12
  PASSED -> v [Step #2] property reaches_50:safety @ task1.ucl, line 12
  PASSED -> v [Step #3] property reaches_50:liveness @ task1.ucl, line 12
  PASSED -> v [Step #3] property reaches_50:safety @ task1.ucl, line 12
  PASSED -> v [Step #4] property reaches_50:liveness @ task1.ucl, line 12
  PASSED -> v [Step #4] property reaches_50:safety @ task1.ucl, line 12
  PASSED -> v [Step #5] property reaches_50:liveness @ task1.ucl, line 12
  PASSED -> v [Step #5] property reaches_50:safety @ task1.ucl, line 12
Finished execution for module: main.

I'm using uclid 0.9.5 as shown by uclid --help.

http://uclid.eecs.berkeley.edu is invalid

I want to start from the UCLID and the tutorial say I can find UCLID at http://uclid.eecs.berkeley.edu. But it seems that this link is invalid now.

Invariants over next states

Is there a way to include the next state of a signal in an invariant.

For example, let's say I want to prove termination of a system through the invariant that a counter is always decreasing. Trying to write an invariant like this gives me a syntax error:

invariant counter_decreases : counter < counter';

Is there a different way to express this?

The counterexample of induction with k > 1 shows one less state in the induction_step.

As suggested in the title, when I run the following model with induction(3)

module main {
    var a : boolean;
    var b : boolean;
    var x : integer;

    var step : integer;

    init {
        a = false;
        b = false;
	x = 0;

	step = 0;
    }

    next {
	// Update a if it is false.
	if (!a) {
	    havoc a;
	} else {
	    a' = false; // default
	}
	// Chain reaction
        if (a && !b) {
            havoc b;
        } else {
            b' = false; // default
        }

        // Side affect of b == true.
        if (b') {
        x' = 1;	
        }

        step' = step + 1;
    }

    invariant prop: !(b && !a);

    control {
        v = induction(3);
        check;
        print_results;
        v.print_cex();
    }
}

the induction_step should show three states, but currently there are only two.

synthesis test 7

Test-synthesis-7 times out, this should be debugged:

/** This is an example to test UCLID5's invariant synthesis.
  */

module main
{
  synthesis function h(x : integer, y : integer) : boolean;
  var x, y, z : integer;
  
  init {
    assume (x == 0);
    assume (y == 1);
    assume (z == 2);
  }
  
  next {
    /*
    x' = x + 1;
    y' = x + y;
    z' = y + z;
    */
    havoc x;
    havoc y;
    havoc z;
    assume (x' == x + 1);
    assume (y' == x + y);
    assume (z' == y + z);
    assert (z >= 0);
  }
  
  invariant always_positive: (z >= 0) && h(z, y);
  
  control {
    induction;
    check;
    print_results;
  }
}

The `bmc` command currently ignores `assert` statements.

This can be observed using the example below:

module main {
    // System description.
    var a, b : integer;
    const flag : boolean;

    procedure set_init()
        modifies a, b;
    {
        havoc a;
        havoc b;
        // embedded assumptions.
        assume (a <= b);
        assume (a >= 0 && b >= 0);
        assume (flag);
    }

    init {
        call set_init();
    }
    next {
        a', b' = b, a + b;
        if (flag) {
            assert (a' <= b');
        } else {
            assert (false);
        }
    }

    // Proof script.
    control {
        bmc (3);
        check;
        print_results;
    }
}

Uclid5 output:

(base) shaokai@Shaokais-MacBook-Pro code % uclid fib_embedded_spec.ucl
Successfully instantiated 1 module(s).
0 assertions passed.
0 assertions failed.
0 assertions indeterminate.
Finished execution for module: main.

Assumption on array causes malfunctioning checks

Hi, I would like to have an arbitrary memory except that, within a fixed range, there are at least two non-zero elements. However, such an assumption makes the checks behave incorrectly. They always pass no matter what I assert.

The code:

module test {
    const RANGE_START: bv4;
    const RANGE_SIZE: bv4;

    var mem: [bv4]bv4;

    init {
        assume(RANGE_START == 1bv4);
        assume(RANGE_SIZE == 8bv4);

        havoc mem;

        // within range [1bv4, 8bv4], 
        // there are at least two non zero elements in mem
        assume(exists (mix, miy: bv4):: 
            (mix >= RANGE_START) && (mix <= RANGE_START + RANGE_SIZE - 1bv4) &&
            (miy >= RANGE_START) && (miy <= RANGE_START + RANGE_SIZE - 1bv4) &&
            (mix != miy) && (mem[mix] != 0bv4) && (mem[miy] != 0bv4));
    }

    next {
    }

    // the invariant shall not hold
    invariant assert_false: (false);

    control {
        vobj = bmc(6);
        check;
        vobj.print_cex();
    }
}

In the code above, I assert false but all checks pass:

Successfully instantiated 1 module(s).
7 assertions passed.
0 assertions failed.
0 assertions indeterminate.
  PASSED -> vobj [Step #0] property assert_false @ ./example.v, line 25
  PASSED -> vobj [Step #1] property assert_false @ ./example.v, line 25
  PASSED -> vobj [Step #2] property assert_false @ ./example.v, line 25
  PASSED -> vobj [Step #3] property assert_false @ ./example.v, line 25
  PASSED -> vobj [Step #4] property assert_false @ ./example.v, line 25
  PASSED -> vobj [Step #5] property assert_false @ ./example.v, line 25
  PASSED -> vobj [Step #6] property assert_false @ ./example.v, line 25
Finished execution for module: test.

But if I comment out those two lines about the range,

        assume(exists (mix, miy: bv4)::
            // (mix >= RANGE_START) && (mix <= RANGE_START + RANGE_SIZE - 1bv4) &&
            // (miy >= RANGE_START) && (miy <= RANGE_START + RANGE_SIZE - 1bv4) &&
            (mix != miy) && (mem[mix] != 0bv4) && (mem[miy] != 0bv4));

Then the checks work again:

0 assertions passed.
7 assertions failed.
0 assertions indeterminate.
  FAILED -> vobj [Step #0] property assert_false @ ./example.v, line 25
  FAILED -> vobj [Step #1] property assert_false @ ./example.v, line 25
  FAILED -> vobj [Step #2] property assert_false @ ./example.v, line 25
  FAILED -> vobj [Step #3] property assert_false @ ./example.v, line 25
  FAILED -> vobj [Step #4] property assert_false @ ./example.v, line 25
  FAILED -> vobj [Step #5] property assert_false @ ./example.v, line 25
  FAILED -> vobj [Step #6] property assert_false @ ./example.v, line 25

I wonder if I am misusing havoc and assumptions. Thank you!

Record Rewriter's Bugs

Nowtime rewriter cannot rewrite the variable inside "print_cex".
I will look into that.

Z3 array not converted to string in counterexample

Arrays constrained by more complex assume statements are not always properly converted to strings in counterexamples.

Code

module main {
    var arr : [bv5]bv2;

    init {
        assume (forall (a : bv5) :: (a > 20bv5 && a < 22bv5) ==> arr[a] == 0bv2);
    }

    next {
        assert (arr[20bv5] == 0bv2); // should fail
        assert (arr[21bv5] == 0bv2);
    }

    control {
        v = bmc_noLTL(1);
        check;
        print_results;
        v.print_cex(arr);
    }
}

Output

$ uclid z3_array_conversion.ucl
Successfully instantiated 1 module(s).
1 assertions passed.
1 assertions failed.
0 assertions indeterminate.
  PASSED -> v [Step #1] assertion @ z3_array_conversion.ucl, line 10
  FAILED -> v [Step #1] assertion @ z3_array_conversion.ucl, line 9
CEX for v [Step #1] assertion @ z3_array_conversion.ucl, line 9
=================================
Step #0
  arr : UCLID is unable to convert this z3 array to string: (lambda ((x!1 (_ BitVec 5)))
  (let ((a!1 (ite (bvule #b10101 x!1)
                  (ite (bvule #b10111 x!1) #b10111 #b10101)
                  #b10100)))
    (ite (= a!1 #b10101) #b00 (ite (= a!1 #b10100) #b01 #b10))))

=================================
=================================
Step #1
  arr : UCLID is unable to convert this z3 array to string: (lambda ((x!1 (_ BitVec 5)))
  (let ((a!1 (ite (bvule #b10101 x!1)
                  (ite (bvule #b10111 x!1) #b10111 #b10101)
                  #b10100)))
    (ite (= a!1 #b10101) #b00 (ite (= a!1 #b10100) #b01 #b10))))

=================================
Finished execution for module: main.

Different verification results produced when there is only a variable name difference

I have the same targets to verify where there is only the difference in a variable name (owner_map in the below). While they contain the exact same code logic and there is no place where the modified variable is used, the verification results are different for some reasons. I think that this is the bug in uclid, but I am not sure what is the root cause of this bug.

$ git diff expected unexpected 
diff --git a/TrustedAbstractPlatform/standard/modules/see-cpu.ucl b/TrustedAbstractPlatform/standard/modules/see-cpu.ucl
index a26af0e..8d737f6 100644
--- a/TrustedAbstractPlatform/standard/modules/see-cpu.ucl
+++ b/TrustedAbstractPlatform/standard/modules/see-cpu.ucl
@@ -9,7 +9,7 @@ var enclave_id   : tap_enclave_id_t;
 var regs         : regs_t;
 var pc           : linear_addr_t;
 var addr_valid   : linear_addr_valid_t;
-var owner_map    : linear_owner_map_t;
+var owner_map_test    : linear_owner_map_t; // XXX: this is the only line modified from the `expected` branch

Different results

[expected results]
smt/ctap-assertion-_____modules_tap-mod_ucl__line_1708-verif_measurement_proof_2:_verify_measurement_proof_part2-0004.smt unknown ----------
smt/ctap-assertion-_____modules_tap-mod_ucl__line_1708-verif_measurement_proof_2:_verify_measurement_proof_part2-0056.smt unknown ----------

[unexpected results]
smt/ctap-assertion-_____modules_tap-mod_ucl__line_1708-verif_measurement_proof_2:_verify_measurement_proof_part2-0004.smt verified.
smt/ctap-assertion-_____modules_tap-mod_ucl__line_1708-verif_measurement_proof_2:_verify_measurement_proof_part2-0011.smt verified.

As there is an explicit false assertion inserted, the expected results are correct.

$ sed -n 1707,1708p trusted-abstract-platform/TrustedAbstractPlatform/standard/modules/tap-mod.ucl
        call simple_test();
        assert false;

However, in the unexpected results, this false assertion is bypassed for some reasons.

Before the false assertion, the child module (see)'s one variable is simply modified.

$ sed -n 566,571p trusted-abstract-platform/TrustedAbstractPlatform/standard/modules/tap-mod.ucl 
procedure [noinline] simple_test()
    ensures (see.enclave_id != old(see.enclave_id));
    modifies see;
{
    call see.havoc_enclave_id();
}

$ sed -n 15,23p trusted-abstract-platform/TrustedAbstractPlatform/standard/modules/see-cpu.ucl 
procedure [noinline] havoc_enclave_id()
  ensures (enclave_id != old(enclave_id));
  modifies enclave_id;
{
  var new_enclave_id : tap_enclave_id_t;
  havoc new_enclave_id;
  assume (new_enclave_id != enclave_id);
  enclave_id = new_enclave_id;
}

How to reproduce?

In the following two branches, expected-branch and unexpected-branch,

cd trusted-abstract-platform/TrustedAbstractPlatform/standard/proofs
$ make measurement-proof-printed
$ run_all_smt.sh

SExpr parser/parsing models

We have some issues parsing back models from CVC4, and models using arrays etc.

These issues are shown in #95

We should either extend the SExpr parser to parse these models, or switch to using get_value.

error splitting commands

uclid test-array-record.ucl

(has no commands)

fix and re-enable redundant assignment eliminator

PR #58 disables the redundant assignment eliminator and adds a test that exposes a bug in the eliminator. This should be fixed and re-enabled

tutorial/ex4.4 embeded assertions not working as expected

Hi, I feel that the embeded assertions are not working. (0.9.5 release works though.)

When I run:
uclid examples/tutorial/ex4.4-fib-model-revisted.ucl

Expected result:

6 assertions passed.
0 assertions failed.
0 assertions indeterminate.

What I got:

0 assertions passed.
0 assertions failed.
0 assertions indeterminate.

using past and history function in invariants

Dear all,

I have been trying to use the history and past function to verify simple invariants, based on the discussion #6 (comment), but I have trouble understanding some Uclid results.

For example, for the example below, I would expect invariants fail0 and fail1 to hold, but I get counter examples, and since it is not possible to print the value of history(cpt,1) in the cex, it is difficult to understand where the problem stems from.

Any advice ?

`
module main {

	var cpt,oldcpt : integer ;
	
	init {
		cpt=0;
	}
  
	next {
		cpt'= cpt+1;
		oldcpt'=cpt;
	}

	invariant inv0 : (cpt>=0);
	invariant pass0 : (cpt>1) ==> (oldcpt==(cpt-1)) ;
	invariant pass1 : (cpt>1) ==> (history(cpt,1)<(cpt)) ;

	invariant fail0 : (cpt>1) ==> (history(cpt,1)==oldcpt) ;
	invariant fail1 : (cpt>1) ==> (history(cpt,1)==(cpt-1)) ;

	control {
		vobj = induction(2);
		check;
		print_results;
 		vobj.print_cex(cpt,oldcpt);
	}
	
}

PS: thanks you for Uclid5, this is a really a very nice tool

Regards,

Steven

[request] will UCLID support a division operator?

Hi! I have been using UCLID for our project deepsea in a model extractor for our programming language. And I have some questions about its features

I noticed that UCLID an interesting software and easier to use compared with things like PlusCal, however, UCLID does not have a division operator, so what we are doing now is to have some hacks like:
procedure div (x : integer, y : integer) returns (r : integer) { assume(y == r * x); } and then use divisions as function calls (statements), but since normally divisions are expressions, that makes it a bit weird to translate (I am aware that I can write an ast pre-processing to solve this, but that would be a bit heavy-weight). So it would be nice if we could have a division operator in UCLID. Also, I wonder why UCLID did not support divisions right now, is it because it makes solving hard of non-linearity?

Bug in unrolling

I don't think the attached code should go through with 50 unrolling. In fact there should be a counter example at step 2. However, uclid says all assertions passed. Uclid is able to find the cex if you move the processor's specification into main.

module processor {
  input pc: bv32;
  input insts: [bv32]bv32;

  procedure exec_inst(new_pc: bv32)
    returns (pc_next: bv32)
  {
    pc_next = new_pc;
  }

  init {
  }

  next {
    call (pc') = exec_inst(insts[pc]);
  }
}

module main {
  var pc: bv32;
  var insts: [bv32]bv32;
  instance thread: processor(insts: (insts), pc: (pc));

  init {
    assume (thread.pc == 1bv32);
    assume (thread.insts[1bv32] == 2bv32);
    assume (thread.insts[2bv32] == 0bv32);
  }

  next {
    next (thread);
  }

  property p: (thread.pc != 0bv32);

  control {
    v = unroll(50);
    check;
    print_results;
    v.print_cex(pc, insts);
  }
}

Assertions on values of variables changed by child modules in `next` block have inconsistent values

(as discussed in uclid meeting on 4/28/22)

Assertions involving variables updated by a call to the next block of a child module use a different value for the variable depending on whether it is placed before or after next.

Code

module assign_child {
    output o : boolean;

    init {
        o = false;
    }

    next {
        o' = true;
    }
}

module main {
    var o0 : boolean;
    var step : integer;
    instance child0 : assign_child(o : (o0));

    init {
        step = 0;
    }

    next {
        assert (step != 0 || !o0); // Correctly passes
        next (child0);
        assert (step != 0 || !o0); // Incorrectly fails
        step' = step + 1;
    }
    
    control {
        v = bmc_noLTL(3);
        check;
        v.print_cex(step, o0);
        print_module;
    }    
}

Output

Successfully instantiated 2 module(s).
CEX for v [Step #1] assertion @ reduced.ucl, line 25
=================================
Step #0
  step : 0
  o0 : false
=================================
=================================
Step #1
  step : 0
  o0 : true
=================================

module main {
  var step : integer; // reduced.ucl, line 15
  next // reduced.ucl, line 22
    { //
      var __ucld_2_step_lhs : integer; // line 15
      var __ucld_1_o_lhs : boolean; // line 2
      assert ((step != 0) || !(o0)); // reduced.ucl, line 23
      __ucld_1_o_lhs = true; // reduced.ucl, line 9
      o0 = __ucld_1_o_lhs; // line 0
      assert ((step != 0) || !(o0)); // reduced.ucl, line 25
      __ucld_2_step_lhs = (step + 1); // reduced.ucl, line 26
      step = __ucld_2_step_lhs; // line 0
    }
  var o0 : boolean; // reduced.ucl, line 14
  init // reduced.ucl, line 18
    { //
      var __ucld_1_o_lhs : boolean; // line 2
      var __ucld_2_step_lhs : integer; // line 15
      __ucld_1_o_lhs = o0; // line 0
      o0 = false; // reduced.ucl, line 5
      __ucld_2_step_lhs = step; // line 0
      step = 0; // reduced.ucl, line 19
    }
  control {
    v = bmc_noLTL((3,3)); // reduced.ucl, line 30
    check; // reduced.ucl, line 31
    v->print_cex((step,step), (o0,o0)); // reduced.ucl, line 32
    print_module; // reduced.ucl, line 33
  }
  // instance_var_map { 
  //   child0.o ::==> o0
  // } end_instance_var_map
  // macro_annotation_map { 
  // } end_macro_annotation_map
}

5 assertions passed.
1 assertions failed.
0 assertions indeterminate.
  PASSED -> v [Step #1] assertion @ reduced.ucl, line 23
  PASSED -> v [Step #2] assertion @ reduced.ucl, line 23
  PASSED -> v [Step #2] assertion @ reduced.ucl, line 25
  PASSED -> v [Step #3] assertion @ reduced.ucl, line 23
  PASSED -> v [Step #3] assertion @ reduced.ucl, line 25
  FAILED -> v [Step #1] assertion @ reduced.ucl, line 25
Finished execution for module: main.

Both assertions in the main module's next block read the value of o0, but the one after next(child0) incorrectly uses the next value of o0. As discussed in the uclid meeting, this may be a consequence of the child module's variable updates being inlined before assertions in the parent module are checked.

LTL bug

creating issue so we don't forget. Multiple LTL properties are currently disabled, because the auxiliary variables created for each property clash with each other and affect the soundness

bitwise operations on integers cause uncaught exceptions

I have a generated model that causes some unexpected behavior. I minimized it to the following:

module main {
  var x : integer;

  procedure foo()
  {
    if ((x ^ 3) == 1) {
    }
  }
}

Uclid5 0.9.5 says the following about this:

$ ./uclid-0.9.5/bin/uclid foo.ucl
Exception in thread "main" java.lang.ClassCastException: class uclid.lang.IntegerType cannot be cast to class uclid.lang.BitVectorType (uclid.lang.IntegerType and uclid.lang.BitVectorType are in unnamed module of loader 'app')
        at uclid.lang.ExpressionTypeCheckerPass.opAppType$1(TypeChecker.scala:370)
        at uclid.lang.ExpressionTypeCheckerPass.typeOf(TypeChecker.scala:622)
        at uclid.lang.ExpressionTypeCheckerPass.applyOnExpr(TypeChecker.scala:231)
        at uclid.lang.ExpressionTypeCheckerPass.applyOnExpr(TypeChecker.scala:213)
        at uclid.lang.ASTAnalyzer.visitExpr(ASTVistors.scala:905)
        at uclid.lang.ASTAnalyzer.$anonfun$visitOperatorApp$1(ASTVistors.scala:995)
        at scala.collection.LinearSeqOptimized.foldLeft(LinearSeqOptimized.scala:126)
        at scala.collection.LinearSeqOptimized.foldLeft$(LinearSeqOptimized.scala:122)
        at scala.collection.immutable.List.foldLeft(List.scala:89)
        at uclid.lang.ASTAnalyzer.visitOperatorApp(ASTVistors.scala:995)
        at uclid.lang.ASTAnalyzer.visitExpr(ASTVistors.scala:900)
        at uclid.lang.ASTAnalyzer.visitIfElseStatement(ASTVistors.scala:795)
        at uclid.lang.ASTAnalyzer.visitStatement(ASTVistors.scala:723)
        at uclid.lang.ASTAnalyzer.$anonfun$visitBlockStatement$2(ASTVistors.scala:788)
        at scala.collection.LinearSeqOptimized.foldLeft(LinearSeqOptimized.scala:126)
        at scala.collection.LinearSeqOptimized.foldLeft$(LinearSeqOptimized.scala:122)
        at scala.collection.immutable.List.foldLeft(List.scala:89)
        at uclid.lang.ASTAnalyzer.visitBlockStatement(ASTVistors.scala:788)
        at uclid.lang.ASTAnalyzer.visitStatement(ASTVistors.scala:722)
        at uclid.lang.ASTAnalyzer.visitProcedure(ASTVistors.scala:359)
        at uclid.lang.ASTAnalyzer.visitDecl(ASTVistors.scala:306)
        at uclid.lang.ASTAnalyzer.$anonfun$visitModule$1(ASTVistors.scala:294)
        at scala.collection.LinearSeqOptimized.foldLeft(LinearSeqOptimized.scala:126)
        at scala.collection.LinearSeqOptimized.foldLeft$(LinearSeqOptimized.scala:122)
        at scala.collection.immutable.List.foldLeft(List.scala:89)
        at uclid.lang.ASTAnalyzer.visitModule(ASTVistors.scala:294)
        at uclid.lang.ExpressionTypeChecker.visit(TypeChecker.scala:637)
        at uclid.lang.PassManager.$anonfun$_run$2(PassManager.scala:70)
        at scala.Option.flatMap(Option.scala:271)
        at uclid.lang.PassManager.$anonfun$_run$1(PassManager.scala:70)
        at scala.collection.LinearSeqOptimized.foldLeft(LinearSeqOptimized.scala:126)
        at scala.collection.LinearSeqOptimized.foldLeft$(LinearSeqOptimized.scala:122)
        at scala.collection.immutable.List.foldLeft(List.scala:89)
        at scala.collection.generic.TraversableForwarder.foldLeft(TraversableForwarder.scala:47)
        at scala.collection.generic.TraversableForwarder.foldLeft$(TraversableForwarder.scala:47)
        at scala.collection.mutable.ListBuffer.foldLeft(ListBuffer.scala:47)
        at uclid.lang.PassManager._run(PassManager.scala:67)
        at uclid.lang.PassManager.run(PassManager.scala:79)
        at uclid.UclidMain$.$anonfun$compile$4(UclidMain.scala:265)
        at scala.collection.LinearSeqOptimized.foldLeft(LinearSeqOptimized.scala:126)
        at scala.collection.LinearSeqOptimized.foldLeft$(LinearSeqOptimized.scala:122)
        at scala.collection.immutable.List.foldLeft(List.scala:89)
        at uclid.UclidMain$.compile(UclidMain.scala:262)
        at uclid.UclidMain$.main(UclidMain.scala:144)
        at uclid.UclidMain$.main(UclidMain.scala:60)
        at uclid.UclidMain.main(UclidMain.scala)

This is one of a number of models I have that exhibits this behavior. The common feature of them seems to be bitwise operations on integers (any of ^, & or ~). I think this is an error, but I was not expecting it to throw an uncaught Java exception.

CI: add CVC4

I already have CVC4 in my Paso CI: https://github.com/ekiwi/paso/blob/main/ext/cvc4.sh

TODO: change inlining semantics

inline/noinline is currently overridden if a requires statement is/isnot provided. Plan is to change this to make inline/noinline directives always be obeyed but print a warning if a requires statement is not provided and noinline is specified

TODO: add travis CI to PR checks

PR checks currently only show github actions CI

TODO: document finite_foralls

finite_foralls are introduced in #104

These should be added to the tutorial/documentation. Creating an issue so we don't forget

(assigning Yatin, could also be Chase?)

Induction bug

I believe that this inductive proof should not go through but it does:

module main {
  // Part 1: System description.
  var a, b : integer;
  var pc : integer;

  init {
    a = 0;
    b = 1;
    pc = 0;
  }
  next {
    case
    (pc < 10) : {
      call ( a', b' ) = fib0 ( a, b );
    }
    default : {
      call ( a', b' ) = fib1 ( a, b );
    }
    esac
  }

  procedure fib0 ( a : integer, b : integer )
    returns ( c: integer, d : integer )
    requires a >= 0 && b >= 0;
    ensures c <= d && c >= 0 && d >= 0;
    modifies pc;
  {
      c = b;
      d = a + b;
      pc = pc + 1;
  }

  procedure fib1 ( a : integer, b : integer )
    returns ( c: integer, d : integer )
    requires a >= 0 && b >= 0;
    ensures c <= d && c >= 0 && d >= 0;
    modifies pc;
  {
      c = a + b;
      d = b;
      pc = pc + 1;
  }

  // Part 2: System specification.
  invariant a_le_b: a <= b;
  invariant a_b_ge_0: (a >= 0 && b >= 0);

  // Part 3: Proof script.
  control {
    x = induction;
    check;
    print_results;
    x.print_cex (a, b);
  }
}

fib0 is the normal fibonacci procedure, fib1 is a buggy fibonacci procedure where the assignments have been reversed. fib0 is called if pc < 10, otherwise fib1 is called. I am not sure why the ensures clause of fib1 does not throw an error.

Verbose mode?

It would be good to add a Verbose mode in UCLID which when enabled prints on screen what UCLID is trying to solve currently.

Is there one already?

instance procedure calls use modified values

Procedure proc1 modifies x and proc2 uses x.
The following results in proc2 using the value of x from the previous step (as expected).

module m {
  ...
  next {
    call () = proc1();
    call () = proc2();
  }
  ...
}

The following results in proc2 using the new value of x.

module main {
  instance m1 : m ();
  ...
  next {
    call () = m1.proc1();
    call () = m1.proc2();
  }
  ...
}

See file test/test-instance-procedure-calls-1.ucl.

uclid-org / uclid Goto Github PK

uclid's Introduction

About

Contact us

UCLID5 Tutorial/Publication

Versions

Installation

Prerequisites:

Installation of prerequisites on Linux

Java 11

SBT (only required to build from source)

External solvers

Installation of prerequisites on Mac

Java 11

SBT (only required to build from source)

External solvers

Using the Pre-built binaries

Compiling uclid5 from source

Running UCLID

Directory Structure

Related Tools

uclid's People

Contributors

Stargazers

Watchers

Forkers

uclid's Issues

Minimal example

More details

Code

Output

Issue 1

Minimal example

Issue 2

Minimal example

Code

Output

Different results

How to reproduce?

Code

Output

Recommend Projects

Recommend Topics

Recommend Org