uclid-org / uclid Goto Github PK

View Code? Open in Web Editor NEW

135.0 135.0 32.0 79.75 MB

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 People

Contributors

Stargazers

Watchers

uclid's Issues

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?)

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.

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);
  }
}

[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?

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

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;
  }
}

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.

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

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.

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.

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.

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.

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

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.

Record Rewriter's Bugs

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

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?

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.

[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).

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.

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.

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.

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);

upgrade SBT

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

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;
  }
}

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.

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?

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`

TODO: add travis CI to PR checks

PR checks currently only show github actions CI

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.

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.

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
  }

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.

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).

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.

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

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.

error splitting commands

uclid test-array-record.ucl

(has no commands)

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)

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

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

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!

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

replace genericProofCommand

creating issue as reminder. cc @FedericoAureliano @DemetrisChr

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.

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.

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

CI: add CVC4

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

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;
    }
}`

```

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)

uclid-org / uclid Goto Github PK

uclid's People

Contributors

Stargazers

Watchers

Forkers

uclid's Issues

Code

Output

Code

Output

Issue 1

Minimal example

Issue 2

Minimal example

Minimal example

More details

Different results

How to reproduce?

Code

Output

Recommend Projects

Recommend Topics

Recommend Org