Skip to content

Commit 13076e1

Browse files
BaltoliBaltoli
authored
Merge branch 'master' into evaluate-2
2 parents 54b1534 + f43af65 commit 13076e1

File tree

18 files changed

+3061
-75
lines changed

18 files changed

+3061
-75
lines changed

‎bin/llvm-kompile-clang

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -131,12 +131,12 @@ if [[ "$OSTYPE" == "darwin"* ]]; then
131131
flags=(
132132
"-L@BREW_PREFIX@/opt/libffi/lib"
133133
"-L@BREW_PREFIX@/lib"
134-
"-Wl,-u,_sort_table"
134+
"-Wl,-u,_table_getArgumentSortsForTag"
135135
"-I" "@BREW_PREFIX@/include"
136136
)
137137
else
138138
libraries=("-ltinfo")
139-
flags=("-Wl,-u,sort_table")
139+
flags=("-Wl,-u,table_getArgumentSortsForTag")
140140
fi
141141

142142
llc_flags+=("--relocation-model=pic")

‎debug/kgdb.py

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -610,7 +610,7 @@ def append(self, subject, isVar, sort):
610610
argData = layoutData['args'] + i
611611
arg = subject.cast(self.long_int) + int(argData.dereference()['offset'])
612612
cat = argData.dereference()['cat']
613-
sort = gdb.lookup_global_symbol("sort_table").value()[tag][i].string("iso-8859-1")
613+
sort = gdb.lookup_global_symbol("table_getArgumentSortsForTag").value()[tag][i].string("iso-8859-1")
614614
if cat == @MAP_LAYOUT@:
615615
self.appendMap(arg.cast(self.map_ptr), sort)
616616
elif cat == @RANGEMAP_LAYOUT@:

‎include/runtime/header.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -353,6 +353,7 @@ bool hook_STRING_eq(SortString, SortString);
353353

354354
const char *getSymbolNameForTag(uint32_t tag);
355355
const char *getReturnSortForTag(uint32_t tag);
356+
const char **getArgumentSortsForTag(uint32_t tag);
356357
const char *topSort(void);
357358

358359
typedef struct {

‎lib/codegen/EmitConfigParser.cpp

Lines changed: 28 additions & 50 deletions
Original file line numberDiff line numberDiff line change
@@ -1248,26 +1248,13 @@ static void emitInjTags(KOREDefinition *def, llvm::Module *mod) {
12481248
}
12491249
}
12501250

1251-
static void emitSortTable(KOREDefinition *definition, llvm::Module *module) {
1252-
llvm::LLVMContext &Ctx = module->getContext();
1253-
auto &syms = definition->getSymbols();
1254-
auto ty = llvm::PointerType::getUnqual(llvm::Type::getInt8PtrTy(Ctx));
1255-
auto dity = getPointerDebugType(getCharPtrDebugType(), "char *");
1256-
auto tableType = llvm::ArrayType::get(ty, syms.size());
1257-
auto table = module->getOrInsertGlobal("sort_table", tableType);
1258-
llvm::GlobalVariable *globalVar = llvm::dyn_cast<llvm::GlobalVariable>(table);
1259-
initDebugGlobal(
1260-
"sort_table",
1261-
getArrayDebugType(
1262-
dity, syms.size(), llvm::DataLayout(module).getABITypeAlign(ty)),
1263-
globalVar);
1264-
std::vector<llvm::Constant *> values;
1265-
for (auto iter = syms.begin(); iter != syms.end(); ++iter) {
1266-
auto entry = *iter;
1267-
auto symbol = entry.second;
1251+
static void emitSortTable(KOREDefinition *def, llvm::Module *mod) {
1252+
auto getter = [](KOREDefinition *definition, llvm::Module *module,
1253+
KORESymbol *symbol) -> llvm::Constant * {
1254+
auto &ctx = module->getContext();
12681255

12691256
auto subtableType = llvm::ArrayType::get(
1270-
llvm::Type::getInt8PtrTy(Ctx), symbol->getArguments().size());
1257+
llvm::Type::getInt8PtrTy(ctx), symbol->getArguments().size());
12711258
auto subtable = module->getOrInsertGlobal(
12721259
fmt::format("sorts_{}", ast_to_string(*symbol)), subtableType);
12731260
llvm::GlobalVariable *subtableVar
@@ -1277,30 +1264,35 @@ static void emitSortTable(KOREDefinition *definition, llvm::Module *module) {
12771264
getArrayDebugType(
12781265
getCharPtrDebugType(), symbol->getArguments().size(),
12791266
llvm::DataLayout(module).getABITypeAlign(
1280-
llvm::Type::getInt8PtrTy(Ctx))),
1267+
llvm::Type::getInt8PtrTy(ctx))),
12811268
subtableVar);
12821269
llvm::Constant *zero
1283-
= llvm::ConstantInt::get(llvm::Type::getInt64Ty(Ctx), 0);
1270+
= llvm::ConstantInt::get(llvm::Type::getInt64Ty(ctx), 0);
12841271
auto indices = std::vector<llvm::Constant *>{zero, zero};
1285-
values.push_back(llvm::ConstantExpr::getInBoundsGetElementPtr(
1286-
subtableType, subtableVar, indices));
12871272

12881273
std::vector<llvm::Constant *> subvalues;
12891274
for (size_t i = 0; i < symbol->getArguments().size(); ++i) {
12901275
auto arg_str = ast_to_string(*symbol->getArguments()[i]);
12911276
auto strType = llvm::ArrayType::get(
1292-
llvm::Type::getInt8Ty(Ctx), arg_str.size() + 1);
1277+
llvm::Type::getInt8Ty(ctx), arg_str.size() + 1);
12931278
auto sortName = module->getOrInsertGlobal(
12941279
fmt::format("sort_name_{}", arg_str), strType);
12951280
subvalues.push_back(llvm::ConstantExpr::getInBoundsGetElementPtr(
12961281
strType, sortName, indices));
12971282
}
12981283
subtableVar->setInitializer(
12991284
llvm::ConstantArray::get(subtableType, subvalues));
1300-
}
1301-
if (!globalVar->hasInitializer()) {
1302-
globalVar->setInitializer(llvm::ConstantArray::get(tableType, values));
1303-
}
1285+
1286+
return llvm::ConstantExpr::getInBoundsGetElementPtr(
1287+
subtableType, subtableVar, indices);
1288+
};
1289+
1290+
auto i8_ptr_ty = llvm::Type::getInt8PtrTy(mod->getContext());
1291+
auto entry_ty = llvm::PointerType::getUnqual(i8_ptr_ty);
1292+
auto debug_ty = getPointerDebugType(getCharPtrDebugType(), "char **");
1293+
1294+
emitDataTableForSymbol(
1295+
"getArgumentSortsForTag", entry_ty, debug_ty, def, mod, getter);
13041296
}
13051297

13061298
/*
@@ -1311,23 +1303,12 @@ static void emitSortTable(KOREDefinition *definition, llvm::Module *module) {
13111303
*
13121304
* Each value in the table is a pointer to a global variable containing the
13131305
* relevant sort name as a null-terminated string.
1314-
*
1315-
* The function `getReturnSortForTag` abstracts accesses to the data in this
1316-
* table.
13171306
*/
1318-
static void
1319-
emitReturnSortTable(KOREDefinition *definition, llvm::Module *module) {
1320-
auto &ctx = module->getContext();
1307+
static void emitReturnSortTable(KOREDefinition *def, llvm::Module *mod) {
1308+
auto getter = [](KOREDefinition *definition, llvm::Module *module,
1309+
KORESymbol *symbol) -> llvm::Constant * {
1310+
auto &ctx = module->getContext();
13211311

1322-
auto const &syms = definition->getSymbols();
1323-
1324-
auto element_type = llvm::Type::getInt8PtrTy(ctx);
1325-
auto table_type = llvm::ArrayType::get(element_type, syms.size());
1326-
1327-
auto table = module->getOrInsertGlobal("return_sort_table", table_type);
1328-
auto values = std::vector<llvm::Constant *>{};
1329-
1330-
for (auto [tag, symbol] : syms) {
13311312
auto sort = symbol->getSort();
13321313
auto sort_str = ast_to_string(*sort);
13331314

@@ -1340,16 +1321,13 @@ emitReturnSortTable(KOREDefinition *definition, llvm::Module *module) {
13401321
auto i64_type = llvm::Type::getInt64Ty(ctx);
13411322
auto zero = llvm::ConstantInt::get(i64_type, 0);
13421323

1343-
auto pointer = llvm::ConstantExpr::getInBoundsGetElementPtr(
1324+
return llvm::ConstantExpr::getInBoundsGetElementPtr(
13441325
str_type, sort_name, std::vector<llvm::Constant *>{zero});
1326+
};
13451327

1346-
values.push_back(pointer);
1347-
}
1348-
1349-
auto global = llvm::dyn_cast<llvm::GlobalVariable>(table);
1350-
if (!global->hasInitializer()) {
1351-
global->setInitializer(llvm::ConstantArray::get(table_type, values));
1352-
}
1328+
emitDataTableForSymbol(
1329+
"getReturnSortForTag", llvm::Type::getInt8PtrTy(mod->getContext()),
1330+
getCharPtrDebugType(), def, mod, getter);
13531331
}
13541332

13551333
void emitConfigParserFunctions(

‎runtime/collections/lists.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -246,6 +246,9 @@ void printList(
246246
return;
247247
}
248248

249+
auto tag = getTagForSymbolName(element);
250+
auto arg_sorts = getArgumentSortsForTag(tag);
251+
249252
sfprintf(file, "\\left-assoc{}(%s(", concat);
250253

251254
bool once = true;
@@ -256,7 +259,7 @@ void printList(
256259
sfprintf(file, ",");
257260
}
258261
sfprintf(file, "%s(", element);
259-
printConfigurationInternal(file, *iter, "SortKItem{}", false, state);
262+
printConfigurationInternal(file, *iter, arg_sorts[0], false, state);
260263
sfprintf(file, ")");
261264
}
262265
sfprintf(file, "))");

‎runtime/collections/maps.cpp

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -200,6 +200,9 @@ void printMap(
200200
return;
201201
}
202202

203+
auto tag = getTagForSymbolName(element);
204+
auto arg_sorts = getArgumentSortsForTag(tag);
205+
203206
sfprintf(file, "\\left-assoc{}(%s(", concat);
204207

205208
bool once = true;
@@ -212,9 +215,9 @@ void printMap(
212215

213216
sfprintf(file, "%s(", element);
214217
auto entry = *iter;
215-
printConfigurationInternal(file, entry.first, "SortKItem{}", false, state);
218+
printConfigurationInternal(file, entry.first, arg_sorts[0], false, state);
216219
sfprintf(file, ",");
217-
printConfigurationInternal(file, entry.second, "SortKItem{}", false, state);
220+
printConfigurationInternal(file, entry.second, arg_sorts[1], false, state);
218221
sfprintf(file, ")");
219222
}
220223
sfprintf(file, "))");

‎runtime/collections/rangemaps.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -265,6 +265,9 @@ void printRangeMap(
265265
return;
266266
}
267267

268+
auto tag = getTagForSymbolName(element);
269+
auto arg_sorts = getArgumentSortsForTag(tag);
270+
268271
sfprintf(file, "\\left-assoc{}(%s(", concat);
269272

270273
bool once = true;
@@ -285,7 +288,7 @@ void printRangeMap(
285288
printConfigurationInternal(
286289
file, entry.first.end(), "SortKItem{}", false, state);
287290
sfprintf(file, "),");
288-
printConfigurationInternal(file, entry.second, "SortKItem{}", false, state);
291+
printConfigurationInternal(file, entry.second, arg_sorts[1], false, state);
289292
sfprintf(file, ")");
290293
}
291294
sfprintf(file, "))");

‎runtime/collections/sets.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -146,6 +146,9 @@ void printSet(
146146
return;
147147
}
148148

149+
auto tag = getTagForSymbolName(element);
150+
auto arg_sorts = getArgumentSortsForTag(tag);
151+
149152
sfprintf(file, "\\left-assoc{}(%s(", concat);
150153

151154
bool once = true;
@@ -157,7 +160,7 @@ void printSet(
157160
}
158161

159162
sfprintf(file, "%s(", element);
160-
printConfigurationInternal(file, *iter, "SortKItem{}", false, state);
163+
printConfigurationInternal(file, *iter, arg_sorts[0], false, state);
161164
sfprintf(file, ")");
162165
}
163166
sfprintf(file, "))");

‎runtime/util/ConfigurationSerializer.cpp

Lines changed: 17 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -114,11 +114,14 @@ void serializeMap(
114114
return;
115115
}
116116

117+
auto tag = getTagForSymbolName(element);
118+
auto arg_sorts = getArgumentSortsForTag(tag);
119+
117120
for (auto iter = map->begin(); iter != map->end(); ++iter) {
118121
serializeConfigurationInternal(
119-
file, iter->first, "SortKItem{}", false, state);
122+
file, iter->first, arg_sorts[0], false, state);
120123
serializeConfigurationInternal(
121-
file, iter->second, "SortKItem{}", false, state);
124+
file, iter->second, arg_sorts[1], false, state);
122125
emitSymbol(instance, element, 2);
123126

124127
if (iter != map->begin()) {
@@ -138,6 +141,9 @@ void serializeRangeMap(
138141
return;
139142
}
140143

144+
auto tag = getTagForSymbolName(element);
145+
auto arg_sorts = getArgumentSortsForTag(tag);
146+
141147
bool once = true;
142148
for (auto iter = rng_map::ConstRangeMapIterator<KElem, KElem>(*map);
143149
iter.has_next(); ++iter) {
@@ -147,7 +153,7 @@ void serializeRangeMap(
147153
file, iter->first.end(), "SortKItem{}", false, state);
148154
emitSymbol(instance, "LblRangemap'Coln'Range{}", 2);
149155
serializeConfigurationInternal(
150-
file, iter->second, "SortKItem{}", false, state);
156+
file, iter->second, arg_sorts[1], false, state);
151157
emitSymbol(instance, element, 2);
152158

153159
if (once) {
@@ -169,8 +175,11 @@ void serializeList(
169175
return;
170176
}
171177

178+
auto tag = getTagForSymbolName(element);
179+
auto arg_sorts = getArgumentSortsForTag(tag);
180+
172181
for (auto iter = list->begin(); iter != list->end(); ++iter) {
173-
serializeConfigurationInternal(file, *iter, "SortKItem{}", false, state);
182+
serializeConfigurationInternal(file, *iter, arg_sorts[0], false, state);
174183
emitSymbol(instance, element, 1);
175184

176185
if (iter != list->begin()) {
@@ -190,8 +199,11 @@ void serializeSet(
190199
return;
191200
}
192201

202+
auto tag = getTagForSymbolName(element);
203+
auto arg_sorts = getArgumentSortsForTag(tag);
204+
193205
for (auto iter = set->begin(); iter != set->end(); ++iter) {
194-
serializeConfigurationInternal(file, *iter, "SortKItem{}", false, state);
206+
serializeConfigurationInternal(file, *iter, arg_sorts[0], false, state);
195207
emitSymbol(instance, element, 1);
196208

197209
if (iter != set->begin()) {

‎runtime/util/util.cpp

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,6 @@
22

33
extern "C" {
44

5-
extern char *return_sort_table;
6-
7-
const char *getReturnSortForTag(uint32_t tag) {
8-
return (&return_sort_table)[tag];
9-
}
10-
115
block *dot_k() {
126
return leaf_block(getTagForSymbolName("dotk{}"));
137
}

‎test/defn/k-files/wasm-maps.k

Lines changed: 85 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,85 @@
1+
module WASM-MAPS
2+
imports MAP-INT-TO-VAL
3+
// imports MAP-INT-TO-INT
4+
5+
configuration
6+
<wasm>
7+
<instrs> $PGM </instrs>
8+
<locals> .MapIntToVal </locals>
9+
// <locals> .MapIntToInt </locals>
10+
</wasm>
11+
12+
syntax Instr ::= "init_local" Int Int
13+
// -----------------------------------
14+
rule <instrs> init_local INDEX VALUE => . ... </instrs>
15+
<locals> LOCALS => LOCALS {{ INDEX <- wrap(VALUE) }} </locals>
16+
17+
endmodule
18+
19+
module MAP-INT-TO-INT
20+
imports WRAPPED-INT
21+
22+
syntax MapIntToInt [hook(MAP.Map)]
23+
syntax MapIntToInt ::= MapIntToInt MapIntToInt
24+
[ left, function, hook(MAP.concat), klabel(_MapIntToInt_),
25+
symbol, assoc, comm, unit(.MapIntToInt), element(_Int2Int|->_)
26+
]
27+
syntax MapIntToInt ::= ".MapIntToInt"
28+
[function, total, hook(MAP.unit),klabel(.MapIntToInt), symbol]
29+
syntax MapIntToInt ::= WrappedInt "Int2Int|->" WrappedInt
30+
[function, total, hook(MAP.element), klabel(_Int2Int|->_), symbol]
31+
32+
syntax MapIntToInt ::= MapIntToInt "[" key: WrappedInt "<-" value: WrappedInt "]" [function, total, klabel(MapInt2Int:update), symbol, hook(MAP.update), prefer]
33+
34+
syntax priorities _Int2Int|->_ > _MapIntToInt_ .MapIntToInt
35+
syntax non-assoc _Int2Int|->_
36+
37+
syntax MapIntToInt ::= MapIntToInt "{{" key: Int "<-" value: Int "}}"
38+
[ function, total, klabel(MapIntToInt:primitiveUpdate), symbol,
39+
prefer
40+
]
41+
rule M:MapIntToInt {{ Key:Int <- Value:Int }}
42+
=> M[wrap(Key) <- wrap(Value)]
43+
44+
endmodule
45+
46+
module MAP-INT-TO-VAL
47+
imports WRAPPED-INT
48+
49+
syntax Val ::= WrappedInt
50+
// -----------------------
51+
52+
syntax MapIntToVal [hook(MAP.Map)]
53+
syntax MapIntToVal ::= MapIntToVal MapIntToVal
54+
[ left, function, hook(MAP.concat), klabel(_MapIntToVal_),
55+
symbol, assoc, comm, unit(.MapIntToVal), element(_Int2Val|->_)
56+
]
57+
syntax MapIntToVal ::= ".MapIntToVal"
58+
[function, total, hook(MAP.unit),klabel(.MapIntToVal), symbol]
59+
syntax MapIntToVal ::= WrappedInt "Int2Val|->" Val
60+
[function, total, hook(MAP.element), klabel(_Int2Val|->_), symbol]
61+
62+
syntax MapIntToVal ::= MapIntToVal "[" key: WrappedInt "<-" value: Val "]" [function, total, klabel(MapInt2Val:update), symbol, hook(MAP.update), prefer]
63+
64+
syntax priorities _Int2Val|->_ > _MapIntToVal_ .MapIntToVal
65+
syntax non-assoc _Int2Val|->_
66+
67+
syntax MapIntToVal ::= MapIntToVal "{{" key: Int "<-" value: Val "}}"
68+
[ function, total, klabel(MapIntToVal:primitiveUpdate), symbol,
69+
prefer
70+
]
71+
rule M:MapIntToVal {{ Key:Int <- Value:Val }}
72+
=> M[wrap(Key) <- Value]
73+
74+
endmodule
75+
76+
module WRAPPED-INT
77+
imports INT
78+
79+
syntax WrappedInt ::= wrap(Int) [symbol, klabel(wrapInt)]
80+
// -------------------------------------------------------
81+
82+
syntax Int ::= unwrap(WrappedInt) [function, total, injective, symbol, klabel(unwrapInt)]
83+
// ---------------------------------------------------------------------------------------
84+
rule unwrap(wrap(A:Int)) => A
85+
endmodule

0 commit comments

Comments
 (0)