Debugger: Example use cases

Variable queries

Datatypes

> run
Error: Assertion violation 
 |
 |   1   datatype Many = C1(x:int) | C2(x:int) | C3(x:int) | C4(x:int) | C5(x:int)
 |   2   function GetX(m:Many) : int { m.x }
 |   3   predicate GoodMany(m:Many)
 |   4   {
 |   5     match m 
 |   6       case C1(x) => x > 0
 |   7       case C2(x) => x > 0
 |   8       case C3(x) => true
 |   9       case C4(x) => x > 0
 |  10       case C5(x) => x > 0
 |  11   }
 |  12
 |  13   method T_datatype2(m:Many)
 |  14     requires GoodMany(m)
 |  15   {
 |  16     assert GetX(m) > 0;
 |------------------------^ here  
    17   }

> ? m

C3(0)

Collections

> run
Error: Assertion violation 
 |
 |   1	method T_map1(m:map<int,int>, key:int, msg:int) 
 |   2	{
 |   3	    var m' := m[key := msg];    
 |   4	    assert m'.Values == m.Values + {msg};
 |----------------------------^
     5	}

> ? m

{ 42 -> 22 }

> ? key

  42

> ? msg

  15

> ?rhs

{ 15, 22 }

> ?lhs

{ 15 }

Quantified Variables

> run
Error: Assertion violation 
 | 
 |   1	method T_int_quantifier0()   
 |   2	{
 |   3	  assert forall i:int :: i > 0; 
 |-----------------^ here
     4	}

> ? i

0

Previous Values

> run
Error: Assertion violation 
 |    
 |   1	method test(x:int) {
 |   2	  var y := x + 1;
 |   3	  y := y + 1;
 |   4	  y := y + 1;
 |   5	  assert y > 2*x;
 |-----------------^
     6	}

> ? y

9

> ? x

6

> ? y @ 2

7

> ? y @ 3

8

Local Variables

> run
Error: Assertion violation 
 |    
 |   1	method test(x:int) {
 |   2	  var y;
 |   3	  if (x > 0) {
 |   4	    y := x + 1;
 |   5	  } else {
 |   6	    y := x;
 |   7	  }
 |   8	
 |   9	  assert y == x;
 |------------------^ here
    10	}

> locals

x -> 4
y -> 5

> run
Error: Assertion violation 
 |
 |   1	datatype Hand = Left(x:int, y:bool) | Right(a:int, b:int)
 |   2	
 |   3	method T_datatype0(h0:Hand, h1:Hand)
 |   4	{
 |   5	  assert h0 == h1;
 |-------------------^
     6	}

> locals

h0 -> Left(0, 1)
h1 -> Right(0, 1)

Interactive Expansion

> run
Error: Assertion violation 
 |
 |   1	predicate F(x:int, y:int) {
 |   2	  x + y > 5 && x > y && y > 0
 |   3	}
 |   4	
 |   5	predicate G(z:int) {
 |   6	  z > 42 || z < -5
 |   7	}
 |   8	
 |   9	predicate H(a:int, b:int, c:int) {
 |  10	  F(a, b) || (G(a) && F(b, c))
 |  11	}
 |  12	
 |  13	function Fun(d:int, e:int) : int {
 |  14	  2*d + 5*e
 |  15	}
 |  16	
 |  17	
 |  18	method test(h:int) {
 |  19	  assert H(Fun(h, 3), 7, h*2);
 |---------------^ here
    20	}

> ? h

5

> ? Fun(h, 3)

25

> expand H

Error: Assertion violation 
 |
 |  assert F(25, 7) || (G(25) && F(7, 10));
 |------------------------^

> expand G

Error: Assertion violation 
 |
 |  assert 25 > 42 || 25 < -5;
 |------------------^

Control Flow

> run
Error: Assertion violation 
 |    
 |   1	method test(x:int) {
 |   2	  var y;
 |   3	  if (x > 0) {
 |   4	    y := x + 1;
 |   5	  } else {
 |   6	    y := x;
 |   7	  }
 |   8	
 |   9	  assert y == x;
 |------------------^ here
    10	}

> locals

x -> 4
y -> 5

> backtrace

     1	method test(x:int) {
     2	  var y;
     3	  assume (x > 0) 
     4	  y := x + 1;
     8	
     9	  assert y == x;

Preconditions

> run

Error: Precondition failure
 |
 |   1	method caller() {
 |   2	  callee(2, 4, 8);
 |-----------^ here
     3	}

Related location: This precondition might not hold:
 |
 |   1	method callee(x:int, y:int, z:int) 
 |   2	  requires F(x) + G(y) + H(x, y, z) > z
 |------------^

> expand

Error: Assertion violation 
 |
 |  assert F(2) + G(4) + H(2, 4, 8) > 8
 |----------------------------------^

> expand

Error: Assertion violation 
 |
 |  assert 1 + 2 + 3 > 8
 |-------------------^

Additional Assert/Assumes

> run
Error: Assertion failure
 |    
 |   1	method test() {
 |   2	  assert ComplexPredicate(0);
 |----------------------^
     3	}

> try assert SimplerPredicate(5)

Verified

> try assert MediumPredicate(7)

Error: Assertion failure

> try assume MediumPredicate(6)   // Tries the most recent assertion, given this assumption

Verified: assert MediumPredicate(7)

> pop   // Move to previous assertion failure

Error: Assertion failure
 |    
 |   1	method test() {
 |   2	  assert ComplexPredicate(0);
 |----------------------^
     3	}

> try assume MediumPredicate(7)

Verified: assert ComplexPredicate(0);

Profiling

> run
Error: Timed out after 30 seconds
 |    
 |   1	method test() {
 |   2	  assert ComplexPredicate(0);
 |----------------------^
     3	}

> profile

  Time Spent
  ----------
    5% Dust
    5% Z3 integer theory
   90% Quantifier instantiations

  Top quantifiers
  ---------------

  Instantiations  Location     Quantifier
  --------------  --------     ----------
  10,000          A.ds:50,22    forall x :: F(x) == F(x + 1)
   5,000          B.ds:75,12    forall ticket :: Expired(ticket) ==> Invalid(ticket)
   1,000          C.ds:12,15    forall student :: Late(student) ==> Fail(student)