search

kenmcmil / ivy

IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Other
77 stars 24 forks source link

Code gerneration: deterministic "non-deterministic" choice #52

Open ArneVogel opened 2 years ago

ArneVogel commented 2 years ago

Following http://microsoft.github.io/ivy/language.html#non-deterministic-choice I found a bug with the code generation of non-deterministic choices. Example ivy program:

#lang ivy1.7

type money
object account = {
    individual balance : money

    after init {
        balance := 0
    }

    action rand_add returns (x:money) = {
        if * {
            x := 1
        } else {
            x := 2
        }
        balance := balance + x;
        # ensure x = 1 | x = 2
    }

    action get_balance returns(x:money) = {
        x := balance
    }
}

export account.rand_add
export account.get_balance

interpret money -> bv[16]

Expected behavior: rand_add randomly adds 1 or 2 to the balance. Actual behaviour: generated code of rand_add only ever adds 1 to the balance.

Output of the test (same behavior in the repl) ``` $ ivy_to_cpp target=test build=true correct_rand.ivy g++ -Wno-parentheses-equality -std=c++11 -I /usr/lib/python2.7/site-packages/ivy/include -L /usr/lib/python2.7/site-packages/ivy/lib -Xlinker -rpath -Xlinker /usr/lib/python2.7/site-packages/ivy/lib -g -o correct_rand correct_rand.cpp -lz3 -pthread ``` ``` $ ./correct_rand > account.rand_add = 1 > account.rand_add = 1 > account.get_balance = 2 > account.get_balance = 2 > account.rand_add = 1 > account.get_balance = 3 > account.rand_add = 1 > account.get_balance = 4 > account.get_balance = 4 > account.rand_add = 1 > account.rand_add = 1 > account.get_balance = 6 > account.get_balance = 6 > account.rand_add = 1 > account.get_balance = 7 > account.get_balance = 7 > account.get_balance = 7 > account.rand_add = 1 > account.rand_add = 1 > account.get_balance = 9 > account.rand_add = 1 > account.rand_add = 1 > account.rand_add = 1 > account.rand_add = 1 > account.rand_add = 1 > account.rand_add = 1 > account.rand_add = 1 > account.rand_add = 1 > account.rand_add = 1 > account.rand_add = 1 > account.get_balance = 19 > account.get_balance = 19 > account.rand_add = 1 > account.rand_add = 1 > account.rand_add = 1 > account.get_balance = 22 > account.rand_add = 1 > account.get_balance = 23 > account.get_balance = 23 > account.rand_add = 1 > account.rand_add = 1 > account.get_balance = 25 > account.get_balance = 25 > account.get_balance = 25 > account.get_balance = 25 > account.rand_add = 1 > account.get_balance = 26 > account.rand_add = 1 > account.rand_add = 1 > account.get_balance = 28 > account.get_balance = 28 > account.get_balance = 28 > account.get_balance = 28 > account.rand_add = 1 > account.rand_add = 1 > account.get_balance = 30 > account.get_balance = 30 > account.rand_add = 1 > account.get_balance = 31 > account.rand_add = 1 > account.rand_add = 1 > account.rand_add = 1 > account.get_balance = 34 > account.rand_add = 1 > account.rand_add = 1 > account.get_balance = 36 > account.get_balance = 36 > account.rand_add = 1 > account.rand_add = 1 > account.get_balance = 38 > account.rand_add = 1 > account.rand_add = 1 > account.rand_add = 1 > account.get_balance = 41 > account.rand_add = 1 > account.get_balance = 42 > account.get_balance = 42 > account.rand_add = 1 > account.get_balance = 43 > account.rand_add = 1 > account.get_balance = 44 > account.rand_add = 1 > account.rand_add = 1 > account.rand_add = 1 > account.rand_add = 1 > account.get_balance = 48 > account.rand_add = 1 > account.rand_add = 1 > account.get_balance = 50 > account.get_balance = 50 > account.rand_add = 1 > account.rand_add = 1 > account.get_balance = 52 > account.get_balance = 52 > account.get_balance = 52 > account.rand_add = 1 > account.rand_add = 1 > account.rand_add = 1 > account.rand_add = 1 > account.get_balance = 56 test_completed ```

ivy_check complains if I remove the x = 2 from the ensure so that code path of ivy does not seem to be effected.

Looking at the generated code it seems like https://xkcd.com/221/ was taken to literally.

int correct_rand::___ivy_choose(int rng,const char *name,int id) {
        return 0;
    }

unsigned correct_rand::ext__account__rand_add(){
    unsigned x;
    x = (unsigned)___ivy_choose(0,"fml:x",0);
    {
        int __tmp0;
        __tmp0 = (int)___ivy_choose(0,"___branch",14);
        if(__tmp0 == 0){
            x = (1 & 65535);
        }
        else {
            x = (2 & 65535);
        }
        account__balance = ((account__balance + x) & 65535);
    }
    return x;
}

https://github.com/kenmcmil/ivy/blob/master/ivy/ivy_to_cpp.py#L2862