CBMC
json_symbol.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: JSON symbol deserialization
4 
5 Author: Chris Smowton, chris.smowton@diffblue.com
6 
7 \*******************************************************************/
8 
9 #include "json_symbol.h"
10 
11 #include <util/exception_utils.h>
12 #include <util/expr.h>
13 #include <util/json_irep.h>
14 #include <util/source_location.h>
15 #include <util/type.h>
16 
21 static const std::string &
22 try_get_string(const jsont &in, const std::string &key)
23 {
24  if(!in.is_string())
26  "symbol_from_json: expected string for key '" + key + "'");
27  return in.value;
28 }
29 
34 static bool try_get_bool(const jsont &in, const std::string &key)
35 {
36  if(!(in.is_true() || in.is_false()))
38  "symbol_from_json: expected bool for key '" + key + "'");
39  return in.is_true();
40 }
41 
46 {
47  if(!in.is_object())
48  throw deserialization_exceptiont("symbol_from_json takes an object");
49  symbolt result;
50  json_irept json2irep(true);
51  for(const auto &kv : to_json_object(in))
52  {
53  if(kv.first == "type")
54  {
55  irept irep = json2irep.convert_from_json(kv.second);
56  result.type = static_cast<typet &>(irep);
57  }
58  else if(kv.first == "value")
59  {
60  irept irep = json2irep.convert_from_json(kv.second);
61  result.value = static_cast<exprt &>(irep);
62  }
63  else if(kv.first == "location")
64  {
65  irept irep = json2irep.convert_from_json(kv.second);
66  result.location = static_cast<source_locationt &>(irep);
67  }
68  else if(kv.first == "name")
69  result.name = try_get_string(kv.second, "name");
70  else if(kv.first == "module")
71  result.module = try_get_string(kv.second, "module");
72  else if(kv.first == "baseName")
73  result.base_name = try_get_string(kv.second, "baseName");
74  else if(kv.first == "mode")
75  result.mode = try_get_string(kv.second, "mode");
76  else if(kv.first == "prettyName")
77  result.pretty_name = try_get_string(kv.second, "prettyName");
78  else if(kv.first == "isType")
79  result.is_type = try_get_bool(kv.second, "isType");
80  else if(kv.first == "isMacro")
81  result.is_macro = try_get_bool(kv.second, "isMacro");
82  else if(kv.first == "isExported")
83  result.is_exported = try_get_bool(kv.second, "isExported");
84  else if(kv.first == "isInput")
85  result.is_input = try_get_bool(kv.second, "isInput");
86  else if(kv.first == "isOutput")
87  result.is_output = try_get_bool(kv.second, "isOutput");
88  else if(kv.first == "isStateVar")
89  result.is_state_var = try_get_bool(kv.second, "isStateVar");
90  else if(kv.first == "isProperty")
91  result.is_property = try_get_bool(kv.second, "isProperty");
92  else if(kv.first == "isStaticLifetime")
93  result.is_static_lifetime = try_get_bool(kv.second, "isStaticLifetime");
94  else if(kv.first == "isThreadLocal")
95  result.is_thread_local = try_get_bool(kv.second, "isThreadLocal");
96  else if(kv.first == "isLvalue")
97  result.is_lvalue = try_get_bool(kv.second, "isLvalue");
98  else if(kv.first == "isFileLocal")
99  result.is_file_local = try_get_bool(kv.second, "isFileLocal");
100  else if(kv.first == "isExtern")
101  result.is_extern = try_get_bool(kv.second, "isExtern");
102  else if(kv.first == "isVolatile")
103  result.is_volatile = try_get_bool(kv.second, "isVolatile");
104  else if(kv.first == "isParameter")
105  result.is_parameter = try_get_bool(kv.second, "isParameter");
106  else if(kv.first == "isAuxiliary")
107  result.is_auxiliary = try_get_bool(kv.second, "isAuxiliary");
108  else if(kv.first == "isWeak")
109  result.is_weak = try_get_bool(kv.second, "isWeak");
110  else if(kv.first == "prettyType")
111  {
112  } // ignore
113  else if(kv.first == "prettyValue")
114  {
115  } // ignore
116  else
118  "symbol_from_json: unexpected key '" + kv.first + "'");
119  }
120 
121  return result;
122 }
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
Base class for all expressions.
Definition: expr.h:56
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:364
irept convert_from_json(const jsont &) const
Deserialize a JSON irep representation.
Definition: json_irep.cpp:95
Definition: json.h:27
bool is_false() const
Definition: json.h:76
std::string value
Definition: json.h:132
bool is_string() const
Definition: json.h:46
bool is_true() const
Definition: json.h:71
bool is_object() const
Definition: json.h:56
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_auxiliary
Definition: symbol.h:77
bool is_volatile
Definition: symbol.h:75
bool is_extern
Definition: symbol.h:74
bool is_macro
Definition: symbol.h:62
bool is_file_local
Definition: symbol.h:73
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
bool is_static_lifetime
Definition: symbol.h:70
bool is_property
Definition: symbol.h:67
bool is_parameter
Definition: symbol.h:76
bool is_thread_local
Definition: symbol.h:71
bool is_type
Definition: symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
bool is_state_var
Definition: symbol.h:66
bool is_output
Definition: symbol.h:65
typet type
Type of symbol.
Definition: symbol.h:31
bool is_weak
Definition: symbol.h:78
irep_idt name
The unique identifier.
Definition: symbol.h:40
bool is_exported
Definition: symbol.h:63
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
bool is_lvalue
Definition: symbol.h:72
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
bool is_input
Definition: symbol.h:64
The type of an expression, extends irept.
Definition: type.h:29
json_objectt & to_json_object(jsont &json)
Definition: json.h:442
static const std::string & try_get_string(const jsont &in, const std::string &key)
Return string value for a given key if present in the json object.
Definition: json_symbol.cpp:22
static bool try_get_bool(const jsont &in, const std::string &key)
Return boolean value for a given key if present in the json object.
Definition: json_symbol.cpp:34
symbolt symbol_from_json(const jsont &in)
Deserialise a json object to a symbolt.
Definition: json_symbol.cpp:45
Defines typet, type_with_subtypet and type_with_subtypest.