search

pepper-project / pequin

A system for verifying outsourced computations, and applying SNARKs. Simplified release of the main Pepper codebase.
Other
122 stars 46 forks source link

update type of lval after ramget using declared Type #61

Closed noresistence closed 5 years ago

noresistence commented 5 years ago

... and throw an error (with a meaningful description) if lval is not an instance of VarLvalue.

This is my fix for https://github.com/pepper-project/pequin/issues/59.

As far as i understand the problem, the above patch fixes the issue. I do not know if maybe there is another location in the code where the same problem occurs, you should have a look at that. The fix changes the type of the lvalue that has been created during the first initialisation of the variable. That undoes the optimization of the type. In my code example, this has no effect, as the value is overridden immediately; but it might have an effect if:

In that scenario (which i have not tested) the patch might also change the type hint in the variable table retroactively and undo type optimizations. Might cause some issues if the type has been set to be bigger than the declared type? (Wouldn't be legal C code, but seems to be the current handling of integer overflows in pequin) But other than for optimization, the type of an lvalue does not seem to have any effect on the computation anyway. I might be completely wrong here, though.

maxhowald commented 5 years ago

Thanks a ton for tracking this down! The fix looks right (or at least, good enough) to me. In the past we haven't worried about handling undefined behavior too sensibly, so I think the issue you mention should be fine.

One thing, I think the same fix should also go here: https://github.com/pepper-project/pequin/blob/e892f0a3dbfba192442f8349da080b83e2171a1c/compiler/frontend/src/SFE/Compiler/RamPutEnhancedStatement.java#L82

Can you update the PR before I merge it?

noresistence commented 5 years ago

Sure, I could add that. But I am not sure if it makes sense at this place. My understanding of the RAMPUT operation is that the content of lval will be assigned to a some address that is accessible by index. But this should not change the content of lval here, and the address should be a new variable anyway. Thus, why should the optimized type of the lval be updated here?

In the RAMGET, it had to be updated, because the content of the lval changed and the optimized type might not fit anymore.

maxhowald commented 5 years ago

I think your'e right. Good catch, again. I'll merge it as-is.