Ported FrontendXcfaBuilder

ftsrg · Jul 21, 2022 · 73fdca0 · 73fdca0
1 parent 40301b6
commit 73fdca0
Show file tree

Hide file tree

Showing 13 changed files with 1,160 additions and 14 deletions.
diff --git a/settings.gradle.kts b/settings.gradle.kts
@@ -17,6 +17,8 @@ include(
         "sts/sts-cli",
 
         "xcfa/xcfa",
+        "xcfa/c2xcfa",
+
         "xcfa-old/xcfa-analysis",
         "xcfa-old/xcfa-cli",
         "xcfa-old/cat",

diff --git a/...ds/litmus2xcfa/src/main/java/hu/bme/mit/theta/frontend/litmus2xcfa/dsl/LitmusAArch64.java b/...ds/litmus2xcfa/src/main/java/hu/bme/mit/theta/frontend/litmus2xcfa/dsl/LitmusAArch64.java
@@ -92,7 +92,7 @@ else if(regDeclCtx != null && regDeclCtx.Amp() == null) {
             locations.putIfAbsent(id, new LinkedHashMap<>());
             final XcfaProcess.Builder process = XcfaProcess.builder();
             final XcfaProcedure.Builder procedure = XcfaProcedure.builder();
-            final XcfaLocation location = XcfaLocation.create("initial" + XcfaLocation.uniqeCounter());
+            final XcfaLocation location = XcfaLocation.create("initial" + XcfaLocation.uniqueCounter());
             procedure.addLoc(location);
             process.addProcedure(procedure);
             process.setMainProcedure(procedure);
@@ -143,7 +143,7 @@ private VarDecl<BvType> getGlobalFromReg(final String name) {
     }
 
     private XcfaLocation newAnonymousLoc() {
-        return getOrCreateLoc("loc" + XcfaLocation.uniqeCounter());
+        return getOrCreateLoc("loc" + XcfaLocation.uniqueCounter());
     }
 
     private XcfaLocation getOrCreateLoc(final String name) {
@@ -234,7 +234,7 @@ public XcfaLabel visitArith64(LitmusAArch64Parser.Arith64Context ctx) {
         @Override
         public XcfaLabel visitLoad32(LitmusAArch64Parser.Load32Context ctx) {
             final VarDecl<BvType> var = getOrCreateVar(ctx.rD32.getText(), 32);
-            final VarDecl<BvType> tmp = getOrCreateVar("tmp" + XcfaLocation.uniqeCounter(), 64);
+            final VarDecl<BvType> tmp = getOrCreateVar("tmp" + XcfaLocation.uniqueCounter(), 64);
             StmtXcfaLabel cast = Stmt(Assign(var, Extract(tmp.getRef(), Int(0), Int(32))));
             LoadXcfaLabel<BvType> load = Load(getGlobalFromReg(ctx.address().r.getText()), tmp, true, ctx.loadInstruction().mo);
             return Sequence(List.of(load, cast));
@@ -248,7 +248,7 @@ public XcfaLabel visitLoad64(LitmusAArch64Parser.Load64Context ctx) {
         @Override
         public XcfaLabel visitStore32(LitmusAArch64Parser.Store32Context ctx) {
             final VarDecl<BvType> var = getOrCreateVar(ctx.rV32.getText(), 32);
-            final VarDecl<BvType> tmp = getOrCreateVar("tmp" + XcfaLocation.uniqeCounter(), 64);
+            final VarDecl<BvType> tmp = getOrCreateVar("tmp" + XcfaLocation.uniqueCounter(), 64);
             StmtXcfaLabel cast = Stmt(Assign(tmp, ZExt(var.getRef(), BvType(64))));
             StoreXcfaLabel<BvType> store = Store(getGlobalFromReg(ctx.address().r.getText()), tmp, true, ctx.storeInstruction().mo);
             return Sequence(List.of(cast, store));

diff --git a/subprojects/xcfa-old/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaLocation.java b/subprojects/xcfa-old/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaLocation.java
@@ -53,12 +53,12 @@ public static XcfaLocation create(final String name) {
 
 	private static int counter = 0;
 
-	public static int uniqeCounter() {
+	public static int uniqueCounter() {
 		return counter++;
 	}
 
 	public static XcfaLocation uniqeCopyOf(final XcfaLocation from) {
-		XcfaLocation xcfaLocation = create(from.getName() + uniqeCounter());
+		XcfaLocation xcfaLocation = create(from.getName() + uniqueCounter());
 		FrontendMetadata.lookupMetadata(from).forEach((s, o) -> {
 			FrontendMetadata.create(xcfaLocation, s, o);
 		});

diff --git a/...ts/xcfa-old/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/utils/FrontendXcfaBuilder.java b/...ts/xcfa-old/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/utils/FrontendXcfaBuilder.java
@@ -103,7 +103,7 @@ private XcfaLocation getLoc(final XcfaProcedure.Builder builder, final String na
 	}
 
 	private XcfaLocation getAnonymousLoc(final XcfaProcedure.Builder builder) {
-		return getLoc(builder, "__loc_" + XcfaLocation.uniqeCounter());
+		return getLoc(builder, "__loc_" + XcfaLocation.uniqueCounter());
 	}
 
 	protected <T> void propagateMetadata(CStatement source, T newOwner) {
@@ -327,7 +327,7 @@ public XcfaLocation visit(CBreak statement, ParamPack param) {
 		builder.addEdge(edge);
 		propagateMetadata(statement, edge);
 		edge = XcfaEdge.of(initLoc, breakLoc, List.of());
-		XcfaLocation unreachableLoc = XcfaLocation.create("Unreachable" + XcfaLocation.uniqeCounter());
+		XcfaLocation unreachableLoc = XcfaLocation.create("Unreachable" + XcfaLocation.uniqueCounter());
 		builder.addLoc(unreachableLoc);
 		propagateMetadata(statement, unreachableLoc);
 		builder.addEdge(edge);
@@ -425,7 +425,7 @@ public XcfaLocation visit(CContinue statement, ParamPack param) {
 		builder.addEdge(edge);
 		propagateMetadata(statement, edge);
 		edge = XcfaEdge.of(initLoc, continueLoc, List.of());
-		XcfaLocation unreachableLoc = XcfaLocation.create("Unreachable" + XcfaLocation.uniqeCounter());
+		XcfaLocation unreachableLoc = XcfaLocation.create("Unreachable" + XcfaLocation.uniqueCounter());
 		builder.addLoc(unreachableLoc);
 		propagateMetadata(statement, unreachableLoc);
 		builder.addEdge(edge);
@@ -591,7 +591,7 @@ public XcfaLocation visit(CGoto statement, ParamPack param) {
 		propagateMetadata(statement, edge);
 		edge = XcfaEdge.of(initLoc, getLoc(builder, statement.getLabel()), List.of());
 		builder.addLoc(getLoc(builder, statement.getLabel()));
-		XcfaLocation unreachableLoc = XcfaLocation.create("Unreachable" + XcfaLocation.uniqeCounter());
+		XcfaLocation unreachableLoc = XcfaLocation.create("Unreachable" + XcfaLocation.uniqueCounter());
 		builder.addLoc(unreachableLoc);
 		propagateMetadata(statement, unreachableLoc);
 		builder.addEdge(edge);

diff --git a/...jects/xcfa-old/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/PorPass.java b/...jects/xcfa-old/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/PorPass.java
@@ -41,13 +41,13 @@ public XcfaProcedure.Builder run(XcfaProcedure.Builder builder) {
 						removed = true;
 					}
 					if (newLabels.size() > 0) {
-						XcfaLocation tmp = XcfaLocation.create("tmp" + XcfaLocation.uniqeCounter());
+						XcfaLocation tmp = XcfaLocation.create("tmp" + XcfaLocation.uniqueCounter());
 						builder.addLoc(tmp);
 						builder.addEdge(edge.withSource(source).withLabels(newLabels).withTarget(tmp));
 						source = tmp;
 						newLabels.clear();
 					}
-					XcfaLocation tmp = XcfaLocation.create("tmp" + XcfaLocation.uniqeCounter());
+					XcfaLocation tmp = XcfaLocation.create("tmp" + XcfaLocation.uniqueCounter());
 					builder.addLoc(tmp);
 					builder.addEdge(edge.withSource(source).withLabels(List.of(label)).withTarget(tmp));
 					source = tmp;

diff --git a/...cfa-old/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/processpass/FunctionInlining.java b/...cfa-old/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/processpass/FunctionInlining.java
@@ -169,7 +169,7 @@ private void splitAndInlineEdges(XcfaProcess.Builder oldBuilder, XcfaProcedure.B
 			XcfaLocation start = xcfaEdge.getSource();
 			XcfaLocation end = xcfaEdge.getTarget();
 			if (i > 0) {
-				XcfaLocation loc1 = XcfaLocation.create("inline" + XcfaLocation.uniqeCounter());
+				XcfaLocation loc1 = XcfaLocation.create("inline" + XcfaLocation.uniqueCounter());
 				FrontendMetadata.lookupMetadata(xcfaEdge).forEach((s, o) -> {
 					FrontendMetadata.create(loc1, s, o);
 				});
@@ -182,7 +182,7 @@ private void splitAndInlineEdges(XcfaProcess.Builder oldBuilder, XcfaProcedure.B
 				start = loc1;
 			}
 			if (i < xcfaEdge.getLabels().size() - 1) {
-				XcfaLocation loc1 = XcfaLocation.create("inline" + XcfaLocation.uniqeCounter());
+				XcfaLocation loc1 = XcfaLocation.create("inline" + XcfaLocation.uniqueCounter());
 				FrontendMetadata.lookupMetadata(xcfaEdge).forEach((s, o) -> {
 					FrontendMetadata.create(loc1, s, o);
 				});

diff --git a/subprojects/xcfa/c2xcfa/build.gradle.kts b/subprojects/xcfa/c2xcfa/build.gradle.kts
@@ -0,0 +1,10 @@
+plugins {
+    id("kotlin-common")
+}
+
+dependencies {
+    implementation(project(":theta-common"))
+    implementation(project(":theta-core"))
+    implementation(project(":theta-xcfa"))
+    implementation(project(":theta-c-frontend"))
+}