viperproject / gobra

Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.
https://gobra.ethz.ch
Other
112 stars 28 forks source link

Underspecified behaviour when evaluating Composite Literals #279

Open jcp19 opened 3 years ago

jcp19 commented 3 years ago

We are not taking into account that the order of evaluation of the components of composite literals is pretty much undefined, apart from function calls, as mentioned here. Taking an example from the go documentation,

a := 1
f := func() int { a++; return a }
x := []int{a, f()}            // x may be [1, 2] or [2, 2]: evaluation order between a and f() is not specified
m := map[int]int{a: 1, a: 2}  // m may be {2: 1} or {2: 2}: evaluation order between the two map assignments is not specified
n := map[int]int{a: f()}      // n may be {2: 3} or {3: 3}: evaluation order between the key and the value is not specified

Right now, Gobra evaluates expressions in the order they occur in a composite literal. To address this undefined behaviour, we would either need an exponential encoding to account for all execution orders, or more reasonably, reject expressions that contain side effects when they occur inside a composite literal

Felalolf commented 3 years ago

This part of the language specifications seems relatively new to me. Back when I added literals, I did not find that the semantics for composite literals are specified so I treated them the same way as calls. I got the same results when checking with the Go compiler. I guess the order of evaluation can change depending on the content of the registers.

There are several solutions:

EDIT: I was a bit blind with the math. The function is of course just f(a,b) = a!(a+1)^b. This is quite intuitive and also follows rather easily by applying the binomial law.