Commit 693b85a3 authored by Maxime Perrotin's avatar Maxime Perrotin
Browse files

Added branch overlap checks

parent 9e516599
......@@ -32,7 +32,8 @@ import re
import fnmatch
import logging
import traceback
from itertools import chain, permutations
from itertools import chain, permutations, combinations
from collections import defaultdict
import antlr3
import antlr3.tree
......@@ -2956,7 +2957,7 @@ def decision(root, parent, context):
warnings.append(['Unsupported DECISION child type: ' +
str(child.type), [dec.pos_x, dec.pos_y]])
# Make type checks to be sure that question and answers are compatible
covered_ranges = []
covered_ranges = defaultdict(list)
need_else = False
for ans in dec.answers:
if ans.kind in ('constant', 'open_range'):
......@@ -2977,54 +2978,54 @@ def decision(root, parent, context):
# Not a constant or a raw number, range is not fix
need_else = True
continue
val_a = int(a_basic.Min)
val_a = int(float(a_basic.Min))
qmin, qmax = int(float(q_basic.Min)), int(float(q_basic.Max))
# Check the operator to compute the range
reachable = True
if ans.openRangeOp == ogAST.ExprLe:
if qmin <= val_a:
covered_ranges.append([qmin, val_a])
covered_ranges[ans].append((qmin, val_a))
else:
warnings.append('Unreachable branch - '
+ ans.inputString)
reachable = False
elif ans.openRangeOp == ogAST.ExprLt:
if qmin < val_a:
covered_ranges.append([qmin, val_a - 1])
covered_ranges[ans].append((qmin, val_a - 1))
else:
warnings.append('Unreachable branch - '
+ ans.inputString)
reachable = False
elif ans.openRangeOp == ogAST.ExprGt:
if qmax > val_a:
covered_ranges.append([val_a + 1, qmax])
covered_ranges[ans].append((val_a + 1, qmax))
else:
warnings.append('Unreachable branch - '
+ ans.inputString)
reachable = False
elif ans.openRangeOp == ogAST.ExprGe:
if qmax >= val_a:
covered_ranges.append([val_a, qmax])
covered_ranges[ans].append((val_a, qmax))
else:
warnings.append('Unreachable branch - '
+ ans.inputString)
reachable = False
elif ans.openRangeOp == ogAST.ExprEq:
if qmin <= val_a <= qmax:
covered_ranges.append([val_a, val_a])
covered_ranges[ans].append((val_a, val_a))
else:
warnings.append('Unreachable branch - '
+ ans.inputString)
reachable = False
elif ans.openRangeOp == ogAST.ExprNeq:
if qmin == val_a:
covered_ranges.append([qmin + 1, qmax])
covered_ranges[ans].append((qmin + 1, qmax))
elif qmax == val_a:
covered_ranges.append([qmin, qmax - 1])
elif q_basic.Min < a_basic.Max < q_basic.Max:
covered_ranges.append([q_basic.Min, a_basic.Max - 1])
covered_ranges.append([a_basic.Max + 1, q_basic.Max])
covered_ranges[ans].append((qmin, qmax - 1))
elif qmin < val_a < qmax:
covered_ranges[ans].append((qmin, val_a - 1))
covered_ranges[ans].append((val_a + 1, qmax))
else:
warnings.append('Condition is always true: {} /= {}'
.format(dec.inputString,
ans.inputString))
else:
warnings.append('Unsupported range expression')
print 'RANGE OF QUESTION: [{} .. {}]'.format(qmin, qmax)
if not reachable:
warnings.append('Decision "{}": '
'Unreachable branch "{}"'
.format(dec.inputString,
ans.inputString))
except (AttributeError, TypeError) as err:
errors.append('Types are incompatible in DECISION: '
'question (' + expr.left.inputString + ', type= ' +
......@@ -3060,12 +3061,46 @@ def decision(root, parent, context):
# Not a constant or a raw number, range is not fix
need_else = True
continue
covered_ranges.append([int(float(a0_basic.Min)),
int(float(a1_basic.Max))])
for each in covered_ranges:
print each
if need_else and not has_else:
warnings.append('Missing ELSE branch in decision')
qmin, qmax = int(float(q_basic.Min)), int(float(q_basic.Max))
a0_val = int(float(a0_basic.Min))
a1_val = int(float(a1_basic.Max))
if a0_val < qmin:
warnings.append('Decision "{dec}": '
'Range [{a0} .. {qmin}] is unreachable'
.format(a0=a0_val, qmin=qmin - 1,
dec=dec.inputString))
if a1_val > qmax:
warnings.append('Decision "{dec}": '
'Range [{qmax} .. {a1}] is unreachable'
.format(qmax=qmax + 1, a1=a1_val,
dec=dec.inputString))
if (a0_val < qmin and a1_val < qmin) or (a0_val > qmax and
a1_val > qmax):
warnings.append('Decision "{dec}": Unreachable branch'
.format(dec=dec.inputString))
covered_ranges[ans].append((int(float(a0_basic.Min)),
int(float(a1_basic.Max))))
# 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
for each in combinations(covered_ranges.viewitems(), 2):
for comb in combinations(
chain.from_iterable(val[1] for val in each), 2):
comb_overlap = (max(comb[0][0], comb[1][0]),
min(comb[0][1], comb[1][1]))
if comb_overlap[0] <= comb_overlap[1]:
errors.append('Non-determinism in decision "{d}": '
'answers {a1} and {a2} '
'are overlapping in range [{o1} .. {o2}]'
.format(d=dec.inputString,
a1=each[0][0].inputString,
a2=each[1][0].inputString,
o1=comb_overlap[0],
o2=comb_overlap[1]))
if need_else and not has_else:
warnings.append('Missing ELSE branch in decision {}'
.format(dec.inputString))
return dec, errors, warnings
......
all: test-ada
edit:
../../../opengeode.py myfunction.pr system_structure.pr
check:
../../../opengeode.py myfunction.pr system_structure.pr --check
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
coverage:
coverage run -p ../../../opengeode.py myfunction.pr system_structure.pr --toAda
clean:
rm -rf *.adb *.ads *.pyc runSpark.sh spark.idx *.o *.ali gnat.cfg examiner bin *.wrn *.gpr datav*.? ber.c xer.c asn1crt.? acn.c real.c testcase
TASTE-BasicTypes DEFINITIONS ::=
BEGIN
-- Set of TASTE predefined basic types
T-Int32 ::= INTEGER (-2147483648 .. 2147483647)
T-UInt32 ::= INTEGER (0 .. 4294967295)
T-Int8 ::= INTEGER (-128 .. 127)
T-UInt8 ::= INTEGER (0 .. 255)
T-Boolean ::= BOOLEAN
END
TASTE-Dataview DEFINITIONS ::=
BEGIN
IMPORTS T-Int32, T-UInt32, T-Int8, T-UInt8, T-Boolean FROM TASTE-BasicTypes;
-- A few simple types to start with ASN.1
MyInteger ::= T-UInt8
MyReal ::= REAL (0.0 .. 1000.0)
LargerReal ::= REAL (0.0 .. 1000000000)
MyEnum ::= ENUMERATED { hello(12), world(13), howareyou(111) }
MySeq ::= SEQUENCE {
a MyInteger,
b ENUMERATED { taste(1), welcomes(2), you(3) }
}
MyChoice ::= CHOICE {
a BOOLEAN,
b MySeq
}
MySeqOf ::= SEQUENCE (SIZE (2)) OF MyEnum
SeqInt ::= SEQUENCE (SIZE(1..2)) OF T-UInt8
SeqBool ::= SEQUENCE (SIZE(2)) OF BOOLEAN
SeqBool2 ::= SEQUENCE (SIZE(1..2)) OF BOOLEAN
MyOctStr ::= OCTET STRING (SIZE (3))
String ::= OCTET STRING (SIZE(0..100))
-- You can also declare variables (they will be visible in C, Ada and SDL)
myVar MySeqOf ::= { hello, world }
END
[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"
[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
/* CIF PROCESS (200, 143), (150, 75) */
PROCESS myfunction;
/* CIF TEXT (0, 142), (282, 128) */
dcl var1 t_Int32 := 0;
dcl var2 t_uint8 := 0;
/* CIF ENDTEXT */
/* CIF TEXT (36, 43), (360, 41) */
-- Test the branch coverage checker in decision answers
/* CIF ENDTEXT */
/* CIF START (243, 292), (70, 35) */
START;
/* CIF DECISION (243, 342), (70, 50) */
DECISION var1
/* CIF COMMENT (333, 349), (191, 35) */
COMMENT 'Check range overlapping';
/* CIF ANSWER (99, 412), (88, 23) */
(-500:500):
/* CIF ANSWER (198, 412), (70, 23) */
(=0):
/* CIF ANSWER (288, 412), (70, 23) */
(/=1):
/* CIF ANSWER (378, 412), (70, 23) */
(>0):
ENDDECISION;
/* CIF DECISION (243, 460), (70, 50) */
DECISION var2
/* CIF COMMENT (333, 467), (241, 35) */
COMMENT 'Check unreachable branch check';
/* CIF ANSWER (117, 530), (52, 33) */
(<0):
/* CIF ANSWER (200, 530), (66, 33) */
(>300):
/* CIF ANSWER (286, 530), (72, 33) */
(-10:-5):
/* CIF ANSWER (372, 530), (83, 23) */
(256:300):
ENDDECISION;
/* CIF NEXTSTATE (243, 588), (70, 35) */
NEXTSTATE wait;
/* CIF STATE (868, 313), (70, 35) */
STATE wait;
ENDSTATE;
ENDPROCESS myfunction;
\ No newline at end of file
/* CIF PROCESS (200, 143), (150, 75) */
PROCESS myfunction;
/* CIF TEXT (0, 142), (282, 128) */
dcl var1 t_Int32 := 0;
dcl var2 t_uint8 := 0;
/* CIF ENDTEXT */
/* CIF TEXT (36, 43), (360, 41) */
-- Test the branch coverage checker in decision answers
/* CIF ENDTEXT */
/* CIF START (243, 292), (70, 35) */
START;
/* CIF DECISION (243, 342), (70, 50) */
DECISION var1
/* CIF COMMENT (333, 349), (191, 35) */
COMMENT 'Check range overlapping';
/* CIF ANSWER (99, 412), (88, 23) */
(-500:500):
/* CIF ANSWER (198, 412), (70, 23) */
(=0):
/* CIF ANSWER (288, 412), (70, 23) */
(/=1):
/* CIF ANSWER (378, 412), (70, 23) */
(>0):
ENDDECISION;
/* CIF DECISION (243, 460), (70, 50) */
DECISION var2
/* CIF COMMENT (333, 467), (241, 35) */
COMMENT 'Check unreachable branch check';
/* CIF ANSWER (117, 530), (52, 33) */
(<0):
/* CIF ANSWER (200, 530), (66, 33) */
(>300):
/* CIF ANSWER (286, 530), (72, 33) */
(-10:-5):
/* CIF ANSWER (372, 530), (83, 23) */
(256:300):
ENDDECISION;
/* CIF NEXTSTATE (243, 588), (70, 35) */
NEXTSTATE wait;
/* CIF STATE (868, 313), (70, 35) */
STATE wait;
ENDSTATE;
ENDPROCESS myfunction;
\ No newline at end of file
/* CIF Keep Specific Geode ASNFilename 'dataview-uniq.asn' */
USE Datamodel;
SYSTEM myfunction;
/* CIF Keep Specific Geode PARAMNAMES tutu */
SIGNAL start_something (T_Int32);
/* CIF Keep Specific Geode PARAMNAMES titi */
SIGNAL result_data (T_Int32);
CHANNEL c
FROM ENV TO myfunction WITH start_something;
FROM myfunction TO ENV WITH result_data;
ENDCHANNEL;
BLOCK myfunction;
SIGNALROUTE r
FROM ENV TO myfunction WITH start_something;
FROM myfunction TO ENV WITH result_data;
CONNECT c and r;
PROCESS myfunction REFERENCED;
ENDBLOCK;
ENDSYSTEM;
\ No newline at end of file
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