cprover
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 : in.object)
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 == "base_name")
73  result.base_name = try_get_string(kv.second, "base_name");
74  else if(kv.first == "mode")
75  result.mode = try_get_string(kv.second, "mode");
76  else if(kv.first == "pretty_name")
77  result.pretty_name = try_get_string(kv.second, "pretty_name");
78  else if(kv.first == "is_type")
79  result.is_type = try_get_bool(kv.second, "is_type");
80  else if(kv.first == "is_macro")
81  result.is_macro = try_get_bool(kv.second, "is_macro");
82  else if(kv.first == "is_exported")
83  result.is_exported = try_get_bool(kv.second, "is_exported");
84  else if(kv.first == "is_input")
85  result.is_input = try_get_bool(kv.second, "is_input");
86  else if(kv.first == "is_output")
87  result.is_output = try_get_bool(kv.second, "is_output");
88  else if(kv.first == "is_state_var")
89  result.is_state_var = try_get_bool(kv.second, "is_state_var");
90  else if(kv.first == "is_property")
91  result.is_property = try_get_bool(kv.second, "is_property");
92  else if(kv.first == "is_static_lifetime")
93  result.is_static_lifetime = try_get_bool(kv.second, "is_static_lifetime");
94  else if(kv.first == "is_thread_local")
95  result.is_thread_local = try_get_bool(kv.second, "is_thread_local");
96  else if(kv.first == "is_lvalue")
97  result.is_lvalue = try_get_bool(kv.second, "is_lvalue");
98  else if(kv.first == "is_file_local")
99  result.is_file_local = try_get_bool(kv.second, "is_file_local");
100  else if(kv.first == "is_extern")
101  result.is_extern = try_get_bool(kv.second, "is_extern");
102  else if(kv.first == "is_volatile")
103  result.is_volatile = try_get_bool(kv.second, "is_volatile");
104  else if(kv.first == "is_parameter")
105  result.is_parameter = try_get_bool(kv.second, "is_parameter");
106  else if(kv.first == "is_auxiliary")
107  result.is_auxiliary = try_get_bool(kv.second, "is_auxiliary");
108  else if(kv.first == "is_weak")
109  result.is_weak = try_get_bool(kv.second, "is_weak");
110  else
112  "symbol_from_json: unexpected key '" + kv.first + "'");
113  }
114 
115  return result;
116 }
exception_utils.h
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:62
symbolt::is_macro
bool is_macro
Definition: symbol.h:61
typet
The type of an expression, extends irept.
Definition: type.h:27
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
jsont::object
objectt object
Definition: json.h:132
deserialization_exceptiont
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
Definition: exception_utils.h:72
jsont::is_true
bool is_true() const
Definition: json.h:59
symbolt::is_input
bool is_input
Definition: symbol.h:62
exprt
Base class for all expressions.
Definition: expr.h:54
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
try_get_bool
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
jsont
Definition: json.h:23
json_irep.h
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
type.h
expr.h
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
jsont::is_string
bool is_string() const
Definition: json.h:39
try_get_string
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
source_location.h
symbolt::is_exported
bool is_exported
Definition: symbol.h:61
symbolt::is_parameter
bool is_parameter
Definition: symbol.h:67
source_locationt
Definition: source_location.h:20
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
symbolt::is_output
bool is_output
Definition: symbol.h:62
symbolt::is_extern
bool is_extern
Definition: symbol.h:66
jsont::is_false
bool is_false() const
Definition: json.h:64
symbolt::is_volatile
bool is_volatile
Definition: symbol.h:66
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:27
symbolt::is_type
bool is_type
Definition: symbol.h:61
symbolt::is_auxiliary
bool is_auxiliary
Definition: symbol.h:67
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
irept
Base class for tree-like data structures with sharing.
Definition: irep.h:156
json_irept
Definition: json_irep.h:20
jsont::is_object
bool is_object() const
Definition: json.h:49
symbolt::is_file_local
bool is_file_local
Definition: symbol.h:66
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
symbolt::is_weak
bool is_weak
Definition: symbol.h:67
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
symbolt::is_property
bool is_property
Definition: symbol.h:62
symbol_from_json
symbolt symbol_from_json(const jsont &in)
Deserialise a json object to a symbolt.
Definition: json_symbol.cpp:45
json_irept::convert_from_json
irept convert_from_json(const jsont &) const
Deserialize a JSON irep representation.
Definition: json_irep.cpp:100
jsont::value
std::string value
Definition: json.h:137
json_symbol.h