Linear normalisation

[zilinc]

Issue by lim060 Thu Jul 23 17:29:30 2015 Originally opened as https://github.csiro.au/ts-filesystems/Cogent/issues/92

---

The current implementation of ANF creates severe problems with code size. It floats out Ifs and Cases, causing exponential growth. As an example, see fsop_do_setattr in bilbyfs, which has five if-statements.

It's obvious that this is bad for code size, which is bad for verification (Isabelle tools are slow). However, it's also a problem because the floating causes non-trivial code movement. We can't just inline the an_xx-binds and get an obvious equality.

ER: Implement normalisation with linear overhead. KNF, our previous quick-fix for ANF, still isn't linear; e.g. it expands ostore_read in bilbyfs (case (if ...) of...).

Proposed linear normalisation (“LNF”?) rules:

• Source: let w = case x of y | z in e
  • ANF: let _v1 = <norm x> in case _v1 of <norm e ∘ y> | <norm e ∘ z>
  • LNF: let _v1 = <norm x>; w = case _v1 of <norm y> | <norm z> in <norm e>
• Source: let w = if x then y else z in e
  • ANF: let _v1 = <norm x> in if _v1 then <norm e ∘ y> else <norm e ∘ z>
  • LNF: let _v1 = <norm x>; w = if _v1 then <norm y> | <norm z> in <norm e>

Rules for other Exprs probably don't need to change.

Milestones:

1. Implement LNF
2. Update verification toolchain (C-refinement may be grazed a bit)
3. Check for performance regressions
4. Phase out ANF

[zilinc]

Comment by lim060 Thu Jul 23 17:32:28 2015

---

Testcase 1:

f: <A Bool | B ()> -> <A Bool | B ()>
f x = let x' = (x
                | A b -> if b then A (not b) else B ()
                | B u -> A True)
                | A b -> if b then B () else A (not b)
                | B u -> A True
      in if x'
            | A b -> b
            | B u -> False
         then x'
              | A b -> B ()
              | B u -> A False
         else x
              | A b -> A (not b)
              | B u -> B u

[gteege]

I propose to make --fnormalisation=knf (or lnf, when implemented) the default in the Cogent compiler. If you do not expect the ANF behavior you wonder why the compiler runs for hours when you added only some lines of code to your program...