Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

LLVM backend support #558

Draft
wants to merge 85 commits into
base: master
Choose a base branch
from
Draft
Changes from 1 commit
Commits
Show all changes
85 commits
Select commit Hold shift + click to select a range
4a083ff
LLVM backend: kcc/runner scripts.
Jun 28, 2019
a8061d4
Dockerfile: build LLVM backend.
chathhorn Aug 28, 2019
b9cd90a
Jenkinsfile: disable rule parse profiling.
chathhorn Aug 30, 2019
2200763
Jenkinsfile: remove parse profiling.
chathhorn Sep 19, 2019
afb5e12
Enable kore output for C++ parser.
chathhorn Oct 22, 2019
5b609e4
generate readable dumps
h0nzZik Feb 6, 2020
03fc204
llvm-krun -save-temps
h0nzZik Feb 6, 2020
2d91b87
kcc -fdebug-translation
h0nzZik Mar 2, 2020
3861e02
append sorts to symbols
h0nzZik Mar 5, 2020
e55a487
fix lookupEnumerator
h0nzZik Mar 5, 2020
05422b7
fix
h0nzZik Mar 5, 2020
ed47382
rename isNoInit => hasInit
h0nzZik Mar 13, 2020
b291263
Revert "append sorts to symbols"
h0nzZik Mar 13, 2020
18f40a9
C++ semantics [symbol] tags.
chathhorn Oct 22, 2019
ee06607
update K
h0nzZik Mar 27, 2020
b8e640b
llvm debug
h0nzZik Mar 27, 2020
a718f5e
UnknownCabsLoc
h0nzZik Mar 25, 2020
d6af82b
workaround for K bug https://github.com/kframework/k/issues/1193
h0nzZik Apr 1, 2020
28cb90a
C++ parser: toplevel sort is KItem
h0nzZik Apr 1, 2020
1a8cdb4
C++ parser #NoName
h0nzZik Apr 2, 2020
aad43ba
[symbol]
h0nzZik Apr 7, 2020
df184b4
remove overloaded ExprLoc
h0nzZik Apr 7, 2020
01944f2
C++ [symbol]
h0nzZik Apr 9, 2020
f88d3b3
fix toCPPTypes
h0nzZik Apr 9, 2020
5ffaa52
fix sorts
h0nzZik Apr 9, 2020
da13059
fix NoInit
h0nzZik Apr 10, 2020
b1e20bd
fix sorts
h0nzZik Apr 10, 2020
f82292b
strip traces in linking semantics
h0nzZik Apr 15, 2020
2c5ded1
fix sort
h0nzZik Apr 15, 2020
edcc511
fix `assertInBounds` and `assert`
h0nzZik Apr 15, 2020
12d1c03
do not escape strings twice
h0nzZik Apr 16, 2020
367ef5e
fix sorts
h0nzZik Apr 16, 2020
5e80cb0
IfAStmtD
h0nzZik Apr 17, 2020
f6cb33b
operatorXYZ_CPP-SYNTAX_OpId
h0nzZik Apr 17, 2020
679b821
fix sorts
h0nzZik Apr 17, 2020
280c0f5
fix sorts
h0nzZik Apr 17, 2020
42ae7ca
isKResult
h0nzZik Apr 17, 2020
f2f2798
fix sorts
h0nzZik Apr 17, 2020
dd76982
fix sorts
h0nzZik Apr 17, 2020
eb36782
Fix sorts
h0nzZik Apr 17, 2020
095d645
Parser: 'And-'
h0nzZik Apr 17, 2020
fbdad09
We no longer have sort BraceInit
h0nzZik Apr 17, 2020
1867f49
fix sorts
h0nzZik Apr 17, 2020
8219c33
fix csetunion
h0nzZik Apr 20, 2020
b2cd6d8
LLVM backend: kcc/runner scripts.
Jun 28, 2019
5b76644
Dockerfile: build LLVM backend.
chathhorn Aug 28, 2019
9bd143f
Jenkinsfile: disable rule parse profiling.
chathhorn Aug 30, 2019
61bccb4
Jenkinsfile: remove parse profiling.
chathhorn Sep 19, 2019
6be94d3
Enable kore output for C++ parser.
chathhorn Oct 22, 2019
b12feca
generate readable dumps
h0nzZik Feb 6, 2020
ae8d900
llvm-krun -save-temps
h0nzZik Feb 6, 2020
0d2a4bd
kcc -fdebug-translation
h0nzZik Mar 2, 2020
04e280c
append sorts to symbols
h0nzZik Mar 5, 2020
b904c32
fix lookupEnumerator
h0nzZik Mar 5, 2020
bd1fd9c
fix
h0nzZik Mar 5, 2020
722765b
rename isNoInit => hasInit
h0nzZik Mar 13, 2020
f8f01a3
Revert "append sorts to symbols"
h0nzZik Mar 13, 2020
3640887
C++ semantics [symbol] tags.
chathhorn Oct 22, 2019
315a00d
update K
h0nzZik Mar 27, 2020
cc2ef43
llvm debug
h0nzZik Mar 27, 2020
f35abc8
UnknownCabsLoc
h0nzZik Mar 25, 2020
0d13a74
workaround for K bug https://github.com/kframework/k/issues/1193
h0nzZik Apr 1, 2020
dd08978
C++ parser: toplevel sort is KItem
h0nzZik Apr 1, 2020
0de15eb
C++ parser #NoName
h0nzZik Apr 2, 2020
63b33c7
fix kcc script merge conflict
Apr 24, 2020
04e182f
Merge branch 'llvm' into latest
h0nzZik Apr 29, 2020
998108d
fix checkLoc
h0nzZik Apr 29, 2020
6124977
fix missing [function]
h0nzZik Apr 29, 2020
c323c29
little refactoring
h0nzZik Apr 29, 2020
a937f17
fix missing [symbol]
h0nzZik Apr 29, 2020
76e5953
Constructor takes AStmt
h0nzZik Apr 30, 2020
0c3571d
Revert "fix csetunion"
h0nzZik Apr 30, 2020
614aeca
make csetunion work with types
h0nzZik Apr 30, 2020
93a6b30
fix sorts
h0nzZik Apr 30, 2020
45c70ba
remove the content of `<initializers>` in the link time
h0nzZik Apr 30, 2020
3dd482d
fix sorts
h0nzZik Apr 30, 2020
8810ac8
parser: skip default arguments in a call
h0nzZik May 1, 2020
8dcf2ed
fix sorts
h0nzZik May 11, 2020
be8951f
fixes
h0nzZik May 12, 2020
eda43b4
kcc -fdebug-linking
h0nzZik May 14, 2020
3818a61
kcc: fix generating kcc_config from linking semantics
h0nzZik May 14, 2020
2891833
linking: overwrite with the same value
h0nzZik May 14, 2020
a5b4248
brace initialization: fix sorts
h0nzZik May 14, 2020
8615063
for: fix sort
h0nzZik May 14, 2020
e88a01b
isKResult
h0nzZik May 14, 2020
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
fix sorts
h0nzZik committed May 11, 2020
commit 8dcf2ed581a7214f13cbef33d0b9ea4fee8e59ba
13 changes: 10 additions & 3 deletions semantics/cpp/language/execution/binding.k
Original file line number Diff line number Diff line change
@@ -8,7 +8,7 @@ module CPP-BINDING-SYNTAX

syntax KItem ::= bindParam(CId, CPPType, Init) [klabel(bindParamCpp3)]

syntax KItem ::= setThis(Expr) [strict(c)]
syntax KItem ::= setThis(K)
endmodule

module CPP-EXECUTION-BINDING
@@ -23,14 +23,21 @@ module CPP-EXECUTION-BINDING
imports CPP-SYNTAX
imports CPP-TYPING-SYNTAX

rule <k> setThis(.K) => .K ...</k>
<this> _ => .K </this>

rule setThis(E:Expr) => #setThis(E)

syntax KItem ::= #setThis(Expr) [strict(c)]

rule <k> (.K => bindParam(X, T, V))
~> bind(
(ListItem(X::CId) => .List) _,
(ListItem(T:CPPType) => .List) _,
(ListItem(V::Init) => .List) _)
...</k>

rule <k> (.K => setThis(V))
rule <k> (.K => #setThis(V))
~> bind(
_,
(ListItem(implicitObjectParameter(T::CPPType)) => .List) _,
@@ -52,7 +59,7 @@ module CPP-EXECUTION-BINDING

rule bindVariadics(.List) => .K

rule <k> setThis(Obj:PRVal) => .K ...</k>
rule <k> #setThis(Obj:PRVal) => .K ...</k>
<this> _ => Obj </this>

rule <k> beginConstruction(Obj:LVal, IsBaseClassSubobject:Bool) => Obj ...</k>
4 changes: 2 additions & 2 deletions semantics/cpp/language/execution/expr/members.k
Original file line number Diff line number Diff line change
@@ -15,10 +15,10 @@ module CPP-EXECUTION-EXPR-MEMBERS

rule <k> evalBraceOrEqualInitializer(C::Class, lv(Loc::SymLoc, Tr::Trace, T::CPPType) #as Base::LVal, E::Expr) => setThis(prv(Loc, Tr, type(pointerType(type(classType(C)))))) ~> E ~> returnFromBraceOrEqualInitializer(Base, OldScope) ~> setThis(OldThis) ...</k>
<curr-scope> OldScope::Scope => classScope(C, true) </curr-scope>
<this> OldThis::PRVal </this>
<this> OldThis::K </this>
requires Execution()

rule <k> V:Val ~> (returnFromBraceOrEqualInitializer(_, Scope::Scope) ~> setThis(OldThis::PRVal) => .K) ...</k>
rule <k> V:Val ~> (returnFromBraceOrEqualInitializer(_, Scope::Scope) ~> setThis(OldThis::K) => .K) ...</k>
<curr-scope> _ => Scope </curr-scope>
<this> _ => OldThis </this>
requires Execution() andBool notBool (isLExpr(V) orBool isPRExpr(V))