Skip to content
This repository was archived by the owner on May 18, 2019. It is now read-only.

Commit ab4e3e6

Browse files
perostOpenModelica-Hudson
perost
authored and
OpenModelica-Hudson
committed
[NF] Improve error checking of when-clauses.
- 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]: - #3001 - OpenModelica/OpenModelica-testsuite#1148
1 parent e3fab53 commit ab4e3e6

File tree

8 files changed

+347
-87
lines changed

8 files changed

+347
-87
lines changed

‎Compiler/NFFrontEnd/NFExpression.mo‎

Lines changed: 30 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -133,27 +133,45 @@ public
133133
ock := match ick
134134
local
135135
Expression i, ic, r, c, si, sm;
136-
case (INFERRED_CLOCK()) then DAE.INFERRED_CLOCK();
137-
case (INTEGER_CLOCK(i, r)) then DAE.INTEGER_CLOCK(Expression.toDAE(i), Expression.toDAE(r));
138-
case (REAL_CLOCK(i)) then DAE.REAL_CLOCK(Expression.toDAE(i));
139-
case (BOOLEAN_CLOCK(c, si)) then DAE.BOOLEAN_CLOCK(Expression.toDAE(c), Expression.toDAE(si));
140-
case (SOLVER_CLOCK(c, sm)) then DAE.SOLVER_CLOCK(Expression.toDAE(c), Expression.toDAE(sm));
136+
case INFERRED_CLOCK() then DAE.INFERRED_CLOCK();
137+
case INTEGER_CLOCK(i, r) then DAE.INTEGER_CLOCK(Expression.toDAE(i), Expression.toDAE(r));
138+
case REAL_CLOCK(i) then DAE.REAL_CLOCK(Expression.toDAE(i));
139+
case BOOLEAN_CLOCK(c, si) then DAE.BOOLEAN_CLOCK(Expression.toDAE(c), Expression.toDAE(si));
140+
case SOLVER_CLOCK(c, sm) then DAE.SOLVER_CLOCK(Expression.toDAE(c), Expression.toDAE(sm));
141141
end match;
142142
end toDAE;
143143

144-
function toString
144+
function toDebugString
145145
input ClockKind ick;
146146
output String ock;
147147
algorithm
148148
ock := match ick
149149
local
150150
Expression i, ic, r, c, si, sm;
151-
case (INFERRED_CLOCK()) then "INFERRED_CLOCK()";
152-
case (INTEGER_CLOCK(i, r)) then "INTEGER_CLOCK(" + Expression.toString(i) + ", " + Expression.toString(r) + ")";
153-
case (REAL_CLOCK(i)) then "REAL_CLOCK(" + Expression.toString(i) + ")";
154-
case (BOOLEAN_CLOCK(c, si)) then "BOOLEAN_CLOCK(" + Expression.toString(c) + ", " + Expression.toString(si) + ")";
155-
case (SOLVER_CLOCK(c, sm)) then "SOLVER_CLOCK(" + Expression.toString(c) + ", " + Expression.toString(sm) + ")";
151+
case INFERRED_CLOCK() then "INFERRED_CLOCK()";
152+
case INTEGER_CLOCK(i, r) then "INTEGER_CLOCK(" + Expression.toString(i) + ", " + Expression.toString(r) + ")";
153+
case REAL_CLOCK(i) then "REAL_CLOCK(" + Expression.toString(i) + ")";
154+
case BOOLEAN_CLOCK(c, si) then "BOOLEAN_CLOCK(" + Expression.toString(c) + ", " + Expression.toString(si) + ")";
155+
case SOLVER_CLOCK(c, sm) then "SOLVER_CLOCK(" + Expression.toString(c) + ", " + Expression.toString(sm) + ")";
156+
end match;
157+
end toDebugString;
158+
159+
function toString
160+
input ClockKind ck;
161+
output String str;
162+
algorithm
163+
str := match ck
164+
local
165+
Expression e1, e2;
166+
167+
case INFERRED_CLOCK() then "";
168+
case INTEGER_CLOCK(e1, e2) then Expression.toString(e1) + ", " + Expression.toString(e2);
169+
case REAL_CLOCK(e1) then Expression.toString(e1);
170+
case BOOLEAN_CLOCK(e1, e2) then Expression.toString(e1) + ", " + Expression.toString(e2);
171+
case SOLVER_CLOCK(e1, e2) then Expression.toString(e1) + ", " + Expression.toString(e2);
156172
end match;
173+
174+
str := "Clock(" + str + ")";
157175
end toString;
158176
end ClockKind;
159177

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

1483-
case CLKCONST(clk) then "CLKCONST(" + ClockKind.toString(clk) + ")";
1501+
case CLKCONST(clk) then ClockKind.toString(clk);
14841502

14851503
case CREF() then ComponentRef.toString(exp.cref);
14861504
case TYPENAME() then Type.typenameString(Type.arrayElementType(exp.ty));

‎Compiler/NFFrontEnd/NFInst.mo‎

Lines changed: 4 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -100,6 +100,7 @@ import Record = NFRecord;
100100
import Variable = NFVariable;
101101
import OperatorOverloading = NFOperatorOverloading;
102102
import EvalConstants = NFEvalConstants;
103+
import VerifyModel = NFVerifyModel;
103104

104105
public
105106
function instClassInProgram
@@ -160,6 +161,8 @@ algorithm
160161
flat_model := SimplifyModel.simplify(flat_model);
161162
funcs := Flatten.collectFunctions(flat_model, name);
162163

164+
VerifyModel.verify(flat_model);
165+
163166
// Collect package constants that couldn't be substituted with their values
164167
// (e.g. because they where used with non-constant subscripts), and add them
165168
// to the model.
@@ -2738,11 +2741,6 @@ algorithm
27382741
algorithm
27392742
exp1 := instExp(scodeEq.expLeft, scope, info);
27402743
exp2 := instExp(scodeEq.expRight, scope, info);
2741-
2742-
if ExpOrigin.flagSet(origin, ExpOrigin.WHEN) and not checkLhsInWhen(exp1) then
2743-
Error.addSourceMessage(Error.WHEN_EQ_LHS, {Expression.toString(exp1)}, info);
2744-
fail();
2745-
end if;
27462744
then
27472745
Equation.EQUALITY(exp1, exp2, Type.UNKNOWN(), makeSource(scodeEq.comment, info));
27482746

@@ -3052,23 +3050,6 @@ algorithm
30523050
scope := InstNode.addIterator(iterator, scope);
30533051
end addIteratorToScope;
30543052

3055-
function checkLhsInWhen
3056-
input Expression exp;
3057-
output Boolean isValid;
3058-
algorithm
3059-
isValid := match exp
3060-
case Expression.CREF() then true;
3061-
case Expression.TUPLE()
3062-
algorithm
3063-
for e in exp.elements loop
3064-
checkLhsInWhen(e);
3065-
end for;
3066-
then
3067-
true;
3068-
else false;
3069-
end match;
3070-
end checkLhsInWhen;
3071-
30723053
function insertGeneratedInners
30733054
"Inner elements can be generated automatically during instantiation if they're
30743055
missing, and are stored in the cache of the top scope since that's easily
@@ -3144,7 +3125,7 @@ algorithm
31443125
algorithm
31453126
for c in cls_tree.components loop
31463127
if not InstNode.isEmpty(c) then
3147-
updateImplicitVariabilityComp(c, evalAllParams);
3128+
updateImplicitVariabilityComp(c, evalAllParams);
31483129
end if;
31493130
end for;
31503131

‎Compiler/NFFrontEnd/NFType.mo‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -237,6 +237,16 @@ public
237237
end match;
238238
end isString;
239239

240+
function isClock
241+
input Type ty;
242+
output Boolean isClock;
243+
algorithm
244+
isClock := match ty
245+
case CLOCK() then true;
246+
else false;
247+
end match;
248+
end isClock;
249+
240250
function isScalar
241251
input Type ty;
242252
output Boolean isScalar;

‎Compiler/NFFrontEnd/NFTyping.mo‎

Lines changed: 102 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -136,6 +136,7 @@ package ExpOrigin
136136
constant Type CONNECT = intBitLShift(1, 17); // Part of connect argument.
137137
constant Type NOEVENT = intBitLShift(1, 18); // Part of noEvent argument.
138138
constant Type ASSERT = intBitLShift(1, 19); // Part of assert argument.
139+
constant Type CLOCKED = intBitLShift(1, 20); // Part of a clocked equation.
139140

140141
// Combined flags:
141142
constant Type EQ_SUBEXPRESSION = intBitOr(EQUATION, SUBEXPRESSION);
@@ -2348,24 +2349,8 @@ algorithm
23482349
Integer next_origin;
23492350
SourceInfo info;
23502351

2351-
case Equation.EQUALITY()
2352-
algorithm
2353-
info := ElementSource.getInfo(eq.source);
2354-
(e1, ty1) := typeExp(eq.lhs, ExpOrigin.setFlag(origin, ExpOrigin.LHS), info);
2355-
(e2, ty2) := typeExp(eq.rhs, ExpOrigin.setFlag(origin, ExpOrigin.RHS), info);
2356-
(e1, e2, ty, mk) := TypeCheck.matchExpressions(e1, ty1, e2, ty2);
2357-
2358-
if TypeCheck.isIncompatibleMatch(mk) then
2359-
Error.addSourceMessage(Error.EQUATION_TYPE_MISMATCH_ERROR,
2360-
{Expression.toString(e1) + " = " + Expression.toString(e2),
2361-
Type.toString(ty1) + " = " + Type.toString(ty2)}, info);
2362-
fail();
2363-
end if;
2364-
then
2365-
Equation.EQUALITY(e1, e2, ty, eq.source);
2366-
2367-
case Equation.CONNECT()
2368-
then typeConnect(eq.lhs, eq.rhs, origin, eq.source);
2352+
case Equation.EQUALITY() then typeEqualityEquation(eq.lhs, eq.rhs, origin, eq.source);
2353+
case Equation.CONNECT() then typeConnect(eq.lhs, eq.rhs, origin, eq.source);
23692354

23702355
case Equation.FOR()
23712356
algorithm
@@ -2385,24 +2370,7 @@ algorithm
23852370
Equation.FOR(eq.iterator, SOME(e1), body, eq.source);
23862371

23872372
case Equation.IF() then typeIfEquation(eq.branches, origin, eq.source);
2388-
2389-
case Equation.WHEN()
2390-
algorithm
2391-
next_origin := ExpOrigin.setFlag(origin, ExpOrigin.WHEN);
2392-
2393-
tybrs := list(
2394-
match br
2395-
case Equation.Branch.BRANCH(condition = cond, body = body)
2396-
algorithm
2397-
(e1, var) := typeCondition(cond, origin, eq.source,
2398-
Error.WHEN_CONDITION_TYPE_ERROR, allowVector = true);
2399-
eqs1 := list(typeEquation(beq, next_origin) for beq in body);
2400-
then
2401-
Equation.makeBranch(e1, eqs1, var);
2402-
end match
2403-
for br in eq.branches);
2404-
then
2405-
Equation.WHEN(tybrs, eq.source);
2373+
case Equation.WHEN() then typeWhenEquation(eq.branches, origin, eq.source);
24062374

24072375
case Equation.ASSERT()
24082376
algorithm
@@ -2543,6 +2511,23 @@ algorithm
25432511
end match;
25442512
end checkConnectorForm;
25452513

2514+
function checkLhsInWhen
2515+
input Expression exp;
2516+
output Boolean isValid;
2517+
algorithm
2518+
isValid := match exp
2519+
case Expression.CREF() then true;
2520+
case Expression.TUPLE()
2521+
algorithm
2522+
for e in exp.elements loop
2523+
checkLhsInWhen(e);
2524+
end for;
2525+
then
2526+
true;
2527+
else false;
2528+
end match;
2529+
end checkLhsInWhen;
2530+
25462531
function typeAlgorithm
25472532
input output Algorithm alg;
25482533
input ExpOrigin.Type origin;
@@ -2686,34 +2671,61 @@ algorithm
26862671
end match;
26872672
end typeStatement;
26882673

2674+
function typeEqualityEquation
2675+
input Expression lhsExp;
2676+
input Expression rhsExp;
2677+
input ExpOrigin.Type origin;
2678+
input DAE.ElementSource source;
2679+
output Equation eq;
2680+
protected
2681+
SourceInfo info = ElementSource.getInfo(source);
2682+
Expression e1, e2;
2683+
Type ty1, ty2, ty;
2684+
MatchKind mk;
2685+
algorithm
2686+
if ExpOrigin.flagSet(origin, ExpOrigin.WHEN) and
2687+
ExpOrigin.flagNotSet(origin, ExpOrigin.CLOCKED) then
2688+
if checkLhsInWhen(lhsExp) then
2689+
Expression.fold(lhsExp, Inst.markStructuralParamsSubs, 0);
2690+
else
2691+
Error.addSourceMessage(Error.WHEN_EQ_LHS, {Expression.toString(lhsExp)}, info);
2692+
fail();
2693+
end if;
2694+
end if;
2695+
2696+
(e1, ty1) := typeExp(lhsExp, ExpOrigin.setFlag(origin, ExpOrigin.LHS), info);
2697+
(e2, ty2) := typeExp(rhsExp, ExpOrigin.setFlag(origin, ExpOrigin.RHS), info);
2698+
(e1, e2, ty, mk) := TypeCheck.matchExpressions(e1, ty1, e2, ty2);
2699+
2700+
if TypeCheck.isIncompatibleMatch(mk) then
2701+
Error.addSourceMessage(Error.EQUATION_TYPE_MISMATCH_ERROR,
2702+
{Expression.toString(e1) + " = " + Expression.toString(e2),
2703+
Type.toString(ty1) + " = " + Type.toString(ty2)}, info);
2704+
fail();
2705+
end if;
2706+
2707+
eq := Equation.EQUALITY(e1, e2, ty, source);
2708+
end typeEqualityEquation;
2709+
26892710
function typeCondition
26902711
input output Expression condition;
26912712
input ExpOrigin.Type origin;
26922713
input DAE.ElementSource source;
26932714
input Error.Message errorMsg;
26942715
input Boolean allowVector = false;
2716+
input Boolean allowClock = false;
2717+
output Type ty;
26952718
output Variability variability;
26962719
protected
2697-
Type ty;
2698-
MatchKind mk;
26992720
SourceInfo info;
2721+
Type ety;
27002722
algorithm
27012723
info := ElementSource.getInfo(source);
27022724
(condition, ty, variability) := typeExp(condition, origin, info);
27032725

2704-
if allowVector and Type.isVector(ty) then
2705-
(_, _, mk) := TypeCheck.matchTypes(Type.arrayElementType(ty), Type.BOOLEAN(), condition);
2706-
if TypeCheck.isIncompatibleMatch(mk) then
2707-
(_, _, mk) := TypeCheck.matchTypes(Type.arrayElementType(ty), Type.CLOCK(), condition);
2708-
end if;
2709-
else
2710-
(_, _, mk) := TypeCheck.matchTypes(ty, Type.BOOLEAN(), condition);
2711-
if TypeCheck.isIncompatibleMatch(mk) then
2712-
(_, _, mk) := TypeCheck.matchTypes(ty, Type.CLOCK(), condition);
2713-
end if;
2714-
end if;
2726+
ety := if allowVector then Type.arrayElementType(ty) else ty;
27152727

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

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

2856+
function typeWhenEquation
2857+
input list<Equation.Branch> branches;
2858+
input ExpOrigin.Type origin;
2859+
input DAE.ElementSource source;
2860+
output Equation whenEq;
2861+
protected
2862+
ExpOrigin.Type next_origin = ExpOrigin.setFlag(origin, ExpOrigin.WHEN);
2863+
list<Equation.Branch> accum_branches = {};
2864+
Expression cond;
2865+
list<Equation> body;
2866+
Type ty;
2867+
Variability var;
2868+
algorithm
2869+
for branch in branches loop
2870+
Equation.Branch.BRANCH(cond, _, body) := branch;
2871+
(cond, ty, var) := typeCondition(cond, origin, source,
2872+
Error.WHEN_CONDITION_TYPE_ERROR, allowVector = true, allowClock = true);
2873+
2874+
if Type.isClock(ty) then
2875+
if listLength(branches) <> 1 then
2876+
if referenceEq(branch, listHead(branches)) then
2877+
Error.addSourceMessage(Error.ELSE_WHEN_CLOCK, {}, ElementSource.getInfo(source));
2878+
else
2879+
Error.addSourceMessage(Error.CLOCKED_WHEN_BRANCH, {}, ElementSource.getInfo(source));
2880+
end if;
2881+
2882+
fail();
2883+
else
2884+
next_origin := ExpOrigin.setFlag(origin, ExpOrigin.CLOCKED);
2885+
end if;
2886+
end if;
2887+
2888+
body := list(typeEquation(eq, next_origin) for eq in body);
2889+
accum_branches := Equation.makeBranch(cond, body, var) :: accum_branches;
2890+
end for;
2891+
2892+
whenEq := Equation.WHEN(listReverseInPlace(accum_branches), source);
2893+
end typeWhenEquation;
2894+
28442895
function typeOperatorArg
28452896
input output Expression arg;
28462897
input Type expectedType;

0 commit comments

Comments
 (0)