Generate kore from c translation semantics #378
Conversation
| @@ -546,8 +546,10 @@ syntax Stmt ::= Defaulted(SpecialMemberFunction, Class) [klabel(DefaultedSMF)] | |||
| <initializers>... X |-> (T |-> I::Init) ...</initializers> | |||
| requires isDeletedDefaultConstructor(X, T, C, FuncT, VM, I) | |||
|
|
|||
| syntax KItem ::= "dotInit" | |||
There was a problem hiding this comment.
Good suggestion, it just didn't occur to me. I'll change it.
semantics/c/language/common/typing.k
Outdated
| | SimplePointerType | ||
| | SimpleStructType | ||
| | SimpleUnionType | ||
| | SimpleFunctionType |
There was a problem hiding this comment.
Can lines 172-176 (in the changed file) just be removed now?
|
|
||
| // assignment expression | ||
| rule typeof(Lbl:KLabel(t(_, Mods::Set, T::SimpleType),_) => t(noQuals, Mods, T)) | ||
| requires isAssignmentKLabel(#klabel(Lbl)) | ||
| rule typeof(assignmentOp(t(_, Mods::Set, T::SimpleType),_) => t(noQuals, Mods, T)) |
There was a problem hiding this comment.
It seems a little unfortunate that macros in the LHS like this look just like any other constructor. I wonder if we shouldn't come up with some convention for macro naming that makes what's going on here a little more clear.
There was a problem hiding this comment.
I'd rather we made a change like this separately. I'd also rather we get all of my existing code that I have in my branches merged before making such an involved refactoring. But if you want, I can add this to my list of things to do once I get the linking semantics to parse with llvm.
| rule nativeDefinedBuiltins => #nativeDefinedBuiltins() | ||
|
|
||
| // defined as a K rule for if the hook is not defined | ||
| rule #nativeDefinedBuiltins() => .Map | ||
| rule [[ #nativeDefinedBuiltins() => .Map ]] |
There was a problem hiding this comment.
What's the meaning of the [[ ]] here?
There was a problem hiding this comment.
This says that #nativeDefinedBuiltins() rewrites to .Map if we match the pattern after it (in this case it will always match because it's just matching on <k> _ </k>. The reason for this is to make it so that the entire configuration is passed as one of the arguments to the hook.
| @@ -81,8 +81,81 @@ module COMPAT-SYNTAX | |||
|
|
|||
| endmodule | |||
|
|
|||
| module COMPAT-KAST [kast] | |||
There was a problem hiding this comment.
This is so this module is not imported on the llvm backend.
* minor fixes for parsing issues * remove explicit use of klabels * remove use of makeEmptyArray * ensure terms have least sort * fix return types * remove fresh var in function * fix imports * fix kseq in map * fix impure function * put functions with klabels in [kast] module * Expression => KItem * update k submodule * fix map lookup of bottom * more fixes for functions that return K * make a few constructs take kseq as argument * another fix for impure function * fix imports of kast module * a few more fixes for badly typed ksequences * fix a few bad outer casts * fix isOpaque check * fix bug where we called type() on variadic * tmp: update k submodule * update k submodule * more parsing fixes * fix some more parser errors with latest version of k * fix nested choices * fix unbound var on rhs * update k submodule * fix another parser error from merged code * update k submodule * fix withConfig * fix syntax * update k submodule * update k submodule * update k submodule * add back linc function in C * fix jan's comments * fix chris's comment
Parses, compiles, emits kore, and validates the C translation semantics. Does not yet work with linking semantics, c++ translation semantics, or execution semantics. Does not yet successfully generate a decision tree.