search

kframework / llvm-semantics

Formal semantics of LLVM IR in K
43 stars 9 forks source link

How to use this semantics in 2022? #49

Open Stevengre opened 1 year ago

Stevengre commented 1 year ago

I'm really interested in the most complete formal semantics of llvm, and want to try it. But there are some challenge for me to try it.

  1. Which K-Version should I use?
  2. Which Backend should I use?
  3. Which file should I kompile?

I have tried "kompile semantics/llvm-semantics.k --backend java" in "5.4.0", and an error occurred:

[Error] Outer Parser: Encountered "[".
Was expecting one of: ["List", "NeList", <UPPER_ID>, <NAT>]
        Source(/mounted/semantics/llvm-syntax.k)
        Location(25,35,25,35)
        25 |        syntax HexConstant ::= Token {[u s]?[0][x][K M L H]?[0-9 a-f A-F]*}
[onlyLabel]

I really want to try this excellent work! Thank you so much!

Stevengre commented 1 year ago

https://github.com/liyili2/llvm-semantics-1 gives the result