runtimeverification / llvm-backend

KORE to llvm translation
BSD 3-Clause "New" or "Revised" License
34 stars 19 forks source link

Exporting `kore_symbol` in `hook_events` and exposing `symbol` entry point in `kore_parser` #1064

Closed Robertorosmaninho closed 1 month ago

Robertorosmaninho commented 1 month ago

This PR introduces the new version of the LLVM Backend Proof Hints: Version 10.

The major update is in the llvm_hook_event, which will have a new field: kore_symbol. The new format of hook accepted and produced is:

symbol_name       ::= string
hook              ::= WORD(0xAA) name symbol_name location arg* WORD(0xBB) kore_term

It also exposes the symbol entry point in the kore_parser.

This modification will help the Math Proof Team from Pi2 to parse the llvm_hook_event->kore_symbol and llvm_function_event using the same method.

Baltoli commented 1 month ago

You will need to bump the hint trace format version here as you're adding new data to the trace.

Robertorosmaninho commented 1 month ago

There's a big switch-case statement where we parse sentences; is it possible to refactor the code in that part to use this new method?

I can do it in application_pattern but not in sentence. The difference is that in the last, we're setting it as hooked or not, and we're using sort_variables(symbol.get()) instead of init_pattern_arguments().

I've modified the code to use symbol in application_pattern.

Baltoli commented 1 month ago

Makes sense!