Commit 4b21d277 authored by Maxime Perrotin's avatar Maxime Perrotin
Browse files

Added semantic checks on decision answer coverage

parent f37272a2
......@@ -33,7 +33,7 @@ import fnmatch
import logging
import traceback
from itertools import chain, permutations, combinations
from collections import defaultdict
from collections import defaultdict, Counter
import antlr3
import antlr3.tree
......@@ -2960,6 +2960,7 @@ def decision(root, parent, context):
covered_ranges = defaultdict(list)
qmin, qmax = 0, 0
need_else = False
is_enum = False
for ans in dec.answers:
if ans.kind in ('constant', 'open_range'):
expr = ans.openRangeOp()
......@@ -2972,6 +2973,13 @@ def decision(root, parent, context):
ans.constant = expr.right
q_basic = find_basic_type(dec.question.exprType)
a_basic = find_basic_type(ans.constant.exprType)
if q_basic.kind.endswith('EnumeratedType'):
if not ans.constant.is_raw:
# Ref to a variable -> can't guarantee coverage
need_else = True
continue
covered_ranges[ans].append(ans.inputString)
is_enum = True
if not q_basic.kind.startswith('Integer'):
continue
# numeric type -> find the range covered by this answer
......@@ -3082,14 +3090,17 @@ def decision(root, parent, context):
l=a0_val, h=a1_val))
covered_ranges[ans].append((int(float(a0_basic.Min)),
int(float(a1_basic.Max))))
# Check the following:
# Check the following
# (1) no overlap between covered ranges in decision answers
# (2) no gap in the coverage of the decision possible values
# (3) ELSE branch, if present, can be reached
# (4) if an answer uses a non-ground expression an ELSE is there
# (5) present() operator and enumerated question are fully covered
q_ranges = [(qmin, qmax)] if is_numeric(dec.question.exprType) else []
for each in combinations(covered_ranges.viewitems(), 2):
if not q_ranges:
continue
for comb in combinations(
chain.from_iterable(val[1] for val in each), 2):
comb_overlap = (max(comb[0][0], comb[1][0]),
......@@ -3104,9 +3115,10 @@ def decision(root, parent, context):
o1=comb_overlap[0],
o2=comb_overlap[1]))
new_q_ranges = []
# for minq, maxq in q_ranges:
# (2) Check that decision range is fully covered
for ans_ref, ranges in covered_ranges.viewitems():
if is_enum:
continue
for mina, maxa in ranges:
for minq, maxq in q_ranges:
left = (minq, min(maxq, mina - 1))
......@@ -3134,6 +3146,21 @@ def decision(root, parent, context):
warnings.append('Decision "{}": Missing ELSE branch'
.format(dec.inputString))
# (5) check coverage of enumerated types
if is_enum:
# check duplicate answers
answers = list(chain.from_iterable(covered_ranges.viewvalues()))
dupl = [a for a, v in Counter(answers).items() if v > 1]
if dupl:
errors.append('Decision "{}": duplicate answers "{}"'
.format(dec.inputString, '", "'.join(dupl)))
enumerants = [en.replace('-', '_') for en in q_basic.EnumValues.keys()]
# check for missing answers
if set(answers) != set(enumerants) and not has_else:
errors.append('Decision "{}": Missing branches for answer(s) "{}"'
.format(dec.inputString,
'", "'.join(set(enumerants) - set(answers))))
return dec, errors, warnings
......
......@@ -10,7 +10,7 @@ test-parse:
../../../opengeode.py myfunction.pr system_structure.pr --check
test-ada:
../../../opengeode.py --toAda myfunction.pr system_structure.pr 2>&1 | diff expected - || exit 0
../../../opengeode.py --toAda myfunction.pr system_structure.pr 2>&1 | sort | diff expected - || exit 0
coverage:
coverage run -p ../../../opengeode.py myfunction.pr system_structure.pr --toAda
......
[ERROR] Decision "var1": answers -500:500 and /=1 are overlapping in range [-500 .. 0]
[ERROR] Decision "var1": answers -500:500 and /=1 are overlapping in range [2 .. 500]
[ERROR] Decision "var1": answers -500:500 and =0 are overlapping in range [0 .. 0]
[ERROR] Decision "var1": answers -500:500 and >0 are overlapping in range [1 .. 500]
[ERROR] Decision "var1": answers =0 and /=1 are overlapping in range [0 .. 0]
[ERROR] Decision "var1": answers >0 and /=1 are overlapping in range [2 .. 2147483647]
[ERROR] Decision "var2": No answer to cover range [0 .. 255]
[ERROR] Decision "var3": No answer to cover range [50 .. 50]
[ERROR] Decision "var3": answers /=50 and 10:20 are overlapping in range [10 .. 20]
[ERROR] Too many errors, cannot generate code
[INFO] Checking ['myfunction.pr', 'system_structure.pr']
[INFO] Parsing complete. Summary, found 6 warnings and 6 errors
[WARNING] Decision "var2": Unreachable branch "<0"
[WARNING] Decision "var2": Unreachable branch ">300"
[INFO] Parsing complete. Summary, found 6 warnings and 9 errors
[WARNING] Decision "var2": Range [-10 .. -1] is unreachable
[WARNING] Decision "var2": Unreachable branch
[WARNING] Decision "var2": Range [256 .. 300] is unreachable
[WARNING] Decision "var2": Unreachable branch
[ERROR] Non-determinism in decision "var1": answers -500:500 and >0 are overlapping in range [1 .. 500]
[ERROR] Non-determinism in decision "var1": answers -500:500 and /=1 are overlapping in range [-500 .. 0]
[ERROR] Non-determinism in decision "var1": answers -500:500 and /=1 are overlapping in range [2 .. 500]
[ERROR] Non-determinism in decision "var1": answers -500:500 and =0 are overlapping in range [0 .. 0]
[ERROR] Non-determinism in decision "var1": answers >0 and /=1 are overlapping in range [2 .. 2147483647]
[ERROR] Non-determinism in decision "var1": answers /=1 and =0 are overlapping in range [0 .. 0]
[ERROR] Too many errors, cannot generate code
[WARNING] Decision "var2": Unreachable branch "<0"
[WARNING] Decision "var2": Unreachable branch ">300"
[WARNING] Decision "var2": Unreachable branch -10:-5
[WARNING] Decision "var2": Unreachable branch 256:300
/* CIF PROCESS (200, 143), (150, 75) */
PROCESS myfunction;
/* CIF TEXT (0, 142), (282, 128) */
/* CIF TEXT (36, 43), (360, 41) */
-- Test the branch coverage checker in decision answers
/* CIF ENDTEXT */
/* CIF TEXT (0, 142), (282, 152) */
dcl var1 t_Int32 := 0;
dcl var2 t_uint8 := 0;
dcl var3 t_uInt8 := 0;
dcl var4 mychoice := a: false;
dcl var5 myenum := hello;
/* CIF ENDTEXT */
/* CIF TEXT (36, 43), (360, 41) */
-- Test the branch coverage checker in decision answers
/* CIF ENDTEXT */
/* CIF START (243, 292), (70, 35) */
/* CIF START (439, 292), (70, 35) */
START;
/* CIF DECISION (243, 342), (70, 50) */
/* CIF DECISION (439, 342), (70, 50) */
DECISION var1
/* CIF COMMENT (333, 349), (191, 35) */
/* CIF COMMENT (529, 349), (191, 35) */
COMMENT 'Check range overlapping';
/* CIF ANSWER (96, 412), (90, 24) */
/* CIF ANSWER (289, 412), (90, 24) */
(-500:500):
/* CIF ANSWER (198, 412), (70, 24) */
/* CIF ANSWER (394, 412), (70, 24) */
(=0):
/* CIF ANSWER (288, 412), (70, 24) */
/* CIF ANSWER (484, 412), (70, 24) */
(/=1):
/* CIF ANSWER (378, 412), (70, 24) */
/* CIF ANSWER (574, 412), (70, 24) */
(>0):
ENDDECISION;
/* CIF DECISION (243, 470), (70, 50) */
/* CIF DECISION (439, 490), (70, 50) */
DECISION var2
/* CIF COMMENT (333, 477), (241, 35) */
/* CIF COMMENT (529, 497), (241, 35) */
COMMENT 'Check unreachable branch check';
/* CIF ANSWER (115, 540), (53, 33) */
/* CIF ANSWER (308, 560), (53, 33) */
(<0):
/* CIF ANSWER (197, 540), (68, 33) */
/* CIF ANSWER (390, 560), (68, 33) */
(>300):
/* CIF ANSWER (286, 540), (72, 33) */
/* CIF ANSWER (482, 560), (72, 33) */
(-10:-5):
/* CIF ANSWER (369, 540), (86, 24) */
/* CIF ANSWER (561, 560), (86, 24) */
(256:300):
ENDDECISION;
/* CIF DECISION (242, 602), (71, 50) */
/* CIF DECISION (438, 622), (71, 50) */
DECISION var3;
/* CIF ANSWER (196, 672), (71, 24) */
/* CIF ANSWER (389, 692), (71, 24) */
(10:20):
/* CIF ANSWER (288, 672), (70, 24) */
/* CIF ANSWER (484, 692), (70, 24) */
(/=50):
ENDDECISION;
/* CIF NEXTSTATE (243, 716), (70, 35) */
/* CIF DECISION (412, 746), (123, 50) */
DECISION present(var4)
/* CIF COMMENT (555, 753), (252, 35) */
COMMENT 'Check coverage of CHOICE answers';
/* CIF ANSWER (441, 816), (66, 34) */
(a):
ENDDECISION;
/* CIF DECISION (437, 880), (74, 50) */
DECISION var5
/* CIF COMMENT (525, 878), (241, 50) */
COMMENT 'Check duplicates and
coverage of ENUMERATED values';
/* CIF ANSWER (304, 950), (70, 24) */
(hello):
/* CIF ANSWER (389, 950), (72, 24) */
(world):
/* CIF ANSWER (481, 950), (72, 24) */
(world):
/* CIF ANSWER (575, 950), (70, 24) */
(hello):
ENDDECISION;
/* CIF DECISION (439, 989), (70, 50) */
DECISION var5
/* CIF COMMENT (529, 996), (224, 35) */
COMMENT 'should be no error due to ELSE';
/* CIF ANSWER (331, 1059), (105, 24) */
(howareyou):
/* CIF ANSWER (522, 1059), (70, 24) */
else:
ENDDECISION;
/* CIF NEXTSTATE (439, 1098), (70, 35) */
NEXTSTATE wait;
/* CIF STATE (868, 313), (70, 35) */
STATE wait;
......
all: test-ada
edit:
../../../opengeode.py orchestrator.pr system_structure.pr
test-parse:
../../../opengeode.py orchestrator.pr system_structure.pr --check
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment