search

kframework / c-semantics

Semantics of C in K
Other
303 stars 40 forks source link

Fix conditional timeout #637

Closed virgil-serbanuta closed 3 years ago

virgil-serbanuta commented 3 years ago

I think the conditional timeout is caused by the following rules in semantics/c/language/translation/typing/expr.k

     rule (.K => elaborate(noEval(elabResult(E1)), noEval(elabResult(E2))))
          ~> typeof(_ ? E1:KItem : E2:KItem)

     context elaborateDone(_, _) ~> typeof(_ ? (HOLE:KItem => typeof(HOLE)) : _) [result(Type)]
     context elaborateDone(_, _) ~> typeof(_ ? _ : (HOLE:KItem => typeof(HOLE))) [result(Type)]

together with this rule from semantics/c/language/translation/expr/conditional.k

     rule (.K => typeof(C ? E1 : E2)) ~> evalConditional(C::RValue, E1:RValue, E2:RValue)

which cause the type of conditionals like a ? b : (c ? d : (e ? f : g)) to have an exponential elaboration: computing the type for x ? y : z implies computing elaborate(noeval(z)), which implies computing typeof(z) if z is a conditional; it also implies computing typeof(z) directly in the elaborateDone context. So we compute typeof(z) twice, and if z is of the form p ? q : r, we will compute typeof(r) four times, i.e. twice for each time we compute typeof(z), and so on.

This PR partly fixes the exponential algorithm by postponing the elaboration of the two noEval expressions above until they are actually needed.

dwightguth commented 3 years ago

I'm not quite sure I follow this PR. Can you explain what the bad case of the evaluation order was and how this PR fixes it?

virgil-serbanuta commented 3 years ago

I'm not quite sure I follow this PR. Can you explain what the bad case of the evaluation order was and how this PR fixes it?

I changed the PR description, does it look better now?