From 90819bf86b41f850542c0dae797b0e2e72e90025 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Mon, 13 Nov 2023 08:24:23 +0100 Subject: [PATCH] Simplified LLVM grammar (combined globalDecl and globalDef) (#567) Added support for parsing external globals (as non-dets). Added support for referencing other globals in initializers (first we parse the declarations and then the initializers). --- dartagnan/src/main/antlr4/LLVMIR.g4 | 10 +-- .../parsers/program/visitors/VisitorLlvm.java | 82 +++++++++++++------ 2 files changed, 59 insertions(+), 33 deletions(-) diff --git a/dartagnan/src/main/antlr4/LLVMIR.g4 b/dartagnan/src/main/antlr4/LLVMIR.g4 index bce2f1f0d8..1ef44da4d1 100644 --- a/dartagnan/src/main/antlr4/LLVMIR.g4 +++ b/dartagnan/src/main/antlr4/LLVMIR.g4 @@ -33,7 +33,6 @@ topLevelEntity: | moduleAsm | typeDef | comdatDef - | globalDecl | globalDef | indirectSymbolDef | funcDecl @@ -53,14 +52,9 @@ comdatDef: | 'nodeduplicate' | 'samesize' ); -globalDecl: - GlobalIdent '=' externalLinkage preemption? visibility? dllStorageClass? threadLocal? - unnamedAddr? addrSpace? externallyInitialized? immutable type ( - ',' globalField - )* (',' metadataAttachment)* funcAttribute*; globalDef: - GlobalIdent '=' internalLinkage? preemption? visibility? dllStorageClass? threadLocal? - unnamedAddr? addrSpace? externallyInitialized? immutable type constant ( + GlobalIdent '=' (externalLinkage | internalLinkage)? preemption? visibility? dllStorageClass? threadLocal? + unnamedAddr? addrSpace? externallyInitialized? immutable type constant? ( ',' globalField )* (',' metadataAttachment)* funcAttribute*; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java index ef595a647c..21447fd6f0 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java @@ -73,11 +73,15 @@ public Program buildProgram() { @Override public Expression visitCompilationUnit(CompilationUnitContext ctx) { - // Create the metadata mapping beforehand, so that instructions can get all attachments + // Create the metadata mapping beforehand, so that instructions can get all attachments. + // Also parse all type definitions. for (final TopLevelEntityContext entity : ctx.topLevelEntity()) { if (entity.metadataDef() != null) { entity.accept(this); } + if (entity.typeDef() != null) { + entity.accept(this); + } } // Declare all globals (functions and variables). @@ -88,12 +92,14 @@ public Expression visitCompilationUnit(CompilationUnitContext ctx) { if (entity.funcDef() != null) { visitFuncHeader(entity.funcDef().funcHeader()); } - // FIXME: Declare global variables + if (entity.globalDef() != null) { + visitGlobalDeclaration(entity.globalDef()); + } } + + // Parse global definitions after declarations. for (final TopLevelEntityContext entity : ctx.topLevelEntity()) { - //FIXME: We need to parse the declaration of globals (similar to func headers) first - // because the initializer may refer to other globals. - if (entity.globalDecl() != null || entity.globalDef() != null || entity.typeDef() != null) { + if (entity.globalDef() != null) { entity.accept(this); } } @@ -101,7 +107,6 @@ public Expression visitCompilationUnit(CompilationUnitContext ctx) { // Parse definitions for (final TopLevelEntityContext entity : ctx.topLevelEntity()) { if (entity.metadataDef() == null && - entity.globalDecl() == null && entity.globalDef() == null && entity.typeDef() == null && entity.funcDecl() == null) { @@ -164,7 +169,7 @@ public Expression visitFuncDef(FuncDefContext ctx) { for (final BasicBlockContext basicBlockContext : ctx.funcBody().basicBlock()) { block = getBlock(basicBlockContext.LabelIdent()); final List blockHeaderMetadata; - if (basicBlockContext.instruction().size() > 0) { + if (!basicBlockContext.instruction().isEmpty()) { blockHeaderMetadata = parseMetadataAttachment(basicBlockContext.instruction(0).metadataAttachment()); } else { blockHeaderMetadata = parseMetadataAttachment(basicBlockContext.terminator().metadataAttachment()); @@ -232,31 +237,32 @@ private Block getBlock(TerminalNode node) { return getBlock(labelName); } - @Override - public Expression visitGlobalDecl(GlobalDeclContext ctx) { - checkSupport(false, "Declared but undefined constants are not supported", ctx); - // FIXME: See on how to handle this - return null; - } - - @Override - public Expression visitGlobalDef(GlobalDefContext ctx) { + public void visitGlobalDeclaration(GlobalDefContext ctx) { final String name = globalIdent(ctx.GlobalIdent()); - check(!constantMap.containsKey(name), "Redefined constant in %s.", ctx); - final Type type = parseType(ctx.type()); - final int size = types.getMemorySizeInBytes(type); + check(!constantMap.containsKey(name), "Redeclared constant in %s.", ctx); + final int size = types.getMemorySizeInBytes(parseType(ctx.type())); final MemoryObject globalObject = program.getMemory().allocate(size, true); globalObject.setCVar(name); if (ctx.threadLocal() != null) { globalObject.setIsThreadLocal(true); } - - //TODO: Merge GlobalDef/GlobalDecl in the LLVM grammar into one single rule with an optional "constant". - // If no constant is provided, we can generate a nondeterministic value - final Expression value = checkExpression(type, ctx.constant()); - setInitialMemoryFromConstant(globalObject, 0, value); // TODO: mark the global as constant, if possible. constantMap.put(name, globalObject); + } + + @Override + public Expression visitGlobalDef(GlobalDefContext ctx) { + final String name = globalIdent(ctx.GlobalIdent()); + final MemoryObject globalObject = (MemoryObject) constantMap.get(name); + final Type type = parseType(ctx.type()); + final boolean isExternal = ctx.externalLinkage() != null; + final boolean hasInitializer = ctx.constant() != null; + + check (!(isExternal && hasInitializer), "External global cannot have initializer: %s", ctx); + check (isExternal || hasInitializer, "Global without initializer; %s", ctx); + + final Expression value = hasInitializer ? checkExpression(type, ctx.constant()) : makeNonDetOfType(type); + setInitialMemoryFromConstant(globalObject, 0, value); return null; } @@ -295,7 +301,7 @@ private Block getBlock(String label) { } private List parseMetadataAttachment(List metadataAttachmentContexts) { - if (metadataAttachmentContexts.size() == 0) { + if (metadataAttachmentContexts.isEmpty()) { return List.of(); } @@ -1279,6 +1285,32 @@ public Expression visitFilenameField(FilenameFieldContext ctx) { // ---------------------------------------------------------------------------------------------------------------- // Helpers + public Expression makeNonDetOfType(Type type) { + if (type instanceof ArrayType arrayType) { + final List entries = new ArrayList<>(arrayType.getNumElements()); + for (int i = 0; i < arrayType.getNumElements(); i++) { + entries.add(makeNonDetOfType(arrayType.getElementType())); + } + return expressions.makeArray(arrayType.getElementType(), entries, true); + } else if (type instanceof AggregateType structType) { + final List elements = new ArrayList<>(structType.getDirectFields().size()); + for (Type fieldType : structType.getDirectFields()) { + elements.add(makeNonDetOfType(fieldType)); + } + return expressions.makeConstruct(elements); + } else if (type instanceof IntegerType intType) { + final INonDet value = new INonDet(program.getConstants().size(), intType, true); + value.setMin(intType.getMinimumValue(true)); + value.setMax(intType.getMaximumValue(true)); + program.addConstant(value); + return value; + } else if (type instanceof BooleanType) { + return new BNonDet(types.getBooleanType()); + } else { + throw new UnsupportedOperationException("Cannot create non-deterministic value of type " + type); + } + } + private void check(boolean condition, String message, ParserRuleContext context) { if (!condition) { throw new ParsingException(String.format(message, context.getText()));