CBMC
language_util.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
9 #include "language_util.h"
10 
11 #include <util/invariant.h>
12 #include <util/namespace.h>
13 #include <util/std_expr.h>
14 #include <util/symbol_table.h>
15 
16 #include "language.h"
17 #include "mode.h"
18 
19 #include <memory>
20 
22  const namespacet &ns,
23  const irep_idt &mode,
24  const exprt &expr)
25 {
26  std::unique_ptr<languaget> language = (mode == ID_unknown)
28  : get_language_from_mode(mode);
29  INVARIANT(
30  language, "could not retrieve language for mode '" + id2string(mode) + "'");
31 
32  std::string result;
33  language->from_expr(expr, result, ns);
34 
35  return result;
36 }
37 
38 std::string from_expr(
39  const namespacet &ns,
40  const irep_idt &identifier,
41  const exprt &expr)
42 {
43  std::unique_ptr<languaget> p(get_language_from_identifier(ns, identifier));
44 
45  std::string result;
46  p->from_expr(expr, result, ns);
47 
48  return result;
49 }
50 
51 std::string from_type(
52  const namespacet &ns,
53  const irep_idt &identifier,
54  const typet &type)
55 {
56  std::unique_ptr<languaget> p(get_language_from_identifier(ns, identifier));
57 
58  std::string result;
59  p->from_type(type, result, ns);
60 
61  return result;
62 }
63 
64 std::string type_to_name(
65  const namespacet &ns,
66  const irep_idt &identifier,
67  const typet &type)
68 {
69  std::unique_ptr<languaget> p(get_language_from_identifier(ns, identifier));
70 
71  std::string result;
72  p->type_to_name(type, result, ns);
73 
74  return result;
75 }
76 
77 std::string from_expr(const exprt &expr)
78 {
79  symbol_tablet symbol_table;
80  return from_expr(namespacet(symbol_table), irep_idt(), expr);
81 }
82 
83 std::string from_type(const typet &type)
84 {
85  symbol_tablet symbol_table;
86  return from_type(namespacet(symbol_table), irep_idt(), type);
87 }
88 
90  const namespacet &ns,
91  const irep_idt &identifier,
92  const std::string &src)
93 {
94  std::unique_ptr<languaget> p(get_language_from_identifier(ns, identifier));
95 
98 
99  const symbolt &symbol=ns.lookup(identifier);
100 
101  exprt expr;
102 
103  if(p->to_expr(src, id2string(symbol.module), expr, ns))
104  return nil_exprt();
105 
106  return expr;
107 }
108 
109 std::string type_to_name(const typet &type)
110 {
111  symbol_tablet symbol_table;
112  return type_to_name(namespacet(symbol_table), irep_idt(), type);
113 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
symbol_tablet
The symbol table.
Definition: symbol_table.h:13
type_to_name
std::string type_to_name(const namespacet &ns, const irep_idt &identifier, const typet &type)
Definition: language_util.cpp:64
typet
The type of an expression, extends irept.
Definition: type.h:28
to_expr
exprt to_expr(const namespacet &ns, const irep_idt &identifier, const std::string &src)
Definition: language_util.cpp:89
get_language_from_mode
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:51
invariant.h
exprt
Base class for all expressions.
Definition: expr.h:55
mode.h
from_type
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
Definition: language_util.cpp:51
irep_idt
dstringt irep_idt
Definition: irep.h:37
namespace.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
languaget::from_type
virtual bool from_type(const typet &type, std::string &code, const namespacet &ns)
Formats the given type in a language-specific way.
Definition: language.cpp:41
language_util.h
languaget::from_expr
virtual bool from_expr(const exprt &expr, std::string &code, const namespacet &ns)
Formats the given expression in a language-specific way.
Definition: language.cpp:32
nil_exprt
The NIL expression.
Definition: std_expr.h:3025
language.h
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
null_message_handlert
Definition: message.h:76
symbolt
Symbol table entry.
Definition: symbol.h:27
languaget::to_expr
virtual bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns)=0
Parses the given string into an expression.
get_language_from_identifier
std::unique_ptr< languaget > get_language_from_identifier(const namespacet &ns, const irep_idt &identifier)
Get the language corresponding to the mode of the given identifier's symbol.
Definition: mode.cpp:84
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
symbol_table.h
Author: Diffblue Ltd.
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
std_expr.h
null_message_handler
null_message_handlert null_message_handler
Definition: message.cpp:14
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:38
languaget::type_to_name
virtual bool type_to_name(const typet &type, std::string &name, const namespacet &ns)
Encodes the given type in a language-specific way.
Definition: language.cpp:50
from_expr_using_mode
std::string from_expr_using_mode(const namespacet &ns, const irep_idt &mode, const exprt &expr)
Formats an expression using the given namespace, using the given mode to retrieve the language printe...
Definition: language_util.cpp:21
get_default_language
std::unique_ptr< languaget > get_default_language()
Returns the default language.
Definition: mode.cpp:139