GaloisInc / ivory

The Ivory EDSL
http://ivorylang.org
BSD 3-Clause "New" or "Revised" License
393 stars 28 forks source link

Remove `IvoryZero` constraint from `ifte` and `cond` #116

Open cblp opened 6 years ago

cblp commented 6 years ago

I want to select a ref value by some condition.

getRef1, getRef2 :: Ivory eff (Ref s a)
ref3 = ifte c getRef1 getRef2

This is safe but Ivory use 0 initialized variable internally, and references can't be initialized with zero, so Ivory doesn't allow this.

So I have to use pointers instead of references and assert they are valid. Assertions, assertions everywhere!

Meanwhile, MISRA says:

Rule 9.1 (required): All automatic variables shall have been assigned a value before being used. The intent of this rule is that all variables shall have been written to before they are read. This does not necessarily require initialization at declaration.

So you don't need to zeroify local variable before an if statement. You don't need to initialize it at all.

Currently, Ivory internal representation requires local variables be initialized. So we need to relax this requirement, only internally, without exposure to the user.

I can do this, but I need an advice on how to do this. Extend Init type? XInit? local representation?