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 Sep 24, 2023
2 parents d78ad2f + dad6af7 commit 78988d2
Show file tree
Hide file tree
Showing 20 changed files with 215 additions and 55 deletions.
67 changes: 46 additions & 21 deletions examples/quickcheck/src/main/java/quickcheck/QuickCheck.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,13 +36,14 @@
import java.util.Map;
import java.util.Vector;

import com.fujitsu.vdmj.Settings;
import com.fujitsu.vdmj.ast.lex.LexBooleanToken;
import com.fujitsu.vdmj.in.INNode;
import com.fujitsu.vdmj.in.expressions.INBooleanLiteralExpression;
import com.fujitsu.vdmj.in.expressions.INExpression;
import com.fujitsu.vdmj.in.patterns.INBindingSetter;
import com.fujitsu.vdmj.lex.Dialect;
import com.fujitsu.vdmj.mapper.ClassMapper;
import com.fujitsu.vdmj.messages.Console;
import com.fujitsu.vdmj.pog.POStatus;
import com.fujitsu.vdmj.pog.ProofObligation;
import com.fujitsu.vdmj.pog.ProofObligationList;
Expand All @@ -53,8 +54,12 @@
import com.fujitsu.vdmj.tc.expressions.TCExistsExpression;
import com.fujitsu.vdmj.tc.expressions.TCExpression;
import com.fujitsu.vdmj.tc.lex.TCNameToken;
import com.fujitsu.vdmj.tc.types.TCParameterType;
import com.fujitsu.vdmj.tc.types.TCRealType;
import com.fujitsu.vdmj.tc.types.TCType;
import com.fujitsu.vdmj.util.GetResource;
import com.fujitsu.vdmj.values.BooleanValue;
import com.fujitsu.vdmj.values.ParameterValue;
import com.fujitsu.vdmj.values.Value;
import com.fujitsu.vdmj.values.ValueList;

Expand Down Expand Up @@ -247,6 +252,12 @@ public ProofObligationList getPOs(ProofObligationList all, List<Integer> poList)
}
}

if (!all.isEmpty() && chosen.isEmpty())
{
String m = (Settings.dialect == Dialect.VDM_SL) ? "module" : "class";
println("No POs in current " + m + " (" + def + ")");
}

return chosen; // No PO#s specified, so use default class/module's POs
}
else
Expand Down Expand Up @@ -310,10 +321,11 @@ public Results getValues(ProofObligation po)
INExpression exp = getINExpression(po);
List<INBindingSetter> binds = getINBindList(exp);
long before = System.currentTimeMillis();
Context ctxt = addTypeParams(po, Interpreter.getInstance().getInitialContext());

for (QCStrategy strategy: strategies)
{
Results presults = strategy.getValues(po, exp, binds);
Results presults = strategy.getValues(po, exp, binds, ctxt);
Map<String, ValueList> cexamples = presults.counterexamples;

for (String bind: cexamples.keySet())
Expand All @@ -336,7 +348,6 @@ public Results getValues(ProofObligation po)
if (!union.containsKey(bind.toString()))
{
// Generate some values for missing bindings, using the fixed method
RootContext ctxt = Interpreter.getInstance().getInitialContext();
ValueList list = new ValueList();
list.addAll(bind.getType().apply(new FixedRangeCreator(ctxt), 10));
union.put(bind.toString(), list);
Expand All @@ -351,9 +362,9 @@ public void checkObligation(ProofObligation po, Results results)
try
{
resetErrors(); // Only flag fatal errors
RootContext ctxt = Interpreter.getInstance().getInitialContext();
Context ctxt = Interpreter.getInstance().getInitialContext();
INExpression poexp = getINExpression(po);
List<INBindingSetter> bindings = getINBindList(poexp);;
List<INBindingSetter> bindings = getINBindList(poexp);

if (!po.isCheckable)
{
Expand Down Expand Up @@ -396,6 +407,9 @@ else if (results.proved &&

long before = System.currentTimeMillis();
Value result = new BooleanValue(false);
ContextException exception = null;

ctxt = addTypeParams(po, ctxt);

try
{
Expand All @@ -404,28 +418,14 @@ else if (results.proved &&
}
catch (ContextException e)
{
printf("PO #%d, Exception: %s\n", po.number, e.getMessage());

if (e.rawMessage.equals("Execution cancelled"))
{
result = null;
}
else
{
result = new BooleanValue(false);

if (e.ctxt.outer != null)
{
e.ctxt.printStackFrames(Console.out);
}
else
{
println("In context of " + e.ctxt.title + " " + e.ctxt.location);
}

println("----");
printBindings(bindings);
println("----");
exception = e;
}
}

Expand Down Expand Up @@ -465,10 +465,15 @@ else if (result instanceof BooleanValue)
{
printf("PO #%d, FAILED %s: ", po.number, duration(before, after));
printFailPath(bindings);

if (exception != null)
{
printf("Causes %s\n", exception.getMessage());
}

println("----");
println(po);
}

}
}
else
Expand Down Expand Up @@ -506,6 +511,26 @@ else if (result instanceof BooleanValue)
}
}

private Context addTypeParams(ProofObligation po, Context ctxt)
{
if (po.typeParams != null)
{
Context params = new Context(po.location, "Type params", ctxt);

for (TCType type: po.typeParams)
{
TCParameterType ptype = (TCParameterType)type;
params.put(ptype.name, new ParameterValue(new TCRealType(po.location)));
}

return params;
}
else
{
return ctxt;
}
}

private void printBindings(List<INBindingSetter> bindings)
{
int MAXVALUES = 10;
Expand Down
4 changes: 1 addition & 3 deletions examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,6 @@
import com.fujitsu.vdmj.messages.InternalException;
import com.fujitsu.vdmj.pog.ProofObligation;
import com.fujitsu.vdmj.runtime.Context;
import com.fujitsu.vdmj.runtime.Interpreter;
import com.fujitsu.vdmj.values.ValueList;

import quickcheck.QuickCheck;
Expand Down Expand Up @@ -122,15 +121,14 @@ public boolean init(QuickCheck qc)
}

@Override
public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds)
public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds, Context ctxt)
{
HashMap<String, ValueList> result = new HashMap<String, ValueList>();
long before = System.currentTimeMillis();
boolean proved = false;

if (po.isCheckable)
{
Context ctxt = Interpreter.getInstance().getInitialContext();
long product = 1;

for (INBindingSetter bind: binds)
Expand Down
42 changes: 38 additions & 4 deletions examples/quickcheck/src/main/java/quickcheck/strategies/FixedQCStrategy.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,23 +58,32 @@
import com.fujitsu.vdmj.messages.InternalException;
import com.fujitsu.vdmj.messages.VDMError;
import com.fujitsu.vdmj.pog.ProofObligation;
import com.fujitsu.vdmj.runtime.Context;
import com.fujitsu.vdmj.runtime.ContextException;
import com.fujitsu.vdmj.runtime.Interpreter;
import com.fujitsu.vdmj.runtime.RootContext;
import com.fujitsu.vdmj.syntax.BindReader;
import com.fujitsu.vdmj.syntax.ExpressionReader;
import com.fujitsu.vdmj.syntax.ParserException;
import com.fujitsu.vdmj.tc.TCNode;
import com.fujitsu.vdmj.tc.definitions.TCDefinition;
import com.fujitsu.vdmj.tc.definitions.TCDefinitionList;
import com.fujitsu.vdmj.tc.definitions.TCLocalDefinition;
import com.fujitsu.vdmj.tc.expressions.TCExpression;
import com.fujitsu.vdmj.tc.expressions.TCExpressionList;
import com.fujitsu.vdmj.tc.lex.TCNameToken;
import com.fujitsu.vdmj.tc.patterns.TCMultipleBind;
import com.fujitsu.vdmj.tc.patterns.TCMultipleBindList;
import com.fujitsu.vdmj.tc.patterns.TCMultipleTypeBind;
import com.fujitsu.vdmj.tc.types.TCFunctionType;
import com.fujitsu.vdmj.tc.types.TCNamedType;
import com.fujitsu.vdmj.tc.types.TCParameterType;
import com.fujitsu.vdmj.tc.types.TCSetType;
import com.fujitsu.vdmj.tc.types.TCType;
import com.fujitsu.vdmj.tc.types.TCTypeList;
import com.fujitsu.vdmj.tc.types.visitors.TCParameterCollector;
import com.fujitsu.vdmj.typechecker.Environment;
import com.fujitsu.vdmj.typechecker.FlatEnvironment;
import com.fujitsu.vdmj.typechecker.NameScope;
import com.fujitsu.vdmj.typechecker.TypeCheckException;
import com.fujitsu.vdmj.typechecker.TypeChecker;
Expand Down Expand Up @@ -226,18 +235,43 @@ private Map<String, ValueList> readRangeFile(String filename)
for (int i=0; i<tcbinds.size(); i++)
{
TCMultipleBind mb = tcbinds.get(i);
TCType mbtype = mb.typeCheck(env, NameScope.NAMESANDSTATE);
Environment penv = env;

if (mb instanceof TCMultipleTypeBind)
{
TCMultipleTypeBind mtb = (TCMultipleTypeBind)mb;
List<String> names = mtb.type.apply(new TCParameterCollector(), null);

if (!names.isEmpty())
{
TCDefinitionList defs = new TCDefinitionList();
LexLocation location = mtb.type.location;

for (String name: names)
{
TCNameToken tcname = new TCNameToken(location, module, name.substring(1));
TCParameterType ptype = new TCParameterType(tcname);
TCDefinition p = new TCLocalDefinition(location, tcname, ptype);
p.markUsed();
defs.add(p);
}

penv = new FlatEnvironment(defs, env);
}
}

TCType mbtype = mb.typeCheck(penv, NameScope.NAMESANDSTATE);
TCSetType mbset = new TCSetType(mb.location, mbtype);
tctypes.add(mbtype);

TCExpression exp = tcexps.get(i);
TCType exptype = exp.typeCheck(env, null, NameScope.NAMESANDSTATE, null);
TCType exptype = exp.typeCheck(penv, null, NameScope.NAMESANDSTATE, null);

if (TypeChecker.getErrorCount() > 0)
{
for (VDMError error: TypeChecker.getErrors())
{
println(exp);
println(mb + " = " + exp);
println(error.toString());
errorCount++;
}
Expand Down Expand Up @@ -438,7 +472,7 @@ public boolean init(QuickCheck qc)
}

@Override
public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds)
public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds, Context ctxt)
{
Map<String, ValueList> values = new HashMap<String, ValueList>();
long before = System.currentTimeMillis();
Expand Down
3 changes: 2 additions & 1 deletion examples/quickcheck/src/main/java/quickcheck/strategies/QCStrategy.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@
import com.fujitsu.vdmj.in.expressions.INExpression;
import com.fujitsu.vdmj.in.patterns.INBindingSetter;
import com.fujitsu.vdmj.pog.ProofObligation;
import com.fujitsu.vdmj.runtime.Context;

import quickcheck.QuickCheck;

Expand All @@ -38,6 +39,6 @@ abstract public class QCStrategy
abstract public boolean hasErrors();
abstract public boolean useByDefault();
abstract public boolean init(QuickCheck qc);
abstract public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds);
abstract public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds, Context ctxt);
abstract public String help();
}
7 changes: 2 additions & 5 deletions examples/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,8 +34,7 @@
import com.fujitsu.vdmj.in.expressions.INExpression;
import com.fujitsu.vdmj.in.patterns.INBindingSetter;
import com.fujitsu.vdmj.pog.ProofObligation;
import com.fujitsu.vdmj.runtime.Interpreter;
import com.fujitsu.vdmj.runtime.RootContext;
import com.fujitsu.vdmj.runtime.Context;
import com.fujitsu.vdmj.values.ValueList;
import com.fujitsu.vdmj.values.ValueSet;

Expand Down Expand Up @@ -128,15 +127,13 @@ public boolean init(QuickCheck qc)
}

@Override
public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds)
public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds, Context ctxt)
{
HashMap<String, ValueList> result = new HashMap<String, ValueList>();
long before = System.currentTimeMillis();

if (po.isCheckable && po.getCheckedExpression() != null)
{
RootContext ctxt = Interpreter.getInstance().getInitialContext();

for (INBindingSetter bind: binds)
{
RandomRangeCreator visitor = new RandomRangeCreator(ctxt, seed++);
Expand Down
3 changes: 2 additions & 1 deletion examples/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@
import com.fujitsu.vdmj.in.expressions.INExpression;
import com.fujitsu.vdmj.in.patterns.INBindingSetter;
import com.fujitsu.vdmj.pog.ProofObligation;
import com.fujitsu.vdmj.runtime.Context;
import com.fujitsu.vdmj.values.NameValuePair;
import com.fujitsu.vdmj.values.NameValuePairList;
import com.fujitsu.vdmj.values.ValueList;
Expand Down Expand Up @@ -78,7 +79,7 @@ public boolean init(QuickCheck qc)
}

@Override
public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds)
public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds, Context ctxt)
{
HashMap<String, ValueList> result = new HashMap<String, ValueList>();
long before = System.currentTimeMillis();
Expand Down
7 changes: 7 additions & 0 deletions examples/quickcheck/src/main/java/quickcheck/visitors/FixedRangeCreator.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,7 @@
import com.fujitsu.vdmj.tc.types.TCNaturalOneType;
import com.fujitsu.vdmj.tc.types.TCNaturalType;
import com.fujitsu.vdmj.tc.types.TCOptionalType;
import com.fujitsu.vdmj.tc.types.TCParameterType;
import com.fujitsu.vdmj.tc.types.TCProductType;
import com.fujitsu.vdmj.tc.types.TCQuoteType;
import com.fujitsu.vdmj.tc.types.TCRationalType;
Expand Down Expand Up @@ -118,6 +119,12 @@ public ValueSet caseUnknownType(TCUnknownType node, Integer limit)
// Anything... ?
return caseBooleanType(new TCBooleanType(LexLocation.ANY), limit);
}

@Override
public ValueSet caseParameterType(TCParameterType node, Integer limit)
{
return realLimit(limit); // For now...!
}

@Override
public ValueSet caseBooleanType(TCBooleanType type, Integer limit)
Expand Down
9 changes: 9 additions & 0 deletions examples/quickcheck/src/main/java/quickcheck/visitors/RandomRangeCreator.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,7 @@
import com.fujitsu.vdmj.tc.types.TCNaturalOneType;
import com.fujitsu.vdmj.tc.types.TCNaturalType;
import com.fujitsu.vdmj.tc.types.TCOptionalType;
import com.fujitsu.vdmj.tc.types.TCParameterType;
import com.fujitsu.vdmj.tc.types.TCProductType;
import com.fujitsu.vdmj.tc.types.TCQuoteType;
import com.fujitsu.vdmj.tc.types.TCRationalType;
Expand Down Expand Up @@ -72,6 +73,7 @@
import com.fujitsu.vdmj.values.NaturalOneValue;
import com.fujitsu.vdmj.values.NaturalValue;
import com.fujitsu.vdmj.values.NilValue;
import com.fujitsu.vdmj.values.ParameterValue;
import com.fujitsu.vdmj.values.QuoteValue;
import com.fujitsu.vdmj.values.RealValue;
import com.fujitsu.vdmj.values.RecordValue;
Expand Down Expand Up @@ -120,6 +122,13 @@ public ValueSet caseUnknownType(TCUnknownType node, Integer limit)
// Anything... ?
return caseBooleanType(new TCBooleanType(LexLocation.ANY), limit);
}

@Override
public ValueSet caseParameterType(TCParameterType node, Integer limit)
{
ParameterValue pv = (ParameterValue) ctxt.get(node.name);
return pv.type.apply(this, limit);
}

@Override
public ValueSet caseBooleanType(TCBooleanType type, Integer limit)
Expand Down
Loading

0 comments on commit 78988d2

Please sign in to comment.