CBMC
statement_list_parse_tree_io.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Statement List Language Parse Tree Output
4 
5 Author: Matthias Weiss, matthias.weiss@diffblue.com
6 
7 \*******************************************************************/
8 
11 
14 
15 #include <util/arith_tools.h>
16 #include <util/bitvector_types.h>
17 #include <util/ieee_float.h>
18 
20 #define NO_VALUE "(none)"
21 
25 static void output_constant(std::ostream &os, const constant_exprt &constant)
26 {
27  mp_integer ivalue;
28  if(!to_integer(constant, ivalue))
29  os << ivalue;
30  else if(can_cast_type<floatbv_typet>(constant.type()))
31  {
32  ieee_floatt real{get_real_type()};
33  real.from_expr(constant);
34  os << real.to_float();
35  }
36  else
37  os << constant.get_value();
38 }
39 
44  std::ostream &os,
45  const code_frontend_assignt &assignment)
46 {
47  os << assignment.lhs().get(ID_identifier) << " := ";
48  const constant_exprt *const constant =
49  expr_try_dynamic_cast<constant_exprt>(assignment.rhs());
50  if(constant)
51  output_constant(os, *constant);
52  else
53  os << assignment.rhs().get(ID_identifier);
54 }
55 
57  std::ostream &out,
58  const statement_list_parse_treet &parse_tree)
59 {
60  for(const auto &function_block : parse_tree.function_blocks)
61  {
62  out << "============== Function Block ==============\n";
63  output_function_block(out, function_block);
64  out << '\n';
65  }
66 
67  for(const auto &function : parse_tree.functions)
68  {
69  out << "================= Function =================\n";
70  output_function(out, function);
71  out << '\n';
72  }
73 
74  if(!parse_tree.tags.empty())
75  {
76  out << "================= Tag List =================\n";
77  for(const auto &tag : parse_tree.tags)
78  {
79  out << tag.pretty();
80  out << '\n';
81  }
82  }
83 }
84 
86  std::ostream &os,
87  const statement_list_parse_treet::function_blockt &function_block)
88 {
89  output_tia_module_properties(function_block, os);
90  output_common_var_declarations(os, function_block);
91  output_static_var_declarations(os, function_block);
92  output_network_list(os, function_block.networks);
93 }
94 
96  std::ostream &os,
98 {
99  output_tia_module_properties(function, os);
100  output_return_value(function, os);
101  output_common_var_declarations(os, function);
102  output_network_list(os, function.networks);
103 }
104 
107  std::ostream &os)
108 {
109  os << "Name: " << module.name << '\n';
110  os << "Version: " << module.version << "\n\n";
111 }
112 
115  std::ostream &os)
116 {
117  os << "Return type: ";
118  if(function.return_type.is_nil())
119  os << "Void";
120  else
121  os << function.return_type.id();
122  os << "\n\n";
123 }
124 
126  std::ostream &os,
128 {
129  if(!module.var_input.empty())
130  {
131  os << "--------- Input Variables ----------\n\n";
133  }
134 
135  if(!module.var_inout.empty())
136  {
137  os << "--------- In/Out Variables ---------\n\n";
139  }
140 
141  if(!module.var_output.empty())
142  {
143  os << "--------- Output Variables ---------\n\n";
145  }
146 
147  if(!module.var_constant.empty())
148  {
149  os << "-------- Constant Variables --------\n\n";
151  }
152 
153  if(!module.var_temp.empty())
154  {
155  os << "---------- Temp Variables ----------\n\n";
157  }
158 }
159 
161  std::ostream &os,
163 {
164  if(!block.var_static.empty())
165  {
166  os << "--------- Static Variables ---------\n\n";
168  }
169 }
170 
172  std::ostream &os,
174 {
175  for(const auto &declaration : declarations)
176  {
177  output_var_declaration(os, declaration);
178  os << "\n\n";
179  }
180 }
181 
183  std::ostream &os,
185 {
186  os << declaration.variable.pretty() << '\n';
187  os << " * default_value: ";
188  if(declaration.default_value)
189  {
190  const constant_exprt &constant =
191  to_constant_expr(declaration.default_value.value());
192  output_constant(os, constant);
193  }
194  else
195  os << NO_VALUE;
196 }
197 
199  std::ostream &os,
201 {
202  os << "-------------- Networks --------------\n\n";
203  for(const auto &network : networks)
204  {
205  output_network(os, network);
206  os << '\n';
207  }
208 }
209 
211  std::ostream &os,
213 {
214  os << "Title: " << network.title.value_or(NO_VALUE) << '\n';
215  os << "Instructions: ";
216  if(network.instructions.empty())
217  os << NO_VALUE;
218  os << '\n';
219  for(const auto &instruction : network.instructions)
220  {
221  output_instruction(os, instruction);
222  os << '\n';
223  }
224 }
225 
227  std::ostream &os,
228  const statement_list_parse_treet::instructiont &instruction)
229 {
230  for(const codet &token : instruction.tokens)
231  {
232  os << token.get_statement();
233  for(const auto &expr : token.operands())
234  {
235  const symbol_exprt *const symbol =
236  expr_try_dynamic_cast<symbol_exprt>(expr);
237  if(symbol)
238  {
239  os << '\t' << symbol->get_identifier();
240  continue;
241  }
242  const constant_exprt *const constant =
243  expr_try_dynamic_cast<constant_exprt>(expr);
244  if(constant)
245  {
246  os << '\t';
247  output_constant(os, *constant);
248  continue;
249  }
250  if(const auto assign = expr_try_dynamic_cast<code_frontend_assignt>(expr))
251  {
252  os << "\n\t";
253  output_parameter_assignment(os, *assign);
254  continue;
255  }
256  os << '\t' << expr.id();
257  }
258  }
259 }
ieee_floatt
Definition: ieee_float.h:116
statement_list_parse_treet::var_declarationt::default_value
optionalt< exprt > default_value
Optional default value of the variable.
Definition: statement_list_parse_tree.h:33
mp_integer
BigInt mp_integer
Definition: smt_terms.h:17
output_return_value
void output_return_value(const statement_list_parse_treet::functiont &function, std::ostream &os)
Prints the return value of a function to the given output stream.
Definition: statement_list_parse_tree_io.cpp:113
arith_tools.h
statement_list_parse_treet::tia_modulet::networks
networkst networks
List of all networks of this module.
Definition: statement_list_parse_tree.h:98
statement_list_parse_treet::networkst
std::list< networkt > networkst
Definition: statement_list_parse_tree.h:75
statement_list_parse_treet::var_declarationst
std::list< var_declarationt > var_declarationst
Definition: statement_list_parse_tree.h:39
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
statement_list_parse_treet::tia_modulet::version
const std::string version
Version of the module.
Definition: statement_list_parse_tree.h:84
statement_list_parse_treet::tia_modulet::var_temp
var_declarationst var_temp
Temp variable declarations.
Definition: statement_list_parse_tree.h:93
statement_list_parse_treet::var_declarationt
Struct for a single variable declaration in Statement List.
Definition: statement_list_parse_tree.h:28
statement_list_parse_treet::tia_modulet::var_input
var_declarationst var_input
Input variable declarations.
Definition: statement_list_parse_tree.h:87
statement_list_parse_treet::instructiont
Represents a regular Statement List instruction which consists out of one or more codet tokens.
Definition: statement_list_parse_tree.h:43
statement_list_parse_treet::tia_modulet
Base element of all modules in the Totally Integrated Automation (TIA) portal by Siemens.
Definition: statement_list_parse_tree.h:79
to_integer
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:20
statement_list_parse_treet::var_declarationt::variable
symbol_exprt variable
Representation of the variable, including identifier and type.
Definition: statement_list_parse_tree.h:31
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:112
statement_list_parse_treet::function_blockt
Structure for a simple function block in Statement List.
Definition: statement_list_parse_tree.h:146
output_parse_tree
void output_parse_tree(std::ostream &out, const statement_list_parse_treet &parse_tree)
Prints the given Statement List parse tree in a human-readable form to the given output stream.
Definition: statement_list_parse_tree_io.cpp:56
code_frontend_assignt::lhs
exprt & lhs()
Definition: std_code.h:41
irept::get
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
output_common_var_declarations
void output_common_var_declarations(std::ostream &os, const statement_list_parse_treet::tia_modulet &module)
Prints all variable declarations functions and function blocks have in common to the given output str...
Definition: statement_list_parse_tree_io.cpp:125
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:84
output_instruction
void output_instruction(std::ostream &os, const statement_list_parse_treet::instructiont &instruction)
Prints the given Statement List instruction in a human-readable form to the given output stream.
Definition: statement_list_parse_tree_io.cpp:226
statement_list_parse_tree_io.h
statement_list_parse_treet::tia_modulet::var_constant
var_declarationst var_constant
Constant variable declarations.
Definition: statement_list_parse_tree.h:95
code_frontend_assignt::rhs
exprt & rhs()
Definition: std_code.h:46
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:142
statement_list_parse_treet::function_blocks
function_blockst function_blocks
List of function blocks this parse tree includes.
Definition: statement_list_parse_tree.h:173
statement_list_parse_treet::tia_modulet::name
const irep_idt name
Name of the module.
Definition: statement_list_parse_tree.h:82
bitvector_types.h
output_var_declaration
void output_var_declaration(std::ostream &os, const statement_list_parse_treet::var_declarationt &declaration)
Prints the given Statement List variable declaration in a human-readable form to the given output str...
Definition: statement_list_parse_tree_io.cpp:182
output_var_declaration_list
void output_var_declaration_list(std::ostream &os, const statement_list_parse_treet::var_declarationst &declarations)
Prints all variable declarations of the given list to the given output stream.
Definition: statement_list_parse_tree_io.cpp:171
code_frontend_assignt
A codet representing an assignment in the program.
Definition: std_code.h:23
statement_list_parse_treet::instructiont::tokens
std::vector< codet > tokens
Data structure for all tokens of the instruction.
Definition: statement_list_parse_tree.h:46
statement_list_parse_treet::networkt::instructions
instructionst instructions
Definition: statement_list_parse_tree.h:61
output_static_var_declarations
void output_static_var_declarations(std::ostream &os, const statement_list_parse_treet::function_blockt &block)
Prints the static variable declarations of a function block to the given output stream.
Definition: statement_list_parse_tree_io.cpp:160
statement_list_parse_treet::networkt::title
optionalt< std::string > title
Definition: statement_list_parse_tree.h:60
statement_list_parse_treet::function_blockt::var_static
var_declarationst var_static
FB-exclusive static variable declarations.
Definition: statement_list_parse_tree.h:149
output_network_list
void output_network_list(std::ostream &os, const statement_list_parse_treet::networkst &networks)
Prints the given network list in a human-readable form to the given output stream.
Definition: statement_list_parse_tree_io.cpp:198
statement_list_parse_treet
Intermediate representation of a parsed Statement List file before converting it into a goto program.
Definition: statement_list_parse_tree.h:20
statement_list_parse_treet::tags
std::vector< symbol_exprt > tags
List of tags that were included in the source.
Definition: statement_list_parse_tree.h:177
ieee_float.h
output_constant
static void output_constant(std::ostream &os, const constant_exprt &constant)
Prints a constant to the given output stream.
Definition: statement_list_parse_tree_io.cpp:25
NO_VALUE
#define NO_VALUE
String to indicate that there is no value.
Definition: statement_list_parse_tree_io.cpp:20
output_tia_module_properties
void output_tia_module_properties(const statement_list_parse_treet::tia_modulet &module, std::ostream &os)
Prints the basic information about a TIA module to the given output stream.
Definition: statement_list_parse_tree_io.cpp:105
get_real_type
floatbv_typet get_real_type()
Creates a new type that resembles the 'Real' type of the Siemens PLC languages.
Definition: statement_list_types.cpp:25
output_parameter_assignment
static void output_parameter_assignment(std::ostream &os, const code_frontend_assignt &assignment)
Prints the assignment of a module parameter to the given output stream.
Definition: statement_list_parse_tree_io.cpp:43
output_function_block
void output_function_block(std::ostream &os, const statement_list_parse_treet::function_blockt &function_block)
Prints the given Statement List function block in a human-readable form to the given output stream.
Definition: statement_list_parse_tree_io.cpp:85
exprt::operands
operandst & operands()
Definition: expr.h:94
output_function
void output_function(std::ostream &os, const statement_list_parse_treet::functiont &function)
Prints the given Statement List function in a human-readable form to the given output stream.
Definition: statement_list_parse_tree_io.cpp:95
statement_list_parse_treet::tia_modulet::var_inout
var_declarationst var_inout
Inout variable declarations.
Definition: statement_list_parse_tree.h:89
statement_list_parse_treet::functiont
Structure for a simple function in Statement List.
Definition: statement_list_parse_tree.h:127
statement_list_parse_treet::tia_modulet::var_output
var_declarationst var_output
Output variable declarations.
Definition: statement_list_parse_tree.h:91
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code_base.h:65
constant_exprt
A constant literal expression.
Definition: std_expr.h:2941
output_network
void output_network(std::ostream &os, const statement_list_parse_treet::networkt &network)
Prints the given Statement List network in a human-readable form to the given output stream.
Definition: statement_list_parse_tree_io.cpp:210
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2950
can_cast_type< floatbv_typet >
bool can_cast_type< floatbv_typet >(const typet &type)
Check whether a reference to a typet is a floatbv_typet.
Definition: bitvector_types.h:354
statement_list_parse_treet::functions
functionst functions
List of functions this parse tree includes.
Definition: statement_list_parse_tree.h:175
statement_list_parse_treet::networkt
Representation of a network in Siemens TIA.
Definition: statement_list_parse_tree.h:58
statement_list_types.h
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:28
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2992