CODEWITHSUNDEEP
dafny
Boro Sitnikovski
Boro Sitnikovski

Reputation: 135

Verification involving arrays

First off, I want to thank Rustan and the whole community for the work you put on Dafny. It is an amazing language!

I am working on my Master's thesis which is about formal verification of virtual machines using Dafny.

This is how I define (a stripped version of) a virtual machine:

class VM
{
    var v: array<bv8>;
    var I: bv16;
    var memory: array<bv8>;
    predicate Valid()
      reads this
    {
        v.Length == 16
        && memory.Length == 0x0FFF
    }

    constructor Init()
      ensures Valid()
    {
        v := new bv8[16];
        I := 0;
        memory := new bv8[0x0FFF];
    }
}

So far so good. I have a few methods that mutate the state of this machine. In particular, here's one:

method parse_opcode_registers(vm: VM, opcode: bv16)
  requires vm.Valid()
  modifies vm`I, vm.v
{
    var i: int := 0;
    var bound := ((opcode & 0x0F00) >> 8) as int;

    if opcode & 0xF0FF == 0xF065
    {
        while i < bound && vm.I as int < vm.memory.Length
          decreases bound - i
        {
            vm.v[i] := vm.memory[vm.I];
            i := i + 1;
            vm.I := vm.I + 1;
        }
    }
}

This passes Dafny's verification. However, the issue occurs when there exists a caller for this method. Namely, the following code will produce an error call may violate context's modifies clause:

method Main() {
    var vm := new VM.Init();
    parse_opcode_registers(vm, 0xF018);
}

Any hints would be appreciated.

Upvotes: 1

Views: 180

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

You need to add ensures fresh(v) to the Init constructor of VM.

Basically, the problem is that Dafny is worried because parse_opcode_register claims to modify vm.v, but Dafny isn't sure where vm.v came from. Remember that Dafny analyzes the program one method at a time, so it does not look inside the constructor Init while analyzing Main. Instead, Dafny only looks at the pre/postcondition. That's why adding fresh(v) to the postcondition fixes it.

The meaning of fresh(blah) is that blah was freshly allocated during the execution of the method.

For more, see the FAQ question about modifies clauses.

Upvotes: 1

Related Questions