Merge pull request #139 from ftsrg/xstsenums

Xsts type system rework, custom type serialization bugfix
ftsrg · Sep 9, 2021 · 1cbc98f · 1cbc98f
2 parents 20b4e49 + f94e626
commit 1cbc98f
Show file tree

Hide file tree

Showing 19 changed files with 353 additions and 177 deletions.
diff --git a/build.gradle.kts b/build.gradle.kts
@@ -10,7 +10,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.inf.theta"
-    version = "2.22.1"
+    version = "2.22.2"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayLitExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/arraytype/ArrayLitExpr.java
@@ -54,7 +54,7 @@ public static <IndexType extends Type, ElemType extends Type> ArrayLitExpr<Index
 
 	public List<Tuple2<LitExpr<IndexType>, LitExpr<ElemType>>> getElements() { return ImmutableList.copyOf(elems); }
 
-	public Expr<ElemType> getElseElem() { return elseElem; }
+	public LitExpr<ElemType> getElseElem() { return elseElem; }
 
 	@Override
 	public ArrayType<IndexType, ElemType> getType() {

diff --git a/...-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/concretizer/XstsStateSequence.java b/...-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/concretizer/XstsStateSequence.java
@@ -6,10 +6,8 @@
 import hu.bme.mit.theta.common.Utils;
 import hu.bme.mit.theta.core.decl.VarDecl;
 import hu.bme.mit.theta.core.type.LitExpr;
-import hu.bme.mit.theta.core.type.inttype.IntLitExpr;
 import hu.bme.mit.theta.xsts.XSTS;
 import hu.bme.mit.theta.xsts.analysis.XstsState;
-import hu.bme.mit.theta.xsts.dsl.XstsTypeDeclSymbol;
 
 import java.util.List;
 import java.util.Optional;
@@ -76,18 +74,9 @@ public String toString() {
 	public String stateToString(ExplState state) {
 		final LispStringBuilder sb = Utils.lispStringBuilder(ExplState.class.getSimpleName()).body();
 		for (VarDecl decl : xsts.getVars()) {
-			Optional<LitExpr<?>> val = state.eval(decl);
+			Optional<LitExpr> val = state.eval(decl);
 			if (val.isPresent()) {
-				if (xsts.getVarToType().containsKey(decl)) {
-					XstsTypeDeclSymbol type = xsts.getVarToType().get(decl);
-					IntLitExpr intValue = (IntLitExpr) val.get();
-					var optSymbol = type.getLiterals().stream()
-							.filter(symbol -> symbol.getIntValue().equals(intValue.getValue()))
-							.findFirst();
-					if(optSymbol.isPresent()) sb.add(String.format("(%s %s)", decl.getName(), optSymbol.get().getName()));
-				} else {
-					sb.add(String.format("(%s %s)", decl.getName(), val.get()));
-				}
+				sb.add(String.format("(%s %s)", decl.getName(), xsts.getVarToType().get(decl).serializeLiteral(val.get())));
 			}
 		}
 		return sb.toString();

diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/XSTS.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/XSTS.java
@@ -7,15 +7,15 @@
 import hu.bme.mit.theta.core.type.booltype.BoolType;
 import hu.bme.mit.theta.core.utils.ExprUtils;
 import hu.bme.mit.theta.core.utils.StmtUtils;
-import hu.bme.mit.theta.xsts.dsl.XstsTypeDeclSymbol;
+import hu.bme.mit.theta.xsts.type.XstsType;
 
 import java.util.*;
 
 import static com.google.common.base.Preconditions.checkNotNull;
 
 public final class XSTS {
 	private final Collection<VarDecl<?>> vars;
-	private final Map<VarDecl<?>, XstsTypeDeclSymbol> varToType;
+	private final Map<VarDecl<?>, XstsType<?>> varToType;
 	private final Set<VarDecl<?>> ctrlVars;
 
 	private final NonDetStmt tran;
@@ -31,7 +31,7 @@ public Collection<VarDecl<?>> getVars() {
 		return vars;
 	}
 
-	public Map<VarDecl<?>, XstsTypeDeclSymbol> getVarToType() { return varToType; }
+	public Map<VarDecl<?>, XstsType<?>> getVarToType() { return varToType; }
 
 	public Expr<BoolType> getProp() { return prop; }
 
@@ -47,7 +47,7 @@ public NonDetStmt getEnv() {
 
 	public Set<VarDecl<?>> getCtrlVars() { return ctrlVars; }
 
-	public XSTS(final Map<VarDecl<?>, XstsTypeDeclSymbol> varToType, final Set<VarDecl<?>> ctrlVars, final NonDetStmt init, final NonDetStmt tran, final NonDetStmt env, final Expr<BoolType> initFormula, final Expr<BoolType> prop) {
+	public XSTS(final Map<VarDecl<?>, XstsType<?>> varToType, final Set<VarDecl<?>> ctrlVars, final NonDetStmt init, final NonDetStmt tran, final NonDetStmt env, final Expr<BoolType> initFormula, final Expr<BoolType> prop) {
 		this.tran = checkNotNull(tran);
 		this.init = checkNotNull(init);
 		this.env = checkNotNull(env);

diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsCustomLiteralSymbol.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsCustomLiteralSymbol.java
@@ -0,0 +1,38 @@
+package hu.bme.mit.theta.xsts.dsl;
+
+import hu.bme.mit.theta.common.dsl.Symbol;
+import hu.bme.mit.theta.core.type.Expr;
+import hu.bme.mit.theta.xsts.type.XstsCustomType;
+
+import java.math.BigInteger;
+
+import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int;
+
+public class XstsCustomLiteralSymbol implements Symbol {
+
+	private final XstsCustomType.XstsCustomLiteral literal;
+
+	private static int counter = 0;
+
+	public XstsCustomLiteralSymbol(String name) {
+		this.literal = XstsCustomType.XstsCustomLiteral.of(name, BigInteger.valueOf(counter++));
+	}
+
+	@Override
+	public String getName() {
+		return literal.getName();
+	}
+
+	@Override
+	public String toString() {
+		return literal.toString();
+	}
+
+	public Expr instantiate(){
+		return Int(literal.getIntValue());
+	}
+
+	public XstsCustomType.XstsCustomLiteral getLiteral() {
+		return literal;
+	}
+}
diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsCustomTypeSymbol.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsCustomTypeSymbol.java
@@ -0,0 +1,53 @@
+package hu.bme.mit.theta.xsts.dsl;
+
+import hu.bme.mit.theta.common.dsl.Symbol;
+import hu.bme.mit.theta.core.type.Type;
+import hu.bme.mit.theta.xsts.type.XstsCustomType;
+
+import java.util.Objects;
+
+public final class XstsCustomTypeSymbol implements Symbol {
+
+	private XstsCustomType xstsType;
+
+	private XstsCustomTypeSymbol(final XstsCustomType xstsType) {
+		this.xstsType =xstsType;
+	}
+
+	public static XstsCustomTypeSymbol of(final XstsCustomType xstsType) {
+		return new XstsCustomTypeSymbol(xstsType);
+	}
+
+	@Override
+	public int hashCode() {
+		return Objects.hash(xstsType);
+	}
+
+	@Override
+	public boolean equals(final Object obj) {
+		if (this == obj) {
+			return true;
+		} else if (obj instanceof XstsCustomTypeSymbol) {
+			final XstsCustomTypeSymbol that = (XstsCustomTypeSymbol) obj;
+			return this.xstsType.equals(that.xstsType);
+		} else {
+			return false;
+		}
+	}
+
+	@Override
+	public String toString() {
+		return xstsType.toString();
+	}
+
+	public XstsCustomType getXstsType(){
+		return xstsType;
+	}
+
+	@Override
+	public String getName() { return xstsType.getName(); }
+
+	public Type instantiate() {
+		return xstsType.getType();
+	}
+}
diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsExpression.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsExpression.java
@@ -498,7 +498,7 @@ private <T1 extends Type, T2 extends Type> Expr<?> createArrayLitExpr(final ArrL
 			final T2 valueType;
 
 			if(ctx.indexType != null) {
-				indexType = (T1) new XstsType(typeTable,ctx.indexType).instantiate(env);
+				indexType = (T1) new XstsType(typeTable,ctx.indexType).instantiate(env).getType();
 			}
 			else {
 				indexType = (T1) ctx.indexExpr.get(0).accept(this).getType();

diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsSpecification.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsSpecification.java
@@ -7,8 +7,11 @@
 import hu.bme.mit.theta.core.stmt.NonDetStmt;
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
+import hu.bme.mit.theta.core.utils.ExprUtils;
 import hu.bme.mit.theta.xsts.XSTS;
 import hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.XstsContext;
+import hu.bme.mit.theta.xsts.type.XstsCustomType;
+import hu.bme.mit.theta.xsts.type.XstsType;
 
 import java.util.*;
 import java.util.regex.Pattern;
@@ -47,56 +50,50 @@ public Optional<? extends Symbol> resolve(String name) {
 	public XSTS instantiate(){
 		final Env env = new Env();
 
-		final Map<VarDecl<?>, XstsTypeDeclSymbol> varToType = Containers.createMap();
+		final Map<VarDecl<?>, XstsType<?>> varToType = Containers.createMap();
 		final Set<VarDecl<?>> ctrlVars = Containers.createSet();
 		final List<Expr<BoolType>> initExprs = new ArrayList<>();
 
 		for(var typeDeclContext: context.typeDeclarations){
-			final List<XstsTypeLiteralSymbol> literals = new ArrayList<>();
+			final List<XstsCustomLiteralSymbol> literalSymbols = new ArrayList<>();
 			for(var literalContext: typeDeclContext.literals){
 				var optSymbol = resolve(literalContext.name.getText());
 				if(optSymbol.isPresent()){
-					literals.add((XstsTypeLiteralSymbol) optSymbol.get());
+					literalSymbols.add((XstsCustomLiteralSymbol) optSymbol.get());
 				} else {
-					var symbol = new XstsTypeLiteralSymbol(literalContext.name.getText());
-					literals.add(symbol);
+					var symbol = new XstsCustomLiteralSymbol(literalContext.name.getText());
+					literalSymbols.add(symbol);
 					declare(symbol);
 					env.define(symbol,symbol.instantiate());
 				}
 			}
+			final List<XstsCustomType.XstsCustomLiteral> literals = literalSymbols.stream().map(XstsCustomLiteralSymbol::getLiteral).collect(Collectors.toList());
+			final XstsCustomType xstsCustomType = XstsCustomType.of(typeDeclContext.name.getText(),literals);
 
-			final XstsTypeDeclSymbol typeDeclSymbol = XstsTypeDeclSymbol.of(typeDeclContext.name.getText(),literals);
+			final XstsCustomTypeSymbol typeDeclSymbol = XstsCustomTypeSymbol.of(xstsCustomType);
 			typeTable.add(typeDeclSymbol);
-			env.define(typeDeclSymbol,typeDeclSymbol.instantiate());
+			env.define(typeDeclSymbol,typeDeclSymbol.getXstsType());
 		}
 
 		for(var varDeclContext: context.variableDeclarations){
 			if (tempVarPattern.matcher(varDeclContext.name.getText()).matches()){
 				throw new ParseException(varDeclContext, "Variable name '" + varDeclContext.name.getText() + "' is reserved!");
 			}
 
-			final XstsVariableSymbol symbol = new XstsVariableSymbol(typeTable,varDeclContext);
+			final XstsVariableSymbol symbol = new XstsVariableSymbol(typeTable, varToType, varDeclContext);
 			declare(symbol);
 
-			final VarDecl<?> var = symbol.instantiate(env);
-			final Optional<? extends Symbol> typeDeclSymbol = typeTable.get(varDeclContext.ttype.getText());
-			if (typeDeclSymbol.isPresent()) {
-				varToType.put(var, (XstsTypeDeclSymbol) typeDeclSymbol.get());
-			}
+			final VarDecl var = symbol.instantiate(env);
 			if(varDeclContext.CTRL()!=null) ctrlVars.add(var);
 			if(varDeclContext.initValue!=null){
 				initExprs.add(Eq(var.getRef(),new XstsExpression(this,typeTable,varDeclContext.initValue).instantiate(env)));
-			} else if(varToType.containsKey(var)) {
-				final var type = varToType.get(var);
-				final Expr<BoolType> expr = Or(type.getLiterals().stream()
-						.map(lit -> Eq(var.getRef(),Int(lit.getIntValue())))
-						.collect(Collectors.toList()));
-				initExprs.add(expr);
+			} else {
+				initExprs.add(varToType.get(var).createBoundExpr(var));
 			}
 			env.define(symbol,var);
 		}
 
-		final Expr<BoolType> initFormula = And(initExprs);
+		final Expr<BoolType> initFormula = ExprUtils.simplify(And(initExprs));
 
 		final NonDetStmt tranSet = new XstsTransitionSet(this,typeTable,context.tran.transitionSet(), varToType).instantiate(env);
 		final NonDetStmt initSet = new XstsTransitionSet(this,typeTable,context.init.transitionSet(), varToType).instantiate(env);

diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsStatement.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsStatement.java
@@ -1,5 +1,6 @@
 package hu.bme.mit.theta.xsts.dsl;
 
+import com.google.common.collect.ImmutableList;
 import hu.bme.mit.theta.common.dsl.*;
 import hu.bme.mit.theta.core.decl.Decls;
 import hu.bme.mit.theta.core.decl.VarDecl;
@@ -11,18 +12,16 @@
 import hu.bme.mit.theta.core.type.arraytype.ArrayType;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
 import hu.bme.mit.theta.core.type.inttype.IntType;
-import hu.bme.mit.theta.core.utils.TypeUtils;
 import hu.bme.mit.theta.xsts.dsl.gen.XstsDslBaseVisitor;
 import hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.*;
+import hu.bme.mit.theta.xsts.type.XstsCustomType;
 
 import java.util.ArrayList;
 import java.util.List;
 import java.util.Map;
-import java.util.stream.Collectors;
 
 import static com.google.common.base.Preconditions.*;
 import static hu.bme.mit.theta.core.stmt.Stmts.*;
-import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq;
 import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Write;
 import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool;
 import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Or;
@@ -34,9 +33,9 @@ public class XstsStatement {
 	private final DynamicScope scope;
 	private final SymbolTable typeTable;
 	private final StmtContext context;
-	private final Map<VarDecl<?>, XstsTypeDeclSymbol> varToType;
+	private final Map<VarDecl<?>, hu.bme.mit.theta.xsts.type.XstsType<?>> varToType;
 
-	public XstsStatement(final DynamicScope scope, final SymbolTable typeTable, final StmtContext context, final Map<VarDecl<?>, XstsTypeDeclSymbol> varToType) {
+	public XstsStatement(final DynamicScope scope, final SymbolTable typeTable, final StmtContext context, final Map<VarDecl<?>, hu.bme.mit.theta.xsts.type.XstsType<?>> varToType) {
 		this.scope = checkNotNull(scope);
 		this.typeTable = checkNotNull(typeTable);
 		this.context = checkNotNull(context);
@@ -57,10 +56,10 @@ private static final class StmtCreatorVisitor extends XstsDslBaseVisitor<Stmt> {
 
 		private DynamicScope currentScope;
 		private final SymbolTable typeTable;
-		final Map<VarDecl<?>, XstsTypeDeclSymbol> varToType;
+		final Map<VarDecl<?>, hu.bme.mit.theta.xsts.type.XstsType<?>> varToType;
 		private final Env env;
 
-		public StmtCreatorVisitor(final DynamicScope scope, final SymbolTable typeTable, final Env env, final Map<VarDecl<?>, XstsTypeDeclSymbol> varToType) {
+		public StmtCreatorVisitor(final DynamicScope scope, final SymbolTable typeTable, final Env env, final Map<VarDecl<?>, hu.bme.mit.theta.xsts.type.XstsType<?>> varToType) {
 			this.currentScope = checkNotNull(scope);
 			this.typeTable = checkNotNull(typeTable);
 			this.env = checkNotNull(env);
@@ -83,14 +82,14 @@ public Stmt visitHavocStmt(final HavocStmtContext ctx) {
 			final String lhsId = ctx.lhs.getText();
 			final Symbol lhsSymbol = currentScope.resolve(lhsId).get();
 			final VarDecl<?> var = (VarDecl<?>) env.eval(lhsSymbol);
-			if(varToType.containsKey(var)){
-				final XstsTypeDeclSymbol type = varToType.get(var);
-				final Expr<BoolType> expr = Or(type.getLiterals().stream()
-						.map(lit -> Eq(var.getRef(),Int(lit.getIntValue())))
-						.collect(Collectors.toList()));
+
+			final hu.bme.mit.theta.xsts.type.XstsType type = varToType.get(var);
+			if(type instanceof XstsCustomType){
+				final Expr<BoolType> expr = type.createBoundExpr(var);
 				final AssumeStmt assume = Assume(expr);
 				return SequenceStmt.of(List.of(Havoc(var),assume));
 			}
+
 			return Havoc(var);
 		}
 
@@ -191,20 +190,27 @@ public Stmt visitLoopStmt(LoopStmtContext ctx) {
 		@Override
 		public Stmt visitLocalVarDeclStmt(LocalVarDeclStmtContext ctx) {
 			final String name = ctx.name.getText();
-			final Type type = new XstsType(typeTable,ctx.ttype).instantiate(env);
+			final hu.bme.mit.theta.xsts.type.XstsType xstsType = new XstsType(typeTable,ctx.ttype).instantiate(env);
+			final Type type = xstsType.getType();
 			final var decl = Decls.Var(name,type);
 			final Symbol symbol = DeclSymbol.of(decl);
 
-
 			final Stmt result;
+			final Stmt havoc = Havoc(decl);
 			if(ctx.initValue==null){
-				result = SkipStmt.getInstance();
+				if(xstsType instanceof XstsCustomType){
+					final Expr<BoolType> expr = xstsType.createBoundExpr(decl);
+					final AssumeStmt assume = Assume(expr);
+					result = SequenceStmt.of(List.of(havoc,assume));
+				} else {
+					result = havoc;
+				}
 			} else {
 				var expr = new XstsExpression(currentScope,typeTable,ctx.initValue).instantiate(env);
 				if (expr.getType().equals(decl.getType())) {
 					@SuppressWarnings("unchecked") final VarDecl<Type> tVar = (VarDecl<Type>) decl;
 					@SuppressWarnings("unchecked") final Expr<Type> tExpr = (Expr<Type>) expr;
-					result = Assign(tVar, tExpr);
+					result = SequenceStmt(ImmutableList.of(havoc, Assign(tVar,tExpr)));
 				} else {
 					throw new IllegalArgumentException("Type of " + decl + " is incompatilbe with " + expr);
 				}

diff --git a/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsTransitionSet.java b/subprojects/xsts/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XstsTransitionSet.java
@@ -9,6 +9,7 @@
 import hu.bme.mit.theta.core.stmt.Stmt;
 import hu.bme.mit.theta.xsts.dsl.gen.XstsDslBaseVisitor;
 import hu.bme.mit.theta.xsts.dsl.gen.XstsDslParser.TransitionSetContext;
+import hu.bme.mit.theta.xsts.type.XstsType;
 
 import java.util.List;
 import java.util.Map;
@@ -21,9 +22,9 @@ public class XstsTransitionSet {
 	private final DynamicScope scope;
 	private final SymbolTable typeTable;
 	private final TransitionSetContext context;
-	private final Map<VarDecl<?>, XstsTypeDeclSymbol> varToType;
+	private final Map<VarDecl<?>, XstsType<?>> varToType;
 
-	public XstsTransitionSet(final DynamicScope scope, final SymbolTable typeTable, final TransitionSetContext context, final Map<VarDecl<?>,XstsTypeDeclSymbol> varToType) {
+	public XstsTransitionSet(final DynamicScope scope, final SymbolTable typeTable, final TransitionSetContext context, final Map<VarDecl<?>,XstsType<?>> varToType) {
 		this.scope = checkNotNull(scope);
 		this.typeTable = checkNotNull(typeTable);
 		this.context = checkNotNull(context);