Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Spot
divine-ltsmin-deb
Commits
bfe1dd38
Commit
bfe1dd38
authored
Mar 09, 2020
by
Etienne Renault
Browse files
Consider guards for out-of-bound checking
* tools/dvecompile.cpp, tools/dvecompile.h: here.
parent
853761a4
Pipeline
#17425
passed with stage
in 7 minutes and 51 seconds
Changes
2
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
tools/dvecompile.cpp
View file @
bfe1dd38
...
...
@@ -909,6 +909,9 @@ void dve_compiler::transition_guard( ext_transition_t *et, std::string in )
if_clause
(
in_state
(
et
->
first
->
get_process_gid
(),
et
->
first
->
get_state1_lid
(),
in
)
);
}
if
(
et
->
first
->
get_guard
())
if_cexp_print_check_bounds
(
*
et
->
first
->
get_guard
(),
in
,
many
);
if_cexpr_clause
(
et
->
first
->
get_guard
(),
in
);
if
(
et
->
synchronized
)
...
...
@@ -1192,6 +1195,8 @@ void dve_compiler::gen_successors()
new_label
();
if_begin
(
true
);
// FIXME
if_clause
(
in_state
(
i
,
iter_process_transition_map
->
first
,
in
)
);
if_end
();
block_begin
();
...
...
tools/dvecompile.h
View file @
bfe1dd38
...
...
@@ -211,21 +211,126 @@ struct dve_compiler: public dve_explicit_system_t
return
stream
.
str
();
}
void
print_check_bounds
(
dve_expression_t
&
expr
,
std
::
string
state
)
std
::
string
if_cexp_print_check_bounds_inner
(
dve_expression_t
&
expr
,
std
::
string
state
)
{
std
::
string
res
=
""
;
dve_symbol_table_t
*
parent_table
=
expr
.
get_symbol_table
();
if
(
!
parent_table
)
gerr
<<
"Writing expression: Symbol table not set"
<<
thr
();
switch
(
expr
.
get_operator
())
{
case
T_LT
:
case
T_LEQ
:
case
T_EQ
:
case
T_NEQ
:
case
T_GT
:
case
T_GEQ
:
case
T_PLUS
:
case
T_MINUS
:
case
T_MULT
:
case
T_AND
:
case
T_OR
:
case
T_XOR
:
case
T_LSHIFT
:
case
T_RSHIFT
:
case
T_BOOL_AND
:
case
T_BOOL_OR
:
case
T_ASSIGNMENT
:
return
"("
+
if_cexp_print_check_bounds_inner
(
*
expr
.
left
(),
state
)
+
" && "
+
if_cexp_print_check_bounds_inner
(
*
expr
.
right
(),
state
)
+
")"
;
break
;
case
T_FOREIGN_SQUARE_BRACKETS
:
case
T_SQUARE_BRACKETS
:
{
res
+=
""
;
if
(
!
expr
.
arity
())
return
""
;
res
=
"("
;
for
(
unsigned
i
=
0
;
i
<
expr
.
arity
();
++
i
)
{
for
(
unsigned
j
=
0
;
j
<
expr
.
subexpr
(
i
)
->
arity
();
++
j
)
{
res
+=
if_cexp_print_check_bounds_inner
(
*
expr
.
subexpr
(
i
)
->
subexpr
(
j
),
state
);
res
+=
"&&"
;
}
res
=
res
+
" ("
+
to_string
(
parent_table
->
get_variable
(
expr
.
get_ident_gid
())
->
get_vector_size
())
+
">"
+
to_string
(
cexpr
(
*
expr
.
subexpr
(
i
),
state
,
false
))
+
") && ("
+
to_string
(
cexpr
(
*
expr
.
subexpr
(
i
),
state
,
false
))
+
"> -1)"
;
if
(
i
<
expr
.
arity
()
-
1
)
res
+=
"&&"
;
}
res
+=
")"
;
return
res
;
}
break
;
case
T_MOD
:
case
T_DIV
:
res
+=
""
;
res
+=
"("
+
if_cexp_print_check_bounds_inner
(
*
expr
.
left
(),
state
)
+
" && "
+
if_cexp_print_check_bounds_inner
(
*
expr
.
right
(),
state
)
+
" && "
+
if_cexp_print_check_bounds_inner
(
*
expr
.
right
(),
state
)
//Maybe fixme
+
"!= 0)"
;
return
res
;
case
T_UNARY_MINUS
:
case
T_TILDE
:
case
T_BOOL_NOT
:
return
if_cexp_print_check_bounds_inner
(
*
expr
.
right
(),
state
)
;
case
T_FOREIGN_ID
:
case
T_ID
:
res
+=
"/*ID*/"
;
break
;
case
T_NAT
:
res
+=
"/*T_NAT*/"
;
break
;
case
T_PARENTHESIS
:
return
if_cexp_print_check_bounds_inner
(
*
expr
.
left
(),
state
)
;
default:
res
+=
"/*Unknown operator*/"
;
gerr
<<
"Problem in expression - unknown operator"
<<
" number "
<<
expr
.
get_operator
()
<<
psh
();
}
res
+=
"true"
;
return
res
;
}
void
if_cexp_print_check_bounds
(
dve_expression_t
&
expr
,
std
::
string
state
,
bool
many
)
{
assert
(
expr
.
get_operator
()
==
T_SQUARE_BRACKETS
);
if
(
!
expr
.
arity
())
return
;
dve_symbol_table_t
*
parent_table
=
expr
.
get_symbol_table
();
line
(
"// Here check out-of-bounds"
);
line
(
"if ("
+
to_string
(
parent_table
->
get_variable
(
expr
.
get_ident_gid
())
->
get_vector_size
())
+
"<="
+
to_string
(
cexpr
(
*
expr
.
subexpr
(
0
),
state
,
false
))
+
")"
);
line
(
"{ /* fprintf( stderr,
\"
Out-of-bound! see line:
\"
);*/ return -1; }"
);
std
::
string
prefix
(
many
?
" "
:
" && "
);
std
::
string
suffix
(
many
?
" && "
:
" "
);
line
(
prefix
+
if_cexp_print_check_bounds_inner
(
expr
,
state
)
+
suffix
);
}
void
print_check_bounds
(
dve_expression_t
&
expr
,
std
::
string
state
)
{
line
(
"if (!("
+
if_cexp_print_check_bounds_inner
(
expr
,
state
)
+
"))"
);
line
(
"{ fprintf( stderr,
\"
Out-of-bound!
\"
); return -1; }"
);
return
;
// assert(expr.get_operator() == T_SQUARE_BRACKETS);
// if (!expr.arity())
// return ;
// dve_symbol_table_t * parent_table = expr.get_symbol_table();
// line ("// Here check out-of-bounds");
// for (unsigned i = 0; i < expr.arity(); ++i)
// for (unsigned j = 0; j < expr.subexpr(i)->arity(); ++j)
// print_check_bounds(*expr.subexpr(i)->subexpr(j), state);
// for (unsigned i = 0; i < expr.arity(); ++i)
// { line ("if (("
// + to_string(parent_table->get_variable(expr.get_ident_gid())->get_vector_size())
// + "<="
// + to_string (cexpr(*expr.subexpr(i), state, false ))
// + ") || ("
// + to_string (cexpr(*expr.subexpr(i), state, false ))
// + "<= -1))"
// );
// line ("{ fprintf( stderr, \"Out-of-bound! see exp: " +
// to_string (cexpr(*expr.subexpr(i), state, false )) + "\"); return -1; }");
// }
}
void
print_cexpr
(
dve_expression_t
&
expr
,
std
::
string
state
)
{
...
...
@@ -248,7 +353,7 @@ struct dve_compiler: public dve_explicit_system_t
print_check_bounds
(
*
expr
.
right
(),
state
);
}
}
line
(
cexpr
(
expr
,
state
,
false
)
+
";"
);
}
...
...
@@ -263,7 +368,7 @@ struct dve_compiler: public dve_explicit_system_t
void
block_end
()
{
deindent
();
line
(
"}"
);
}
std
::
string
in_state
(
int
process
,
int
state
,
std
::
string
from_state
)
{
return
"("
+
process_state
(
process
,
from_state
)
+
" == "
+
wibble
::
str
::
fmt
(
state
)
+
")"
;
return
"("
+
process_state
(
process
,
from_state
)
+
" == "
+
wibble
::
str
::
fmt
(
state
)
+
")"
;
}
void
setOutput
(
std
::
ostream
&
o
)
{
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment