8000 Code gerneration: deterministic "non-deterministic" choice · Issue #52 · kenmcmil/ivy · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
ArneVogel opened this issue Feb 18, 2022 · 0 comments
Open

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

ArneVogel opened this issue Feb 18, 2022 · 0 comments

Comments

@ArneVogel
Copy link
ArneVogel commented Feb 18, 2022 •
edited
Loading

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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@ArneVogel
0