Skip to content

Commit

Permalink
[NF] Improve error checking of when-clauses.
Browse files Browse the repository at this point in the history 
- Moved the check of equations inside when-equations from Inst to
  Typing, to allow skipping the check if the when is clocked.
- Mark lhs subscripts in when-equations as structural.
- Added check that clocked when doesn't have an elsewhen.
- Added check that non-clocked when doesn't have a clocked elsewhen.
- Made clocked when illegal in algorithm.
- Added new phase VerifyModel that checks for errors that can't be
  detected until after flattening and constant evaluation.
  It currently checks that each branch of a when-equation contains
  the same set of crefs.
- Implemented BaseAvlSet.isEqual.
- Renamed Expression.ClockKind.toString to toDebugString, and
  implemented new toString that doesn't leak implementation details.

Belonging to [master]:
  - OpenModelica/OMCompiler#3001
  - OpenModelica/OpenModelica-testsuite#1148
  • Loading branch information
@perost @OpenModelica-Hudson
perost authored and OpenModelica-Hudson committed Mar 26, 2019
1 parent e3fab53 commit ab4e3e6
Show file tree
Hide file tree
Showing 8 changed files with 347 additions and 87 deletions.
42 changes: 30 additions & 12 deletions Compiler/NFFrontEnd/NFExpression.mo
View file
Expand Up @@ -133,27 +133,45 @@ public
ock := match ick
local
Expression i, ic, r, c, si, sm;
case (INFERRED_CLOCK()) then DAE.INFERRED_CLOCK();
case (INTEGER_CLOCK(i, r)) then DAE.INTEGER_CLOCK(Expression.toDAE(i), Expression.toDAE(r));
case (REAL_CLOCK(i)) then DAE.REAL_CLOCK(Expression.toDAE(i));
case (BOOLEAN_CLOCK(c, si)) then DAE.BOOLEAN_CLOCK(Expression.toDAE(c), Expression.toDAE(si));
case (SOLVER_CLOCK(c, sm)) then DAE.SOLVER_CLOCK(Expression.toDAE(c), Expression.toDAE(sm));
case INFERRED_CLOCK() then DAE.INFERRED_CLOCK();
case INTEGER_CLOCK(i, r) then DAE.INTEGER_CLOCK(Expression.toDAE(i), Expression.toDAE(r));
case REAL_CLOCK(i) then DAE.REAL_CLOCK(Expression.toDAE(i));
case BOOLEAN_CLOCK(c, si) then DAE.BOOLEAN_CLOCK(Expression.toDAE(c), Expression.toDAE(si));
case SOLVER_CLOCK(c, sm) then DAE.SOLVER_CLOCK(Expression.toDAE(c), Expression.toDAE(sm));
end match;
end toDAE;

function toString
function toDebugString
input ClockKind ick;
output String ock;
algorithm
ock := match ick
local
Expression i, ic, r, c, si, sm;
case (INFERRED_CLOCK()) then "INFERRED_CLOCK()";
case (INTEGER_CLOCK(i, r)) then "INTEGER_CLOCK(" + Expression.toString(i) + ", " + Expression.toString(r) + ")";
case (REAL_CLOCK(i)) then "REAL_CLOCK(" + Expression.toString(i) + ")";
case (BOOLEAN_CLOCK(c, si)) then "BOOLEAN_CLOCK(" + Expression.toString(c) + ", " + Expression.toString(si) + ")";
case (SOLVER_CLOCK(c, sm)) then "SOLVER_CLOCK(" + Expression.toString(c) + ", " + Expression.toString(sm) + ")";
case INFERRED_CLOCK() then "INFERRED_CLOCK()";
case INTEGER_CLOCK(i, r) then "INTEGER_CLOCK(" + Expression.toString(i) + ", " + Expression.toString(r) + ")";
case REAL_CLOCK(i) then "REAL_CLOCK(" + Expression.toString(i) + ")";
case BOOLEAN_CLOCK(c, si) then "BOOLEAN_CLOCK(" + Expression.toString(c) + ", " + Expression.toString(si) + ")";
case SOLVER_CLOCK(c, sm) then "SOLVER_CLOCK(" + Expression.toString(c) + ", " + Expression.toString(sm) + ")";
end match;
end toDebugString;

function toString
input ClockKind ck;
output String str;
algorithm
str := match ck
local
Expression e1, e2;

case INFERRED_CLOCK() then "";
case INTEGER_CLOCK(e1, e2) then Expression.toString(e1) + ", " + Expression.toString(e2);
case REAL_CLOCK(e1) then Expression.toString(e1);
case BOOLEAN_CLOCK(e1, e2) then Expression.toString(e1) + ", " + Expression.toString(e2);
case SOLVER_CLOCK(e1, e2) then Expression.toString(e1) + ", " + Expression.toString(e2);
end match;

str := "Clock(" + str + ")";
end toString;
end ClockKind;

Expand Down Expand Up @@ -1480,7 +1498,7 @@ public
case ENUM_LITERAL(ty = t as Type.ENUMERATION())
then Absyn.pathString(t.typePath) + "." + exp.name;

case CLKCONST(clk) then "CLKCONST(" + ClockKind.toString(clk) + ")";
case CLKCONST(clk) then ClockKind.toString(clk);

case CREF() then ComponentRef.toString(exp.cref);
case TYPENAME() then Type.typenameString(Type.arrayElementType(exp.ty));
Expand Down
27 changes: 4 additions & 23 deletions Compiler/NFFrontEnd/NFInst.mo
View file
Expand Up @@ -100,6 +100,7 @@ import Record = NFRecord;
import Variable = NFVariable;
import OperatorOverloading = NFOperatorOverloading;
import EvalConstants = NFEvalConstants;
import VerifyModel = NFVerifyModel;

public
function instClassInProgram
Expand Down Expand Up @@ -160,6 +161,8 @@ algorithm
flat_model := SimplifyModel.simplify(flat_model);
funcs := Flatten.collectFunctions(flat_model, name);

VerifyModel.verify(flat_model);

// Collect package constants that couldn't be substituted with their values
// (e.g. because they where used with non-constant subscripts), and add them
// to the model.
Expand Down Expand Up @@ -2738,11 +2741,6 @@ algorithm
algorithm
exp1 := instExp(scodeEq.expLeft, scope, info);
exp2 := instExp(scodeEq.expRight, scope, info);

if ExpOrigin.flagSet(origin, ExpOrigin.WHEN) and not checkLhsInWhen(exp1) then
Error.addSourceMessage(Error.WHEN_EQ_LHS, {Expression.toString(exp1)}, info);
fail();
end if;
then
Equation.EQUALITY(exp1, exp2, Type.UNKNOWN(), makeSource(scodeEq.comment, info));

Expand Down Expand Up @@ -3052,23 +3050,6 @@ algorithm
scope := InstNode.addIterator(iterator, scope);
end addIteratorToScope;

function checkLhsInWhen
input Expression exp;
output Boolean isValid;
algorithm
isValid := match exp
case Expression.CREF() then true;
case Expression.TUPLE()
algorithm
for e in exp.elements loop
checkLhsInWhen(e);
end for;
then
true;
else false;
end match;
end checkLhsInWhen;

function insertGeneratedInners
"Inner elements can be generated automatically during instantiation if they're
missing, and are stored in the cache of the top scope since that's easily
Expand Down Expand Up @@ -3144,7 +3125,7 @@ algorithm
algorithm
for c in cls_tree.components loop
if not InstNode.isEmpty(c) then
updateImplicitVariabilityComp(c, evalAllParams);
updateImplicitVariabilityComp(c, evalAllParams);
end if;
end for;

Expand Down
10 changes: 10 additions & 0 deletions Compiler/NFFrontEnd/NFType.mo
View file
Expand Up @@ -237,6 +237,16 @@ public
end match;
end isString;

function isClock
input Type ty;
output Boolean isClock;
algorithm
isClock := match ty
case CLOCK() then true;
else false;
end match;
end isClock;

function isScalar
input Type ty;
output Boolean isScalar;
Expand Down
153 changes: 102 additions & 51 deletions Compiler/NFFrontEnd/NFTyping.mo
View file
Expand Up @@ -136,6 +136,7 @@ package ExpOrigin
constant Type CONNECT = intBitLShift(1, 17); // Part of connect argument.
constant Type NOEVENT = intBitLShift(1, 18); // Part of noEvent argument.
constant Type ASSERT = intBitLShift(1, 19); // Part of assert argument.
constant Type CLOCKED = intBitLShift(1, 20); // Part of a clocked equation.

// Combined flags:
constant Type EQ_SUBEXPRESSION = intBitOr(EQUATION, SUBEXPRESSION);
Expand Down Expand Up @@ -2348,24 +2349,8 @@ algorithm
Integer next_origin;
SourceInfo info;

case Equation.EQUALITY()
algorithm
info := ElementSource.getInfo(eq.source);
(e1, ty1) := typeExp(eq.lhs, ExpOrigin.setFlag(origin, ExpOrigin.LHS), info);
(e2, ty2) := typeExp(eq.rhs, ExpOrigin.setFlag(origin, ExpOrigin.RHS), info);
(e1, e2, ty, mk) := TypeCheck.matchExpressions(e1, ty1, e2, ty2);

if TypeCheck.isIncompatibleMatch(mk) then
Error.addSourceMessage(Error.EQUATION_TYPE_MISMATCH_ERROR,
{Expression.toString(e1) + " = " + Expression.toString(e2),
Type.toString(ty1) + " = " + Type.toString(ty2)}, info);
fail();
end if;
then
Equation.EQUALITY(e1, e2, ty, eq.source);

case Equation.CONNECT()
then typeConnect(eq.lhs, eq.rhs, origin, eq.source);
case Equation.EQUALITY() then typeEqualityEquation(eq.lhs, eq.rhs, origin, eq.source);
case Equation.CONNECT() then typeConnect(eq.lhs, eq.rhs, origin, eq.source);

case Equation.FOR()
algorithm
Expand All @@ -2385,24 +2370,7 @@ algorithm
Equation.FOR(eq.iterator, SOME(e1), body, eq.source);

case Equation.IF() then typeIfEquation(eq.branches, origin, eq.source);

case Equation.WHEN()
algorithm
next_origin := ExpOrigin.setFlag(origin, ExpOrigin.WHEN);

tybrs := list(
match br
case Equation.Branch.BRANCH(condition = cond, body = body)
algorithm
(e1, var) := typeCondition(cond, origin, eq.source,
Error.WHEN_CONDITION_TYPE_ERROR, allowVector = true);
eqs1 := list(typeEquation(beq, next_origin) for beq in body);
then
Equation.makeBranch(e1, eqs1, var);
end match
for br in eq.branches);
then
Equation.WHEN(tybrs, eq.source);
case Equation.WHEN() then typeWhenEquation(eq.branches, origin, eq.source);

case Equation.ASSERT()
algorithm
Expand Down Expand Up @@ -2543,6 +2511,23 @@ algorithm
end match;
end checkConnectorForm;

function checkLhsInWhen
input Expression exp;
output Boolean isValid;
algorithm
isValid := match exp
case Expression.CREF() then true;
case Expression.TUPLE()
algorithm
for e in exp.elements loop
checkLhsInWhen(e);
end for;
then
true;
else false;
end match;
end checkLhsInWhen;

function typeAlgorithm
input output Algorithm alg;
input ExpOrigin.Type origin;
Expand Down Expand Up @@ -2686,34 +2671,61 @@ algorithm
end match;
end typeStatement;

function typeEqualityEquation
input Expression lhsExp;
input Expression rhsExp;
input ExpOrigin.Type origin;
input DAE.ElementSource source;
output Equation eq;
protected
SourceInfo info = ElementSource.getInfo(source);
Expression e1, e2;
Type ty1, ty2, ty;
MatchKind mk;
algorithm
if ExpOrigin.flagSet(origin, ExpOrigin.WHEN) and
ExpOrigin.flagNotSet(origin, ExpOrigin.CLOCKED) then
if checkLhsInWhen(lhsExp) then
Expression.fold(lhsExp, Inst.markStructuralParamsSubs, 0);
else
Error.addSourceMessage(Error.WHEN_EQ_LHS, {Expression.toString(lhsExp)}, info);
fail();
end if;
end if;

(e1, ty1) := typeExp(lhsExp, ExpOrigin.setFlag(origin, ExpOrigin.LHS), info);
(e2, ty2) := typeExp(rhsExp, ExpOrigin.setFlag(origin, ExpOrigin.RHS), info);
(e1, e2, ty, mk) := TypeCheck.matchExpressions(e1, ty1, e2, ty2);

if TypeCheck.isIncompatibleMatch(mk) then
Error.addSourceMessage(Error.EQUATION_TYPE_MISMATCH_ERROR,
{Expression.toString(e1) + " = " + Expression.toString(e2),
Type.toString(ty1) + " = " + Type.toString(ty2)}, info);
fail();
end if;

eq := Equation.EQUALITY(e1, e2, ty, source);
end typeEqualityEquation;

function typeCondition
input output Expression condition;
input ExpOrigin.Type origin;
input DAE.ElementSource source;
input Error.Message errorMsg;
input Boolean allowVector = false;
input Boolean allowClock = false;
output Type ty;
output Variability variability;
protected
Type ty;
MatchKind mk;
SourceInfo info;
Type ety;
algorithm
info := ElementSource.getInfo(source);
(condition, ty, variability) := typeExp(condition, origin, info);

if allowVector and Type.isVector(ty) then
(_, _, mk) := TypeCheck.matchTypes(Type.arrayElementType(ty), Type.BOOLEAN(), condition);
if TypeCheck.isIncompatibleMatch(mk) then
(_, _, mk) := TypeCheck.matchTypes(Type.arrayElementType(ty), Type.CLOCK(), condition);
end if;
else
(_, _, mk) := TypeCheck.matchTypes(ty, Type.BOOLEAN(), condition);
if TypeCheck.isIncompatibleMatch(mk) then
(_, _, mk) := TypeCheck.matchTypes(ty, Type.CLOCK(), condition);
end if;
end if;
ety := if allowVector then Type.arrayElementType(ty) else ty;

if TypeCheck.isIncompatibleMatch(mk) then
if not (Type.isBoolean(ety) or (allowClock and Type.isClock(ety))) then
Error.addSourceMessage(errorMsg,
{Expression.toString(condition), Type.toString(ty)}, info);
fail();
Expand All @@ -2736,7 +2748,7 @@ algorithm
// Type the conditions of all the branches.
for b in branches loop
Equation.Branch.BRANCH(cond, _, eql) := b;
(cond, var) := typeCondition(cond, cond_origin, source, Error.IF_CONDITION_TYPE_ERROR);
(cond, _, var) := typeCondition(cond, cond_origin, source, Error.IF_CONDITION_TYPE_ERROR);

if var > Variability.PARAMETER or isNonExpandableExp(cond) then
// If the condition doesn't fulfill the requirements for allowing
Expand Down Expand Up @@ -2841,6 +2853,45 @@ algorithm
end match;
end isNonConstantIfCondition;

function typeWhenEquation
input list<Equation.Branch> branches;
input ExpOrigin.Type origin;
input DAE.ElementSource source;
output Equation whenEq;
protected
ExpOrigin.Type next_origin = ExpOrigin.setFlag(origin, ExpOrigin.WHEN);
list<Equation.Branch> accum_branches = {};
Expression cond;
list<Equation> body;
Type ty;
Variability var;
algorithm
for branch in branches loop
Equation.Branch.BRANCH(cond, _, body) := branch;
(cond, ty, var) := typeCondition(cond, origin, source,
Error.WHEN_CONDITION_TYPE_ERROR, allowVector = true, allowClock = true);

if Type.isClock(ty) then
if listLength(branches) <> 1 then
if referenceEq(branch, listHead(branches)) then
Error.addSourceMessage(Error.ELSE_WHEN_CLOCK, {}, ElementSource.getInfo(source));
else
Error.addSourceMessage(Error.CLOCKED_WHEN_BRANCH, {}, ElementSource.getInfo(source));
end if;

fail();
else
next_origin := ExpOrigin.setFlag(origin, ExpOrigin.CLOCKED);
end if;
end if;

body := list(typeEquation(eq, next_origin) for eq in body);
accum_branches := Equation.makeBranch(cond, body, var) :: accum_branches;
end for;

whenEq := Equation.WHEN(listReverseInPlace(accum_branches), source);
end typeWhenEquation;

function typeOperatorArg
input output Expression arg;
input Type expectedType;
Expand Down

0 comments on commit ab4e3e6

Please sign in to comment.