disabling common subexpression elimination

Stream: lean4

[Tomas Skrivan]

I would like to measure how many times a certain function gets called in an expression if naively evaluated. Just adding dbg_trace to that function does not work as there seems to be some form of common subexpression elimination. Consider this code

def foo (x y : Float) : Float :=
  dbg_trace "calling foo"
  x * y

def f (x : Float) := foo x x + foo x x

-- calling foo
-- 8.000000
#eval f 2

it prints out calling foo only once. I would expect twice.

A more complicated example:

code

def foo (x y : Float) : Float :=
  dbg_trace "calling foo"
  x * y

def fooD (x y : Float) : Float×(Float→Float×Float) :=
  (foo x y,
   fun dz =>
     (foo dz y, foo dz x))

def g (x : Float) :=
    let zdfoo := fooD x x;
    let ydg0 := zdfoo.fst;
    let zdfoo_1 := fooD ydg0 ydg0;
    let xdf0 := zdfoo_1.fst;
    let zdfoo_2 := fooD xdf0 x;
    let ydg0 := zdfoo_2.fst;
    let zdfoo_3 := fooD ydg0 ydg0;
    let xdf0 := zdfoo_3.fst;
    let zdfoo_4 := fooD xdf0 x;
    let ydg0 := zdfoo_4.fst;
    let zdfoo_5 := fooD ydg0 ydg0;
    let xdf0 := zdfoo_5.fst;
    let zdfoo_6 := fooD xdf0 x;
    let ydg0 := zdfoo_6.fst;
    (ydg0, fun dz =>
      let dxdy := Prod.snd zdfoo_6 dz;
      let dxdy_1 := Prod.snd zdfoo_5 dxdy.fst;
      let dxdy_2 := Prod.snd zdfoo_4 dxdy_1.fst;
      let dxdy_3 := Prod.snd zdfoo_3 dxdy_2.fst;
      let dxdy_4 := Prod.snd zdfoo_2 dxdy_3.fst;
      let dxdy_5 := Prod.snd zdfoo_1 dxdy_4.fst;
      let dxdy_6 := Prod.snd zdfoo dxdy_5.fst;
      let dxdy_7 := Prod.snd zdfoo dxdy_5.snd;
      let dxdy_8 := Prod.snd zdfoo_2 dxdy_3.snd;
      let dxdy_9 := Prod.snd zdfoo_1 dxdy_8.fst;
      let dxdy_10 := Prod.snd zdfoo dxdy_9.fst;
      let dxdy_11 := Prod.snd zdfoo dxdy_9.snd;
      let dxdy_12 := Prod.snd zdfoo_4 dxdy_1.snd;
      let dxdy_13 := Prod.snd zdfoo_3 dxdy_12.fst;
      let dxdy_14 := Prod.snd zdfoo_2 dxdy_13.fst;
      let dxdy_15 := Prod.snd zdfoo_1 dxdy_14.fst;
      let dxdy_16 := Prod.snd zdfoo dxdy_15.fst;
      let dxdy_17 := Prod.snd zdfoo dxdy_15.snd;
      let dxdy_18 := Prod.snd zdfoo_2 dxdy_13.snd;
      let dxdy_19 := Prod.snd zdfoo_1 dxdy_18.fst;
      let dxdy_20 := Prod.snd zdfoo dxdy_19.fst;
      let dxdy_21 := Prod.snd zdfoo dxdy_19.snd;
      dxdy_6.fst + dxdy_6.snd + (dxdy_7.fst + dxdy_7.snd) + dxdy_4.snd +
              (dxdy_10.fst + dxdy_10.snd + (dxdy_11.fst + dxdy_11.snd) + dxdy_8.snd) +
            dxdy_2.snd +
          (dxdy_16.fst + dxdy_16.snd + (dxdy_17.fst + dxdy_17.snd) + dxdy_14.snd +
              (dxdy_20.fst + dxdy_20.snd + (dxdy_21.fst + dxdy_21.snd) + dxdy_18.snd) +
            dxdy_12.snd) +
        dxdy.snd)

-- 17 × calling foo
-- 385875968.000000
#eval (g 2).2 4

which prints out calling foo only 17 times, but I would expect 7 + 22 * 2 = 51 times.

I'm generating this kind of code automatically and I want to measure how many times a certain function gets evaluated to get a better idea which code generation is better/worse. I do not want this this measurement be skewed by downstream optimizations.

[Tomas Skrivan]

The question is can I disable this common subexpression elimination? Or is there a different way to measure how many times a function gets called when expression is evaluated naively?

[James Gallicchio]

wrap it in a state monad that counts each call? :p that might be a bit of a heavy solution though...

[James Gallicchio]

(i don't know of any way to turn off the compiler optimizations other than constant lifting...)

[Tomas Skrivan]

Yeah I thought of using monads but I do not generate monadic code and turning it into monadic is probably as hard as writing a meta code that inspects the code and counts the number of calls. I really do not know how to approach this apart from effectively writing my own interpreter.