Skip to content

Commit d61a8f4

Browse files
tautschnigtautschnig
authored
Merge pull request #5054 from MatWise/feature/statement-list-jumps
Statement List: Jump instructions
2 parents 8e651e4 + 5656450 commit d61a8f4

14 files changed

+614
-110
lines changed

‎regression/statement-list/Jump1/main.awl

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
FUNCTION_BLOCK "Main"
2+
VERSION : 0.1
3+
VAR_TEMP
4+
temp1 : Bool;
5+
temp2 : Bool;
6+
END_VAR
7+
BEGIN
8+
NETWORK
9+
TITLE =
10+
SET;
11+
= temp1;
12+
= temp2;
13+
JU lab0;
14+
CALL "__CPROVER_assert"
15+
( condition := FALSE
16+
);
17+
lab0: SET;
18+
lab1: A temp1;
19+
A temp2;
20+
NOT;
21+
= temp2;
22+
A temp2;
23+
24+
JCN lab1;
25+
CALL "__CPROVER_assert"
26+
( condition := #temp2
27+
);
28+
29+
JC lab2;
30+
CALL "__CPROVER_assert"
31+
( condition := FALSE
32+
);
33+
34+
lab2: NOP 0;
35+
36+
END_FUNCTION_BLOCK
37+

‎regression/statement-list/Jump1/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.awl
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎src/statement-list/converters/convert_string_value.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -32,10 +32,12 @@ string_constantt convert_version(const std::string &src)
3232
return result;
3333
}
3434

35-
code_labelt convert_label(const std::string &src)
35+
string_constantt convert_label(const std::string &src)
3636
{
3737
// Cut the trailing colon
3838
std::string value = src.substr(0, src.length() - 1);
3939

40-
return code_labelt{value, codet(ID_label)};
40+
string_constantt result{value};
41+
result.set(ID_statement_list_type, ID_label);
42+
return result;
4143
}

‎src/statement-list/converters/convert_string_value.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ string_constantt convert_version(const std::string &src);
3232

3333
/// Converts a string into a Statement List label.
3434
/// \param src: String returned by the parser.
35-
/// \return Code label expression representing the label.
36-
code_labelt convert_label(const std::string &src);
35+
/// \return String constant representing the label.
36+
string_constantt convert_label(const std::string &src);
3737

3838
#endif // CPROVER_STATEMENT_LIST_CONVERTERS_CONVERT_STRING_VALUE_H

‎src/statement-list/converters/expr2statement_list.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,7 @@ Author: Matthias Weiss, [email protected]
5959
/// such. This can reduce complexity in some cases.
6060
/// \param lhs: Left side of the binary expression.
6161
/// \param rhs: Right side of the binary expression.
62-
/// \return: List of instrumented operands.
62+
/// \return List of instrumented operands.
6363
static std::vector<exprt>
6464
instrument_equal_operands(const exprt &lhs, const exprt &rhs)
6565
{
@@ -93,7 +93,7 @@ instrument_equal_operands(const exprt &lhs, const exprt &rhs)
9393

9494
/// Checks if the expression or one of its parameters is not of type bool.
9595
/// \param expr: Expression to verify.
96-
/// \return: True if the expression and its operands are not or only partially
96+
/// \return True if the expression and its operands are not or only partially
9797
/// of type bool, false otherwise.
9898
static bool is_not_bool(const exprt &expr)
9999
{

‎src/statement-list/converters/expr2statement_list.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,7 @@ class expr2stlt
6262
/// recursively in the process.
6363
/// \param expr: Expression to convert. Operands of this expression will be
6464
/// converted as well via recursion.
65-
/// \return: String containing human-readable STL code for the expression.
65+
/// \return String containing human-readable STL code for the expression.
6666
std::string convert(const exprt &expr);
6767

6868
private:
@@ -147,7 +147,7 @@ class expr2stlt
147147
/// Returns the given identifier in a form that is compatible with STL by
148148
/// looking up the symbol or cutting the scope when needed.
149149
/// \param identifier: Identifier that should be converted.
150-
/// \return: Converted identifier.
150+
/// \return Converted identifier.
151151
irep_idt id_shorthand(const irep_idt &identifier);
152152
};
153153

‎src/statement-list/parser.y

Lines changed: 31 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -128,6 +128,9 @@ extern char *yystatement_listtext;
128128
%token TOK_ACCU_DINT_GTE ">=D"
129129
%token TOK_ACCU_DINT_LTE "<=D"
130130
%token TOK_ASSIGNMENT ":="
131+
%token TOK_JUMP_UNCONDITIONAL "JU"
132+
%token TOK_JUMP_CONDITIONAL "JC"
133+
%token TOK_JUMP_CONDITIONAL_NOT "JCN"
131134

132135
/*** Value tokens ***/
133136
%token TOK_INT_LITERAL
@@ -668,7 +671,7 @@ Opt_Instruction_List:
668671
}
669672
;
670673

671-
// Structured Text grammar
674+
// Statement List grammar
672675
Instruction_List:
673676
Oom_IL_Instruction
674677
;
@@ -688,7 +691,7 @@ Oom_IL_Instruction:
688691
;
689692

690693
IL_Instruction:
691-
Opt_Label Opt_Instruction ';'
694+
Opt_Label Instruction ';'
692695
{
693696
$$ = $2;
694697
parser_stack($$).add_to_operands(std::move(parser_stack($1)));
@@ -708,14 +711,9 @@ IL_Label:
708711
TOK_LABEL
709712
;
710713

711-
Opt_Instruction:
714+
Instruction:
712715
IL_Simple_Operation
713716
| IL_Invocation
714-
| /* nothing */
715-
{
716-
newstack($$);
717-
parser_stack($$).id(ID_statement_list_instruction);
718-
}
719717
;
720718

721719
IL_Simple_Operation:
@@ -932,12 +930,12 @@ IL_Simple_Operator:
932930
{
933931
$$ = $1;
934932
parser_stack($$).id(ID_statement_list_xor);
935-
}
933+
}
936934
| TOK_XOR_NOT
937935
{
938936
$$ = $1;
939937
parser_stack($$).id(ID_statement_list_xor_not);
940-
}
938+
}
941939
| TOK_AND_NESTED
942940
{
943941
$$ = $1;
@@ -947,22 +945,22 @@ IL_Simple_Operator:
947945
{
948946
$$ = $1;
949947
parser_stack($$).id(ID_statement_list_and_not_nested);
950-
}
948+
}
951949
| TOK_OR_NESTED
952950
{
953951
$$ = $1;
954952
parser_stack($$).id(ID_statement_list_or_nested);
955-
}
953+
}
956954
| TOK_OR_NOT_NESTED
957955
{
958956
$$ = $1;
959957
parser_stack($$).id(ID_statement_list_or_not_nested);
960-
}
958+
}
961959
| TOK_XOR_NESTED
962960
{
963961
$$ = $1;
964962
parser_stack($$).id(ID_statement_list_xor_nested);
965-
}
963+
}
966964
| TOK_XOR_NOT_NESTED
967965
{
968966
$$ = $1;
@@ -972,7 +970,7 @@ IL_Simple_Operator:
972970
{
973971
$$ = $1;
974972
parser_stack($$).id(ID_statement_list_nesting_closed);
975-
}
973+
}
976974
| TOK_ASSIGN
977975
{
978976
$$ = $1;
@@ -987,7 +985,7 @@ IL_Simple_Operator:
987985
{
988986
$$ = $1;
989987
parser_stack($$).id(ID_statement_list_clr_rlo);
990-
}
988+
}
991989
| TOK_SET
992990
{
993991
$$ = $1;
@@ -997,12 +995,27 @@ IL_Simple_Operator:
997995
{
998996
$$ = $1;
999997
parser_stack($$).id(ID_statement_list_reset);
1000-
}
998+
}
1001999
| TOK_NOT
10021000
{
10031001
$$ = $1;
10041002
parser_stack($$).id(ID_statement_list_not);
1005-
}
1003+
}
1004+
| TOK_JUMP_UNCONDITIONAL
1005+
{
1006+
$$ = $1;
1007+
parser_stack($$).id(ID_statement_list_jump_unconditional);
1008+
}
1009+
| TOK_JUMP_CONDITIONAL
1010+
{
1011+
$$ = $1;
1012+
parser_stack($$).id(ID_statement_list_jump_conditional);
1013+
}
1014+
| TOK_JUMP_CONDITIONAL_NOT
1015+
{
1016+
$$ = $1;
1017+
parser_stack($$).id(ID_statement_list_jump_conditional_not);
1018+
}
10061019
;
10071020

10081021
IL_Operand:

‎src/statement-list/scanner.l

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -165,6 +165,9 @@ void statement_list_scanner_init()
165165
\<D { loc(); return TOK_ACCU_DINT_LT; }
166166
\>=D { loc(); return TOK_ACCU_DINT_GTE; }
167167
\<=D { loc(); return TOK_ACCU_DINT_LTE; }
168+
JU { loc(); return TOK_JUMP_UNCONDITIONAL; }
169+
JC { loc(); return TOK_JUMP_CONDITIONAL; }
170+
JCN { loc(); return TOK_JUMP_CONDITIONAL_NOT; }
168171

169172
(10#)?[\+-]?[0-9]+ {
170173
newstack(yystatement_listlval);
@@ -272,7 +275,7 @@ void statement_list_scanner_init()
272275
return TOK_IDENTIFIER;
273276
}
274277

275-
[a-zA-Z_\.][a-zA-Z0-9_\.]*: {
278+
[a-zA-Z_][a-zA-Z0-9_]*: {
276279
newstack(yystatement_listlval);
277280
parser_stack(yystatement_listlval) =
278281
convert_label(yytext);

‎src/statement-list/statement_list_language.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ class statement_list_languaget : public languaget
3232
/// instance's parse tree.
3333
/// \param instream: Input to parse.
3434
/// \param path: Path of the input.
35-
/// \return: False if successful.
35+
/// \return False if successful.
3636
bool parse(std::istream &instream, const std::string &path) override;
3737

3838
/// Currently unused.
@@ -45,7 +45,7 @@ class statement_list_languaget : public languaget
4545
/// \param module: Name of the file that has been parsed.
4646
/// \param keep_file_local: Set to true if local variables of this module
4747
/// should be included in the table.
48-
/// \return: False if no errors occurred, true otherwise.
48+
/// \return False if no errors occurred, true otherwise.
4949
bool typecheck(
5050
symbol_tablet &symbol_table,
5151
const std::string &module,

‎src/statement-list/statement_list_parser.cpp

Lines changed: 16 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -248,7 +248,7 @@ static exprt find_network_instructions(const exprt &network)
248248
UNREACHABLE; // Network expression should always have an instruction list
249249
}
250250

251-
/// Adds all valid instructions to the given network.
251+
/// Adds all valid instructions to the given network.
252252
/// \param network: The network to which the instructions belong.
253253
/// \param instructions: The root expression of a valid instruction list.
254254
static void find_instructions(
@@ -258,13 +258,24 @@ static void find_instructions(
258258
for(const exprt &instruction_expr : instructions.operands())
259259
{
260260
statement_list_parse_treet::instructiont instruction;
261+
261262
codet code_token(to_multi_ary_expr(instruction_expr).op0().id());
262-
for(const exprt &operand : instruction_expr.operands())
263+
string_constantt label{ID_nil};
264+
for(auto op_it = std::next(instruction_expr.operands().begin());
265+
op_it != end(instruction_expr.operands());
266+
++op_it)
263267
{
264-
if(operand.is_not_nil() && operand.id() != code_token.get_statement())
265-
code_token.add_to_operands(operand);
268+
if(op_it->get(ID_statement_list_type) == ID_label)
269+
label = to_string_constant(*op_it);
270+
else if(op_it->is_not_nil())
271+
code_token.add_to_operands(*op_it);
266272
}
267-
instruction.add_token(code_token);
273+
274+
if(label.get_value() == ID_nil)
275+
instruction.add_token(code_token);
276+
else
277+
instruction.add_token(code_labelt{label.get_value(), code_token});
278+
268279
network.add_instruction(instruction);
269280
}
270281
}

‎src/statement-list/statement_list_parser.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ class statement_list_parsert : public parsert
3636
public:
3737
/// Starts the parsing process and saves the result inside of this instance's
3838
/// parse tree.
39-
/// \return: False if successful.
39+
/// \return False if successful.
4040
bool parse() override;
4141

4242
/// Adds a function block to the parse tree by converting the \p block

0 commit comments

Comments
 (0)