zetzit / zz

πŸΊπŸ™ ZetZ a zymbolic verifier and tranzpiler to bare metal C
MIT License
1.6k stars 52 forks source link

closures can't be assigned to local variables #152

Open sternenseemann opened 3 years ago

sternenseemann commented 3 years ago

Taken from the README with fixed syntax:

closure rand_t() -> int;

fn secure_random() -> int {
    return 42;
}

fn main() {
    rand_t rand = secure_random;
}

Compiling fails:

[ERROR] incompatible types ::zztest::main::rand_t and ::zztest::main::secure_random
 --> /home/lukas/src/misc/zztest/src/main.zz:8:5
  |
8 |     rand_t rand = secure_random;␊
  |     ^-------------------------^
  |
  = this expression is unprovable over incompatible types

 --> /home/lukas/src/misc/zztest/src/main.zz:8:5
  |
8 |     rand_t rand = secure_random;␊
  |     ^-------------------------^
  |
  = rand := ::zztest::main::rand_t Uninitialized

 --> /home/lukas/src/misc/zztest/src/main.zz:3:1
  |
3 | fn secure_random() -> int {␊
  | ...
6 | fn main() -> int {␊
  | ^
  |
  = ::zztest::main::secure_random := ::zztest::main::secure_random Uninitialized
aep commented 3 years ago

ah yes, closures can't be assigned to local variables. i dont know why, this looks like a bug.

aep commented 3 years ago

oh i remember why. fixing this is hard because closures are emitted as structures for capture context. this is a corner case where there's no special assignment case in symbolic, its just passed as literal = into C, and using = for structs is not legal in C. We'd either need yet another special case or finally some more generic way to assignment.

jacereda commented 3 years ago

C should handle = for structs AFAIK...


struct foo { void * p; int i; };

struct foo test() {
  struct foo a = {0,1};
  struct foo b;
  b = a;
  return b;
}