Merge pull request #171 from s0mark/function

Basic function support

build.gradle.kts

@@ -11,7 +11,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.inf.theta"
-    version = "4.1.0"
+    version = "4.2.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

doc/Build.md

@@ -2,8 +2,8 @@
 
 Theta uses Java (JDK) 17 with [Gradle 7.4](https://gradle.org/) as a build system.
 Currently, we use [OpenJDK 17](https://openjdk.java.net/projects/jdk/17/) (see instructions for [Windows](https://java.tutorials24x7.com/blog/how-to-install-openjdk-17-on-windows) and [Ubuntu](https://www.linuxuprising.com/2019/04/install-latest-openjdk-12-11-or-8-in.html)).
-We are developing Theta both on Linux and Windows.
-Currently, floating point types are only fully supported on Linux. Windows support is experimental and can cause cryptic exceptions to occur in native code. 
+We are developing Theta on Linux, Windows and MacOS _(10.15.7)_.
+Currently, floating point types are only fully supported on Linux and MacOS. Windows support is experimental and can cause cryptic exceptions to occur in native code. 
 Theta can be built from the command line, but you can also import it into [IntelliJ IDEA](https://www.jetbrains.com/idea/).
 Unfortunately, Eclipse [does not support](https://github.com/eclipse/buildship/issues/222) Gradle projects with Kotlin build scripts (yet).
 
@@ -12,15 +12,19 @@ Unfortunately, Eclipse [does not support](https://github.com/eclipse/buildship/i
 Theta has some external dependencies that may need to be obtained/installed depending on what parts of the framework you are working with.
 
 **Z3 SMT Solver:**
-The libraries for the Z3 solver (version 4.5.0) are included in the _lib_ directory, both for Windows and Ubuntu (64 bit).
+The libraries for the Z3 solver (version 4.5.0) are included in the _lib_ directory, for Windows, Ubuntu (64 bit) and MacOS.
 However, on Windows, _libz3.dll_ also requires some libraries from the [Microsoft Visual C++ Redistributable package](https://www.microsoft.com/en-us/download/details.aspx?id=48145) that we could not include due to licensing.
 Install it, or just execute `Download-VCredist.ps1`, which will download the required libraries.
+On MacOS, _libz3.dylib_ and _libz3java.dylib_ need to be on `DYLD_LIBRARY_PATH`.
 If you have a different OS, you should download the appropriate [Z3 binary for version 4.5.0](https://github.com/Z3Prover/z3/releases/tag/z3-4.5.0).
 These libraries should be available on `PATH` for the executable tools.
 
 *Troubleshooting*:
 * If Z3 gives an assertion error (unreachable code reached), your Z3 version may not be correct.
 
+**MPFR:**
+For floating point support on MacOS, _libmpfr_java-1.4.jnilib_ and _libmpfr.dylib_ (as _libmpfr.4.dylib_) need to be on `DYLD_LIBRARY_PATH`. Additionally, _libmpfr_java-1.4.jnilib_ needs to linked as _libmpfr_java.jnilib_ onto both `DYLD_LIBRARY_PATH` and `java.library.path`.
+
 **GraphViz:**
 Theta can export graphs in _dot_ format and automatically convert them to images.
 For this, [GraphViz](http://www.graphviz.org/) has to be installed and _dot_ (or _dot.exe_ on Windows) has to be on the `PATH`.

subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3SolverFactory.java

@@ -45,6 +45,7 @@ private static void loadLibraries() {
 				System.loadLibrary("libz3java");
 				break;
 			case LINUX:
+			case MAC:
 				System.loadLibrary("z3java");
 				break;
 			default:

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/impl/singlethread/XcfaSTAction.java

@@ -16,12 +16,16 @@
 package hu.bme.mit.theta.xcfa.analysis.impl.singlethread;
 
 import hu.bme.mit.theta.common.Utils;
+import hu.bme.mit.theta.core.decl.VarDecl;
 import hu.bme.mit.theta.core.stmt.Stmt;
+import hu.bme.mit.theta.frontend.FrontendMetadata;
 import hu.bme.mit.theta.xcfa.model.XcfaEdge;
 import hu.bme.mit.theta.xcfa.model.XcfaLabel;
 import hu.bme.mit.theta.xcfa.model.XcfaLocation;
+import hu.bme.mit.theta.xcfa.model.utils.XcfaLabelVarReplacer;
 
 import java.util.List;
+import java.util.Map;
 import java.util.Objects;
 import java.util.stream.Collectors;
 
@@ -44,6 +48,10 @@ public static XcfaSTAction create(final XcfaEdge edge) {
 		return new XcfaSTAction(edge.getSource(), edge.getTarget(), edge.getLabels());
 	}
 
+	public static XcfaSTAction createWithVars(final XcfaEdge edge, Map<VarDecl<?>, VarDecl<?>> newVarLut) {
+		return new XcfaSTAction(edge.getSource(), edge.getTarget(), XcfaLabelVarReplacer.replaceVars(edge.getLabels(), newVarLut));
+	}
+
 	public XcfaLocation getSource() {
 		return source;
 	}
@@ -70,6 +78,13 @@ public XcfaSTAction withLabels(final List<XcfaLabel> stmts) {
 		return new XcfaSTAction(source, target, stmts);
 	}
 
+	public static XcfaSTAction copyOf(XcfaSTAction action, Map<VarDecl<?>, VarDecl<?>> newVarLut) {
+		List<XcfaLabel> newStmts = XcfaLabelVarReplacer.replaceVars(action.getLabels(), newVarLut);
+		XcfaSTAction xcfaSTAction = new XcfaSTAction(action.source, action.target, newStmts);
+		FrontendMetadata.lookupMetadata(action).forEach((s, o) -> FrontendMetadata.create(xcfaSTAction, s, o));
+		return xcfaSTAction;
+	}
+
 	@Override
 	public boolean equals(Object o) {
 		if (this == o) return true;

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/impl/singlethread/XcfaSTLts.java

@@ -19,6 +19,7 @@
 import hu.bme.mit.theta.analysis.LTS;
 import hu.bme.mit.theta.xcfa.model.XcfaEdge;
 import hu.bme.mit.theta.xcfa.model.XcfaLocation;
+import hu.bme.mit.theta.xcfa.passes.processpass.FunctionInlining;
 
 import java.util.ArrayList;
 import java.util.Collection;
@@ -29,7 +30,9 @@ public Collection<XcfaSTAction> getEnabledActionsFor(final XcfaSTState<?> state)
 		final Collection<XcfaSTAction> xcfaActions = new ArrayList<>();
 		final XcfaLocation loc = state.getCurrentLoc();
 		for (XcfaEdge outgoingEdge : loc.getOutgoingEdges()) {
-			final XcfaSTAction xcfaAction = XcfaSTAction.create(outgoingEdge);
+			final XcfaSTAction xcfaAction = FunctionInlining.inlining == FunctionInlining.InlineFunctions.ON ?
+					XcfaSTAction.create(outgoingEdge) :
+					XcfaSTAction.createWithVars(outgoingEdge, ((XcfaSTStateStack<?>) state).getCurrentVars());
 			xcfaActions.add(xcfaAction);
 		}
 		return xcfaActions;

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/impl/singlethread/XcfaSTOrd.java

@@ -31,12 +31,12 @@ private XcfaSTOrd(final PartialOrd<S> partialOrd) {
 	}
 
 	public static <S extends ExprState> XcfaSTOrd<S> create(final PartialOrd<S> partialOrd) {
-		return new XcfaSTOrd<S>(partialOrd);
+		return new XcfaSTOrd<>(partialOrd);
 	}
 
 	@Override
 	public boolean isLeq(final XcfaState<S> state1, final XcfaState<S> state2) {
-		return state1.getCurrentLoc().equals(state2.getCurrentLoc()) &&
-				partialOrd.isLeq(state1.getGlobalState(), state2.getGlobalState());
+		return ((XcfaSTState<S>) state1).equalLocations(((XcfaSTState<S>) state2))
+				&& partialOrd.isLeq(state1.getGlobalState(), state2.getGlobalState());
 	}
 }

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/impl/singlethread/XcfaSTState.java

@@ -20,20 +20,19 @@
 import hu.bme.mit.theta.core.type.booltype.BoolType;
 import hu.bme.mit.theta.xcfa.analysis.common.XcfaState;
 import hu.bme.mit.theta.xcfa.model.XcfaLocation;
+import hu.bme.mit.theta.xcfa.passes.processpass.FunctionInlining;
 
-import java.util.Objects;
+public abstract class XcfaSTState<S extends ExprState> extends XcfaState<S> {
+	protected final S globalState;
 
-public class XcfaSTState<S extends ExprState> extends XcfaState<S> {
-	private final XcfaLocation currentLoc;
-	private final S globalState;
-
-	private XcfaSTState(final XcfaLocation currentLoc, final S globalState) {
-		this.currentLoc = currentLoc;
+	protected XcfaSTState(final S globalState) {
 		this.globalState = globalState;
 	}
 
 	public static <S extends ExprState> XcfaSTState<S> create(final XcfaLocation currentLoc, final S globalState) {
-		return new XcfaSTState<S>(currentLoc, globalState);
+		return FunctionInlining.inlining == FunctionInlining.InlineFunctions.ON ?
+				new XcfaSTStateSimple<>(currentLoc, globalState) :
+				new XcfaSTStateStack<>(currentLoc, globalState);
 	}
 
 	@Override
@@ -52,28 +51,19 @@ public S getGlobalState() {
 	}
 
 	@Override
-	public XcfaLocation getCurrentLoc() {
-		return currentLoc;
-	}
+	public abstract XcfaLocation getCurrentLoc();
 
 	@Override
 	public boolean equals(Object o) {
 		if (this == o) return true;
 		if (o == null || getClass() != o.getClass()) return false;
 		XcfaSTState<?> that = (XcfaSTState<?>) o;
-		return Objects.equals(currentLoc, that.currentLoc) && globalState.equals(that.globalState);
+		return globalState.equals(that.globalState) && equalLocations(that);
 	}
 
-	@Override
-	public int hashCode() {
-		return Objects.hash(currentLoc, globalState);
-	}
+	public abstract boolean equalLocations(XcfaSTState<?> o);
 
-	public XcfaSTState<S> withState(final S succState) {
-		return create(currentLoc, succState);
-	}
+	public abstract XcfaSTState<S> withState(final S succState);
 
-	public XcfaSTState<S> withLocation(final XcfaLocation location) {
-		return create(location, globalState);
-	}
+	public abstract XcfaSTState<S> withLocation(final XcfaLocation location);
 }

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/impl/singlethread/XcfaSTStateSimple.java

@@ -0,0 +1,57 @@
+/*
+ *  Copyright 2022 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
+package hu.bme.mit.theta.xcfa.analysis.impl.singlethread;
+
+import hu.bme.mit.theta.analysis.expr.ExprState;
+import hu.bme.mit.theta.xcfa.model.XcfaLocation;
+
+import java.util.Objects;
+
+public class XcfaSTStateSimple <S extends ExprState> extends XcfaSTState<S> {
+    private final XcfaLocation currentLocation;
+
+    protected XcfaSTStateSimple(final XcfaLocation currentLoc, final S globalState) {
+        super(globalState);
+        this.currentLocation = currentLoc;
+    }
+
+    @Override
+    public XcfaLocation getCurrentLoc() {
+        return currentLocation;
+    }
+
+    @Override
+    public boolean equalLocations(XcfaSTState<?> o) {
+        XcfaSTStateSimple<?> that = (XcfaSTStateSimple<?>) o;
+        return this.currentLocation.equals(that.currentLocation);
+    }
+
+    @Override
+    public int hashCode() {
+        return Objects.hash(currentLocation, globalState);
+    }
+
+    @Override
+    public XcfaSTState<S> withState(S succState) {
+        return new XcfaSTStateSimple<>(this.currentLocation, succState);
+    }
+
+    @Override
+    public XcfaSTState<S> withLocation(XcfaLocation location) {
+        return new XcfaSTStateSimple<>(location, this.globalState);
+    }
+}