Skip to content
Snippets Groups Projects
Commit 161812a1 authored by Cookiebowser's avatar Cookiebowser
Browse files

Implemented tests for Booleans and Integers

parent a884d3d8
No related branches found
No related tags found
No related merge requests found
package de.hhu.stups.codegenerator;
import java.io.ByteArrayOutputStream;
import java.io.IOException;
import java.io.InputStream;
import java.io.OutputStream;
import java.io.*;
import java.nio.file.Files;
import java.nio.file.Path;
import java.util.List;
......@@ -19,6 +17,10 @@ public class TestHelper {
writeInputToOutput(inputStream, System.err);
}
public static String readFile(File file) throws IOException {
return streamToString(Files.newInputStream(file.toPath()));
}
public static String streamToString(InputStream inputStream) throws IOException {
ByteArrayOutputStream result = new ByteArrayOutputStream();
byte[] buffer = new byte[1024];
......
package de.hhu.stups.codegenerator.rust_embedded;
import org.junit.Test;
import java.io.IOException;
import java.net.URISyntaxException;
public class TestBools extends TestRSE {
public TestBools() throws URISyntaxException, IOException {}
@Test
public void testAnd() throws Exception {
testRSE("And", "AndAddition.strs");
}
@Test
public void testOr() throws Exception {
testRSE("Or", "OrAddition.strs");
}
@Test
public void testImplies() throws Exception {
testRSE("Implies", "ImpliesAddition.strs");
}
@Test
public void testEquivalent() throws Exception {
testRSE("Equivalent", "EquivalentAddition.strs");
}
@Test
public void testNot() throws Exception {
testRSE("Not", "NotAddition.strs");
}
@Test
public void testEqual() throws Exception {
testRSE("Equal", "EqualAddition.strs");
}
@Test
public void testUnequal() throws Exception {
testRSE("Unequal", "UnequalAddition.strs");
}
}
package de.hhu.stups.codegenerator.rust_embedded;
import org.junit.Test;
import java.io.IOException;
import java.net.URISyntaxException;
public class TestInteger extends TestRSE {
public TestInteger() throws URISyntaxException, IOException {}
@Test
public void testGreater() throws Exception {
testRSE("Greater", "GreaterAddition.strs");
}
@Test
public void testGreaterEqual() throws Exception {
testRSE("GreaterEqual", "GreaterEqualAddition.strs");
}
@Test
public void testLess() throws Exception {
testRSE("Less", "LessAddition.strs");
}
@Test
public void testLessEqual() throws Exception {
testRSE("LessEqual", "LessEqualAddition.strs");
}
@Test
public void testPlus() throws Exception {
testRSE("Plus", "PlusAddition.strs");
}
@Test
public void testMinus() throws Exception {
testRSE("Minus", "MinusAddition.strs");
}
@Test
public void testMultiply() throws Exception {
testRSE("Multiply", "MultiplyAddition.strs");
}
@Test
public void testDivide() throws Exception {
testRSE("Divide", "DivideAddition.strs");
}
@Test
public void testPower() throws Exception {
testRSE("IntegerPower", "IntegerPowerAdditions.strs");
}
@Test
public void testModulo() throws Exception {
testRSE("Modulo", "ModuloAddition.strs");
}
@Test
public void testUnaryMinus() throws Exception {
testRSE("UnaryMinus", "UnaryMinusAddition.strs");
}
@Test
public void testPred() throws Exception {
testRSE("Pred", "PredAddition.strs");
}
@Test
public void testSucc() throws Exception {
testRSE("Succ", "SuccAddition.strs");
}
}
package de.hhu.stups.codegenerator.rust_embedded;
import de.hhu.stups.codegenerator.GeneratorMode;
import de.hhu.stups.codegenerator.TestHelper;
import org.junit.Before;
import org.junit.Test;
import java.io.File;
import java.io.FileInputStream;
import java.io.IOException;
import java.net.URI;
import java.net.URISyntaxException;
import java.net.URL;
import java.nio.file.Files;
import java.nio.file.Path;
import java.nio.file.Paths;
import java.util.Arrays;
import java.util.List;
import java.util.stream.Collectors;
import static org.junit.Assert.*;
public class TestRSE {
final ClassLoader classLoader = this.getClass().getClassLoader();
final Path tomlPath = Paths.get(classLoader.getResource("./").toURI()).getParent().getParent().getParent().getParent().resolve(Paths.get("btypes_primitives/src/main/rust_embedded/bmachine/Cargo.toml"));
final Path rustSrcPath = tomlPath.getParent().resolve(Paths.get("src/"));
final Runtime runtime = Runtime.getRuntime();
final Path testFileBasePath = Paths.get(classLoader.getResource("./").toURI()).getParent().getParent().getParent().resolve("resources/test/de/hhu/stups/codegenerator/");
public TestRSE() throws URISyntaxException, IOException {
Files.createDirectories(rustSrcPath);
}
public void cleanup() {
File[] oldFiles = rustSrcPath.toFile().listFiles();
if (oldFiles != null) Arrays.stream(oldFiles).forEach(File::delete);
}
public void generateTestFiles(String machineName, boolean modelChecking, String addition) throws IOException {
if (addition == null) addition = "DefaultAddition.strs";
cleanup();
Path machinePath = testFileBasePath.resolve(machineName + ".mch");
List<Path> rsFilePaths = TestHelper.generateCode(machinePath, GeneratorMode.RS, modelChecking, addition, true);
rsFilePaths.forEach(path -> {
Path dest = rustSrcPath.resolve(Paths.get(path.toFile().getName()));
path.toFile().renameTo(dest.toFile());
});
File mainPath = rustSrcPath.resolve(machineName + ".rs").toFile();
File newMainFile = rustSrcPath.resolve("main.rs").toFile();
mainPath.renameTo(newMainFile);
}
public void compileTestFiles() throws IOException, InterruptedException {
Process process = runtime.exec("cargo build --release --manifest-path " + tomlPath);
TestHelper.writeInputToSystem(process.getErrorStream());
TestHelper.writeInputToOutput(process.getErrorStream(), process.getOutputStream());
process.waitFor();
if (process.exitValue() != 0) {
throw new RuntimeException("cargo build failed, exitcode: " + process.exitValue());
}
}
public String runTestFiles(boolean modelChecking, boolean noDead, boolean noInv) throws IOException, InterruptedException {
String progArgs = "";
if (modelChecking) { progArgs = " -- mixed 2 true"; }
if (noDead) { progArgs += " -nodead"; }
if (noInv) { progArgs += " -noinv"; }
Process executeProcess = runtime.exec("cargo run --release --manifest-path " + tomlPath + progArgs);
executeProcess.waitFor();
String error = TestHelper.streamToString(executeProcess.getErrorStream());
if(executeProcess.exitValue() != 0) {
System.err.println("cargo run failed!");
throw new RuntimeException(error);
}
return TestHelper.streamToString(executeProcess.getInputStream());
}
public void verifyOutput(String machineName, boolean modelChecking, String actualOutput) throws IOException {
if (modelChecking && !machineName.contains("MC")) machineName += "_MC";
File outFile = testFileBasePath.resolve(machineName + ".out").toFile();
String expectedOutput = TestHelper.readFile(outFile).replaceAll("[\n\r]", "");
actualOutput = actualOutput.replaceAll("[\n\r]", "");
if (!modelChecking) {
System.out.println("Assert: " + actualOutput + " = " + expectedOutput);
assertEquals(expectedOutput, actualOutput);
} else {
System.out.println("Asserting Success: ");
System.out.println("Expected: " + expectedOutput);
System.out.println("Gotten : " + actualOutput);
assertTrue(actualOutput.contains(expectedOutput));
}
}
public void testRSE(String machineName, String addition) throws IOException, InterruptedException {
boolean execute = true;
boolean modelChecking = false;
boolean noInv = false;
boolean noDead = false;
generateTestFiles(machineName, modelChecking, addition);
compileTestFiles();
if(!execute) {
cleanup();
return;
}
String result = runTestFiles(modelChecking, noDead, noInv);
verifyOutput(machineName, modelChecking, result);
cleanup();
}
}
MACHINE IntegerPower
VARIABLES x,y,res
INVARIANT x : INT & y : INT & res : INT
INITIALISATION x := 2; y := 8; res := 0
OPERATIONS
calculate = BEGIN res := x ** y END;
out <-- getRes = out := res
END
\ No newline at end of file
256
\ No newline at end of file
fn main() {
let mut ip = IntegerPower::new();
ip.calculate();
println!("{}", ip.getRes());
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment