Merge branch 'master' into highprecision

nickbattle · Nov 8, 2024 · 0e47ba6 · 0e47ba6
2 parents 8aec033 + ffde163
commit 0e47ba6
Show file tree

Hide file tree

Showing 17 changed files with 313 additions and 101 deletions.
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.java
@@ -99,8 +99,19 @@ public ProofObligationList getDefProofObligations(POContextStack ctxt, POGState
 
 		for (PODefinition d: this)
 		{
-			obligations.addAll(d.getProofObligations(ctxt, pogState, env));
-			ctxt.push(new POLetDefContext(d));
+			if (d instanceof POExplicitFunctionDefinition || d instanceof POImplicitFunctionDefinition)
+			{
+				// local functions push their context first, to be callable in the POs that they generate.
+				ctxt.push(new POLetDefContext(d));
+				obligations.addAll(d.getProofObligations(ctxt, pogState, env));
+			}
+			else
+			{
+				// Regular definitions are only defined after themselves
+				obligations.addAll(d.getProofObligations(ctxt, pogState, env));
+				ctxt.push(new POLetDefContext(d));
+			}
+
 			count++;
 		}
 

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POValueDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POValueDefinition.java
@@ -110,7 +110,6 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog
 				(annotations != null) ? annotations.poBefore(this, ctxt) : new ProofObligationList();
 
 		list.addAll(exp.getProofObligations(ctxt, pogState, env));
-		list.stateUpdate(pogState, exp);
 
 		if (!(pattern instanceof POIdentifierPattern) &&
 			!(pattern instanceof POIgnorePattern) &&

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java
@@ -94,14 +94,6 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog
 
 		if (!type.isUnknown(location))
 		{
-			if (type.isOperation(location))
-			{
-				// We have to say that the POGState is as if the operation updates state, because
-				// it may read state even if pure, and an apply uses the return value. So QC can't
-				// evaluate them. This makes subsequent POs Unchecked.
-				pogState.setUpdateState(true, location);
-			}
-
 			if (type.isMap(location))
 			{
 				TCMapType m = type.getMap();
@@ -161,6 +153,14 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog
 			{
 				obligations.add(new SeqApplyObligation(root, args.get(0), ctxt));
 			}
+
+			if (type.isOperation(location))
+			{
+				// We have to say that the POGState is as if the operation updates state, because
+				// it may read state even if pure, and an apply uses the return value. So QC can't
+				// evaluate them. This makes subsequent POs Unchecked.
+				pogState.addOperationCall(location, null);
+			}
 		}
 
 		obligations.addAll(root.getProofObligations(ctxt, pogState, env));

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POExpression.java
@@ -165,20 +165,18 @@ public ProofObligationList checkUnionQualifiers(POExpression exp, TCTypeQualifie
 		return obligations;
 	}
 
-	public boolean updatesState()
+	public TCNameSet updatesState()
 	{
 		POStatementStateFinder finder = new POStatementStateFinder();
 		POVisitorSet<TCNameToken, TCNameSet, Boolean> vset = finder.getVistorSet();
-		TCNameSet names = vset.applyExpressionVisitor(this, true);
-		return !names.isEmpty();
+		return vset.applyExpressionVisitor(this, true);
 	}
 
-	public boolean readsState()
+	public TCNameSet readsState()
 	{
 		POStatementStateFinder finder = new POStatementStateFinder();
 		POVisitorSet<TCNameToken, TCNameSet, Boolean> vset = finder.getVistorSet();
-		TCNameSet names = vset.applyExpressionVisitor(this, false);
-		return !names.isEmpty();
+		return vset.applyExpressionVisitor(this, false);
 	}
 
 	/**

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAssignmentStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAssignmentStatement.java
@@ -93,7 +93,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog
 
 		for (TCNameToken update: updates)
 		{
-			pogState.didUpdateState(update);
+			pogState.didUpdateState(update, location);
 		}
 
 		if (!TypeComparator.isSubType(ctxt.checkType(exp, expType), targetType))

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallObjectStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallObjectStatement.java
@@ -26,15 +26,23 @@
 
 import com.fujitsu.vdmj.ast.lex.LexNameToken;
 import com.fujitsu.vdmj.po.definitions.PODefinition;
+import com.fujitsu.vdmj.po.definitions.POExplicitFunctionDefinition;
+import com.fujitsu.vdmj.po.definitions.POExplicitOperationDefinition;
+import com.fujitsu.vdmj.po.definitions.POImplicitFunctionDefinition;
+import com.fujitsu.vdmj.po.definitions.POImplicitOperationDefinition;
 import com.fujitsu.vdmj.po.expressions.POExpression;
 import com.fujitsu.vdmj.po.expressions.POExpressionList;
 import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor;
 import com.fujitsu.vdmj.pog.POContextStack;
 import com.fujitsu.vdmj.pog.POGState;
 import com.fujitsu.vdmj.pog.ProofObligationList;
+import com.fujitsu.vdmj.pog.SubTypeObligation;
 import com.fujitsu.vdmj.tc.lex.TCIdentifierToken;
 import com.fujitsu.vdmj.tc.lex.TCNameToken;
+import com.fujitsu.vdmj.tc.types.TCType;
+import com.fujitsu.vdmj.tc.types.TCTypeList;
 import com.fujitsu.vdmj.typechecker.Environment;
+import com.fujitsu.vdmj.typechecker.TypeComparator;
 import com.fujitsu.vdmj.util.Utils;
 
 public class POCallObjectStatement extends POStatement
@@ -72,16 +80,63 @@ public String toString()
 	public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env)
 	{
 		ProofObligationList obligations = new ProofObligationList();
+		TCTypeList paramTypes = getParamTypes();
+		int i = 0;
 
 		for (POExpression exp: args)
 		{
 			obligations.addAll(exp.getProofObligations(ctxt, pogState, env));
+
+			TCType pt = paramTypes.get(i);
+			TCType at = exp.getExptype();
+
+			if (!TypeComparator.isSubType(at, pt))
+			{
+				obligations.add(new SubTypeObligation(args.get(i), pt, at, ctxt));
+			}
+
+			i++;
 		}
 
-		pogState.addOperation(location, fdef);
+		pogState.addOperationCall(location, fdef);
 
 		return obligations;
 	}
+
+	private TCTypeList getParamTypes()
+	{
+		if (fdef instanceof POExplicitOperationDefinition)
+		{
+			POExplicitOperationDefinition exop = (POExplicitOperationDefinition)fdef;
+			return exop.type.parameters;
+		}
+		else if (fdef instanceof POImplicitOperationDefinition)
+		{
+			POImplicitOperationDefinition imop = (POImplicitOperationDefinition)fdef;
+			return imop.type.parameters;
+		}
+		else if (fdef instanceof POExplicitFunctionDefinition)
+		{
+			POExplicitFunctionDefinition exfn = (POExplicitFunctionDefinition)fdef;
+			return exfn.type.parameters;
+		}
+		else if (fdef instanceof POImplicitFunctionDefinition)
+		{
+			POImplicitFunctionDefinition imfn = (POImplicitFunctionDefinition)fdef;
+			return imfn.type.parameters;
+		}
+		else	// Should never happen, but don't fail
+		{
+			TCTypeList list = new TCTypeList();
+
+			for (POExpression arg: args)
+			{
+				list.add(arg.getExptype());
+			}
+
+			return list;
+		}
+	}
 
 	@Override
 	public <R, S> R apply(POStatementVisitor<R, S> visitor, S arg)

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallStatement.java
@@ -25,14 +25,22 @@
 package com.fujitsu.vdmj.po.statements;
 
 import com.fujitsu.vdmj.po.definitions.PODefinition;
+import com.fujitsu.vdmj.po.definitions.POExplicitFunctionDefinition;
+import com.fujitsu.vdmj.po.definitions.POExplicitOperationDefinition;
+import com.fujitsu.vdmj.po.definitions.POImplicitFunctionDefinition;
+import com.fujitsu.vdmj.po.definitions.POImplicitOperationDefinition;
 import com.fujitsu.vdmj.po.expressions.POExpression;
 import com.fujitsu.vdmj.po.expressions.POExpressionList;
 import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor;
 import com.fujitsu.vdmj.pog.POContextStack;
 import com.fujitsu.vdmj.pog.POGState;
 import com.fujitsu.vdmj.pog.ProofObligationList;
+import com.fujitsu.vdmj.pog.SubTypeObligation;
 import com.fujitsu.vdmj.tc.lex.TCNameToken;
+import com.fujitsu.vdmj.tc.types.TCType;
+import com.fujitsu.vdmj.tc.types.TCTypeList;
 import com.fujitsu.vdmj.typechecker.Environment;
+import com.fujitsu.vdmj.typechecker.TypeComparator;
 import com.fujitsu.vdmj.util.Utils;
 
 public class POCallStatement extends POStatement
@@ -60,17 +68,64 @@ public String toString()
 	public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env)
 	{
 		ProofObligationList obligations = new ProofObligationList();
+		TCTypeList paramTypes = getParamTypes();
+		int i = 0;
 
 		for (POExpression exp: args)
 		{
 			obligations.addAll(exp.getProofObligations(ctxt, pogState, env));
+
+			TCType pt = paramTypes.get(i);
+			TCType at = exp.getExptype();
+
+			if (!TypeComparator.isSubType(at, pt))
+			{
+				obligations.add(new SubTypeObligation(args.get(i), pt, at, ctxt));
+			}
+
+			i++;
 		}
 
-		pogState.addOperation(location, opdef);
+		pogState.addOperationCall(location, opdef);
 
 		return obligations;
 	}
 
+	private TCTypeList getParamTypes()
+	{
+		if (opdef instanceof POExplicitOperationDefinition)
+		{
+			POExplicitOperationDefinition exop = (POExplicitOperationDefinition)opdef;
+			return exop.type.parameters;
+		}
+		else if (opdef instanceof POImplicitOperationDefinition)
+		{
+			POImplicitOperationDefinition imop = (POImplicitOperationDefinition)opdef;
+			return imop.type.parameters;
+		}
+		else if (opdef instanceof POExplicitFunctionDefinition)
+		{
+			POExplicitFunctionDefinition exfn = (POExplicitFunctionDefinition)opdef;
+			return exfn.type.parameters;
+		}
+		else if (opdef instanceof POImplicitFunctionDefinition)
+		{
+			POImplicitFunctionDefinition imfn = (POImplicitFunctionDefinition)opdef;
+			return imfn.type.parameters;
+		}
+		else	// Should never happen, but don't fail
+		{
+			TCTypeList list = new TCTypeList();
+
+			for (POExpression arg: args)
+			{
+				list.add(arg.getExptype());
+			}
+
+			return list;
+		}
+	}
+
 	@Override
 	public <R, S> R apply(POStatementVisitor<R, S> visitor, S arg)
 	{

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/visitors/POStatementStateFinder.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/visitors/POStatementStateFinder.java
@@ -116,7 +116,7 @@ public TCNameSet caseLetDefStatement(POLetDefStatement node, Boolean updates)
 			{
 				POValueDefinition vdef = (POValueDefinition)def;
 
-				if (vdef.exp.readsState())
+				if (!vdef.exp.readsState().isEmpty())
 				{
 					for (PODefinition ldef: vdef.defs)
 					{