Skip to content

Commit

Permalink
Merge branch 'master' into highprecision
Browse files Browse the repository at this point in the history
  • Loading branch information
@nickbattle
nickbattle committed Jan 5, 2024
2 parents 37f7d34 + d63e79c commit 919f7d6
Show file tree
Hide file tree
Showing 5 changed files with 65 additions and 36 deletions.
40 changes: 28 additions & 12 deletions quickcheck/src/main/java/quickcheck/QuickCheck.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,8 @@
package quickcheck;

import static com.fujitsu.vdmj.plugins.PluginConsole.errorln;
import static com.fujitsu.vdmj.plugins.PluginConsole.infof;
import static com.fujitsu.vdmj.plugins.PluginConsole.infoln;
import static com.fujitsu.vdmj.plugins.PluginConsole.println;
import static quickcheck.commands.QCConsole.infof;
import static quickcheck.commands.QCConsole.infoln;
Expand All @@ -45,8 +47,8 @@
import com.fujitsu.vdmj.in.definitions.INClassDefinition;
import com.fujitsu.vdmj.in.expressions.INBooleanLiteralExpression;
import com.fujitsu.vdmj.in.expressions.INExpression;
import com.fujitsu.vdmj.in.patterns.INBindingOverride;
import com.fujitsu.vdmj.in.patterns.INBindingGlobals;
import com.fujitsu.vdmj.in.patterns.INBindingOverride;
import com.fujitsu.vdmj.lex.Dialect;
import com.fujitsu.vdmj.mapper.ClassMapper;
import com.fujitsu.vdmj.po.annotations.POAnnotation;
Expand All @@ -71,8 +73,8 @@
import com.fujitsu.vdmj.values.Value;
import com.fujitsu.vdmj.values.ValueList;

import quickcheck.annotations.po.POQuickCheckAnnotation;
import quickcheck.annotations.IterableContext;
import quickcheck.annotations.po.POQuickCheckAnnotation;
import quickcheck.strategies.FixedQCStrategy;
import quickcheck.strategies.QCStrategy;
import quickcheck.strategies.StrategyResults;
Expand Down Expand Up @@ -751,6 +753,10 @@ private Context addSelf(ProofObligation po, Context ctxt)
{
try
{
ClassInterpreter in = ClassInterpreter.getInstance();
INClassDefinition classdef = in.getDefaultClass();
ObjectValue object = null;

if (po.annotations != null)
{
for (POAnnotation a: po.annotations)
Expand All @@ -759,29 +765,39 @@ private Context addSelf(ProofObligation po, Context ctxt)
{
POQuickCheckAnnotation qca = (POQuickCheckAnnotation)a;

if (qca.qcConstructor != null)
if (qca.tc != null)
{
// create object and return it... how?
if (qca.newexp == null) // cached
{
qca.newexp = ClassMapper.getInstance(INNode.MAPPINGS).convert(qca.tc.qcConstructor);
}

object = (ObjectValue) qca.newexp.eval(in.getInitialContext());
break;
}
}
}
}

ClassInterpreter in = ClassInterpreter.getInstance();
INClassDefinition classdef = in.getDefaultClass();
ObjectValue object = classdef.newInstance(null, null, ctxt);

ctxt = new ObjectContext(
classdef.name.getLocation(), classdef.name.getName() + "()",
ctxt, object);

if (object == null)
{
object = classdef.newInstance(null, null, ctxt);

ctxt = new ObjectContext(
classdef.name.getLocation(), classdef.name.getName() + "()",
ctxt, object);
}

ctxt.put(classdef.name.getSelfName(), object);
}
catch (ValueException e)
{
// Use ctxt unchanged?
}
catch (Exception e)
{
// Problem with "new"?
}
}

return ctxt;
Expand Down
15 changes: 9 additions & 6 deletions quickcheck/src/main/java/quickcheck/annotations/po/POQuickCheckAnnotation.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,36 +24,39 @@

package quickcheck.annotations.po;

import com.fujitsu.vdmj.in.expressions.INNewExpression;
import com.fujitsu.vdmj.po.annotations.POAnnotation;
import com.fujitsu.vdmj.po.expressions.PONewExpression;
import com.fujitsu.vdmj.tc.lex.TCIdentifierToken;
import com.fujitsu.vdmj.tc.types.TCParameterType;
import com.fujitsu.vdmj.tc.types.TCTypeList;
import com.fujitsu.vdmj.util.Utils;

import quickcheck.annotations.tc.TCQuickCheckAnnotation;

public class POQuickCheckAnnotation extends POAnnotation
{
private static final long serialVersionUID = 1L;

public final TCParameterType qcParam;
public final TCTypeList qcTypes;
public final PONewExpression qcConstructor;
public final TCQuickCheckAnnotation tc;
public INNewExpression newexp;

public POQuickCheckAnnotation(TCIdentifierToken name,
TCParameterType qcParam, TCTypeList qcTypes, PONewExpression qcConstructor)
TCParameterType qcParam, TCTypeList qcTypes, TCQuickCheckAnnotation tc)
{
super(name, null);
this.qcParam = qcParam;
this.qcTypes = qcTypes;
this.qcConstructor = qcConstructor;
this.tc = tc;
}

@Override
public String toString()
{
if (qcConstructor != null)
if (tc != null)
{
return "@" + name + " " + qcConstructor + ";";
return "@" + name + " " + tc.qcConstructor + ";";
}
else
{
Expand Down
2 changes: 1 addition & 1 deletion quickcheck/src/main/java/quickcheck/annotations/tc/TCQuickCheckAnnotation.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ public void tcBefore(TCDefinition def, Environment env, NameScope scope)

private void checkConstructor(TCDefinition def, Environment env, NameScope scope)
{
// check?
qcConstructor.typeCheck(env, null, scope, null);
}

private void checkTypeParams(TCDefinition def, Environment env, NameScope scope)
Expand Down
2 changes: 1 addition & 1 deletion quickcheck/src/main/resources/tc-po.mappings
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,5 +4,5 @@

# annotations
package quickcheck.annotations.tc to quickcheck.annotations.po;
map TCQuickCheckAnnotation{name, qcParam, qcTypes, qcConstructor} to POQuickCheckAnnotation(name, qcParam, qcTypes, qcConstructor);
map TCQuickCheckAnnotation{name, qcParam, qcTypes} to POQuickCheckAnnotation(name, qcParam, qcTypes, this);

42 changes: 26 additions & 16 deletions vdmj/src/main/java/com/fujitsu/vdmj/mapper/ClassMapper.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@

import java.io.File;
import java.io.InputStream;
import java.io.PrintStream;
import java.lang.reflect.Constructor;
import java.lang.reflect.Field;
import java.lang.reflect.InvocationTargetException;
Expand Down Expand Up @@ -65,19 +66,26 @@ public class ClassMapper

/**
* Get an instance of a mapper, defined by the mapspec file name (resource).
* The error stream can be passed too, with a default getInstance that
* uses System.err.
*/
public static ClassMapper getInstance(String config)
public static ClassMapper getInstance(String config, PrintStream err)
{
ClassMapper mapper = mappers.get(config);

if (mapper == null)
{
mapper = new ClassMapper(config);
mapper = new ClassMapper(config, err);
mappers.put(config, mapper);
}

return mapper;
}

public static ClassMapper getInstance(String config)
{
return getInstance(config, System.err);
}

/**
* Initialise the progress stack and converted objects map.
Expand Down Expand Up @@ -106,6 +114,7 @@ public ClassMapper init()
/**
* Fields used during the processing of the configuration file
*/
private final PrintStream errorStream;
private final String configFile;
private Field SELF;
private String srcPackage = "";
Expand All @@ -116,8 +125,9 @@ public ClassMapper init()
/**
* The private constructor, passed the resource name of the mapping file.
*/
private ClassMapper(String config)
private ClassMapper(String config, PrintStream err)
{
errorStream = err;
configFile = config;
long before = System.currentTimeMillis();

Expand All @@ -136,7 +146,7 @@ private ClassMapper(String config)

if (errorCount > 0)
{
System.err.println("Aborting with " + errorCount + " errors");
errorStream.println("Aborting with " + errorCount + " errors");
throw new ClassMapperException(config);
}
}
Expand Down Expand Up @@ -235,7 +245,7 @@ public String toString()

private void error(String message)
{
System.err.println(configFile + " line " + lineNo + ": " + message);
errorStream.println(configFile + " line " + lineNo + ": " + message);
errorCount++;
}

Expand Down Expand Up @@ -370,7 +380,7 @@ private void processUnmapped(Mapping command)

if (mappings.containsKey(toIgnore))
{
System.err.println("Class is already mapped: " + toIgnore.getName());
errorStream.println("Class is already mapped: " + toIgnore.getName());
}
// else
{
Expand Down Expand Up @@ -475,7 +485,7 @@ else if (srcFields.containsKey(field))

if (mappings.containsKey(srcClass))
{
System.err.println("Class is already mapped: " + srcClass.getName());
errorStream.println("Class is already mapped: " + srcClass.getName());
}
// else
{
Expand Down Expand Up @@ -580,21 +590,21 @@ private void verifyConstructors()
{
error("No such constructor: " + mp.destClass.getSimpleName() + "(" + typeString(paramTypes) + ")");

System.err.println("Fields available from " + entry.getSimpleName() + ":");
errorStream.println("Fields available from " + entry.getSimpleName() + ":");

for (Field f: getAllFields(entry))
{
System.err.println(" " + f.getType().getSimpleName() + " " + f.getName());
errorStream.println(" " + f.getType().getSimpleName() + " " + f.getName());
}

System.err.println("Constructors available for " + mp.destClass.getSimpleName() + ":");
errorStream.println("Constructors available for " + mp.destClass.getSimpleName() + ":");

for (Constructor<?> ctor: mp.destClass.getConstructors())
{
System.err.println(" " + mp.destClass.getSimpleName() + "(" + typeString(ctor.getParameterTypes()) + ")");
errorStream.println(" " + mp.destClass.getSimpleName() + "(" + typeString(ctor.getParameterTypes()) + ")");
}

System.err.println();
errorStream.println();
}

mp.setters = new Method[mp.setterFields.size()];
Expand Down Expand Up @@ -983,22 +993,22 @@ private void dumpProgress(Throwable throwable)
{
if (!inProgress.isEmpty())
{
System.err.println("ClassMapper conversion stack...");
errorStream.println("ClassMapper conversion stack...");
Progress top = inProgress.peek();
MapParams target = mappings.get(top.source.getClass());

for (Progress item: inProgress)
{
System.err.println(item.toString());
errorStream.println(item.toString());
}

if (target != null)
{
System.err.println(target.toString());
errorStream.println(target.toString());
}
}

System.err.println("FAILED: " + throwable.toString());
errorStream.println("FAILED: " + throwable.toString());
dumpedProgress = true;
}
}
Expand Down

0 comments on commit 919f7d6

Please sign in to comment.