compiler metrics #425
compiler metrics #425
Conversation
…/bedrock2 into regalloc-metrics
…ntics not updated yet
…/bedrock2 into regalloc-metrics
…ec to fix build error
…etrics Conflicts: compiler/src/compiler/FlatImp.v compiler/src/compiler/FlatToRiscvMetric.v compiler/src/compiler/FlattenExpr.v compiler/src/compiler/RegAlloc.v compiler/src/compiler/Spilling.v
side effects: - breaks useimmediate - fixes spilling
it seems i am trying to do too many things at once so i am committing the shared things so that i do not have to worry about missing dependencies due to commit order
The spilling phase adds some boilerplate inside functions and around function calls, so we need to account for it by making things artificially more expensive before the spilling phase. In an effort to avoid monolithic commits, this is a partial commit, so the code definitely doesn't compile in the current state since lots of things changed as a side effect. There are a few comments that say "cost_something constraint:", which document the various constraints on the magic numbers chosen as upper bounds for the costs (100, 95, 50). These should probably change to better numbers at some point.
The pipeline now knows that metrics are preserved throughout. Many further changes are needed in RegAlloc.v and UseImmediate.v, so changes to theorems in those files are not included in this commit (and it will therefore not compile by itself as a result).
|
@samuelgruetter I think this branch should be in a pretty good state to merge now! A few notes:
|
bedrock2/src/bedrock2/MetricLoops.v
Outdated
|
|
||
| eapply Hexit. | ||
| (*Qed.*) | ||
| Admitted. |
There was a problem hiding this comment.
Please do not admit any lemmas. If there is partial work in a lemma that you would not like to delete but also don't want to finish right now, you can use Abort instead of Admitted, so that the lemma can't be used by accident.
There was a problem hiding this comment.
Whoops, I didn't realize the WIP loop lemmas had made it into the PR; I deleted everything in that file that isn't finished (including the commented out stuff), possibly to be added back later now added back with correct proofs!
There was a problem hiding this comment.
(pinging @samuelgruetter since i believe there are no remaining outstanding comments)
to be restored later
|
Merged, thanks @tckmn 🎉 For the record, there are still a few points that would be nice to address in a later PR:
But to avoid that this PR goes stale and to make sure others can work on top of this, I now merged this PR. |
Some comments on the code as I'm looking the whole thing over now:
I have only just now realized the ipow example no longer compiles, because I factored out lots of hardcoded constants into functions like
cost_op. This should be extremely easy to fix at the tactic automation level (but I'm making this pull request now in the interest of being able to see the code sooner).In the previous code, the large constant bound on function calls was added twice in the semantics, once in the
exec fbodyjudgment and once in the postcondition. I don't really understand why this is, but I kept them both (ascost_call_internalandcost_call_external). As far as I can tell, only one of these is needed, and putting it in either place works just as well.