replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Equip json_arrayt and json_objectt with a full API to enable hiding 

As the comment said, various members of jsont should not need to be public.
This commit is contained in:
Michael Tautschnig 2018-12-18 19:01:39 +00:00
parent 2be33443b2
commit 5167bcb818
12 changed files with 182 additions and 88 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
jbmc/src/java_bytecode/java_bytecode_language.cpp
View File

@ -161,7 +161,7 @@ void java_bytecode_languaget::set_language_options(const optionst &options)
throw "the JSON file has a wrong format";
// add jars from JSON config file to classpath
for(const jsont &file_entry : include_files.array)
for(const jsont &file_entry : to_json_array(include_files))
{
DATA_INVARIANT(
file_entry.is_string() && has_suffix(file_entry.value, ".jar"),

2
jbmc/src/java_bytecode/java_class_loader_limit.cpp
View File

@ -74,7 +74,7 @@ void java_class_loader_limitt::setup_class_load_limit(
jsont include_files=json_cp_config["classFiles"];
if(!include_files.is_null() && !include_files.is_array())
throw "the JSON file has a wrong format";
for(const jsont &file_entry : include_files.array)
for(const jsont &file_entry : to_json_array(include_files))
{
assert(file_entry.is_string());
set_matcher.insert(file_entry.value);

2
src/goto-analyzer/taint_analysis.cpp
View File

@ -358,7 +358,7 @@ bool taint_analysist::operator()(
json["file"] = json_stringt(i_it->source_location.get_file());
json["line"]=
json_numbert(id2string(i_it->source_location.get_line()));
json_result.array.push_back(json);
json_result.push_back(json);
}
else
{

23
src/goto-analyzer/taint_parser.cpp
View File

@ -40,28 +40,25 @@ bool taint_parser(
return true;
}
for(jsont::arrayt::const_iterator
it=json.array.begin();
it!=json.array.end();
it++)
for(const auto &taint_spec : to_json_array(json))
{
if(!it->is_object())
if(!taint_spec.is_object())
{
messaget message(message_handler);
message.error() << "expecting an array of objects "
<< "in the taint file, but got "
<< *it << messaget::eom;
<< "in the taint file, but got " << taint_spec
<< messaget::eom;
return true;
}
taint_parse_treet::rulet rule;
const std::string kind=(*it)["kind"].value;
const std::string function=(*it)["function"].value;
const std::string where=(*it)["where"].value;
const std::string taint=(*it)["taint"].value;
const std::string message=(*it)["message"].value;
const std::string id=(*it)["id"].value;
const std::string kind = taint_spec["kind"].value;
const std::string function = taint_spec["function"].value;
const std::string where = taint_spec["where"].value;
const std::string taint = taint_spec["taint"].value;
const std::string message = taint_spec["message"].value;
const std::string id = taint_spec["id"].value;
if(kind=="source")
rule.kind=taint_parse_treet::rulet::SOURCE;

6
src/goto-analyzer/unreachable_instructions.cpp
View File

@ -197,7 +197,7 @@ void unreachable_instructions(
}
}
if(json && !json_result.array.empty())
if(json && !json_result.empty())
os << json_result << '\n';
}
@ -239,7 +239,7 @@ bool static_unreachable_instructions(
}
}
if(options.get_bool_option("json") && !json_result.array.empty())
if(options.get_bool_option("json") && !json_result.empty())
out << json_result << '\n';
else if(options.get_bool_option("xml"))
out << xml_result << '\n';
@ -369,7 +369,7 @@ static void list_functions(
}
}
if(options.get_bool_option("json") && !json_result.array.empty())
if(options.get_bool_option("json") && !json_result.empty())
os << json_result << '\n';
else if(options.get_bool_option("xml"))
os << xml_result << '\n';

91
src/goto-cc/linker_script_merge.cpp
View File

@ -400,7 +400,7 @@ int linker_script_merget::ls_data2instructions(
{
goto_programt::instructionst initialize_instructions=gp.instructions;
std::map<irep_idt, std::size_t> truncated_symbols;
for(auto &d : data["regions"].array)
for(auto &d : to_json_array(data["regions"]))
{
bool has_end=d["has-end-symbol"].is_true();
@ -446,11 +446,13 @@ int linker_script_merget::ls_data2instructions(
// Since the value of the pointer will be a random CBMC address, write a
// note about the real address in the object file
auto it=std::find_if(data["addresses"].array.begin(),
data["addresses"].array.end(),
[&d](const jsont &add)
{ return add["sym"].value==d["start-symbol"].value; });
if(it==data["addresses"].array.end())
auto it = std::find_if(
to_json_array(data["addresses"]).begin(),
to_json_array(data["addresses"]).end(),
[&d](const jsont &add) {
return add["sym"].value == d["start-symbol"].value;
});
if(it == to_json_array(data["addresses"]).end())
{
error() << "Start: Could not find address corresponding to symbol '"
<< d["start-symbol"].value << "' (start of section)" << eom;
@ -481,12 +483,12 @@ int linker_script_merget::ls_data2instructions(
linker_values[d["end-symbol"].value]=std::make_pair(end_sym, array_end);
auto entry = std::find_if(
data["addresses"].array.begin(),
data["addresses"].array.end(),
to_json_array(data["addresses"]).begin(),
to_json_array(data["addresses"]).end(),
[&d](const jsont &add) {
return add["sym"].value == d["end-symbol"].value;
});
if(entry == data["addresses"].array.end())
if(entry == to_json_array(data["addresses"]).end())
{
error() << "Could not find address corresponding to symbol '"
<< d["end-symbol"].value << "' (end of section)" << eom;
@ -539,7 +541,7 @@ int linker_script_merget::ls_data2instructions(
// address. These will have been declared extern too, so we need to give them
// a value also. Here, we give them the actual value that they have in the
// object file, since we're not assigning any object to them.
for(const auto &d : data["addresses"].array)
for(const auto &d : to_json_array(data["addresses"]))
{
auto it=linker_values.find(irep_idt(d["sym"].value));
if(it!=linker_values.end())
@ -591,7 +593,7 @@ int linker_script_merget::ls_data2instructions(
#else
{
goto_programt::instructionst initialize_instructions=gp.instructions;
for(const auto &d : data["regions"].array)
for(const auto &d : to_json_array(data["regions"]))
{
unsigned start=safe_string2unsigned(d["start"].value);
unsigned size=safe_string2unsigned(d["size"].value);
@ -623,7 +625,7 @@ int linker_script_merget::ls_data2instructions(
symbol_table.add(sym);
}
for(const auto &d : data["addresses"].array)
for(const auto &d : to_json_array(data["addresses"]))
{
source_locationt loc;
loc.set_file(linker_script);
@ -738,38 +740,51 @@ int linker_script_merget::goto_and_object_mismatch(
int linker_script_merget::linker_data_is_malformed(const jsont &data) const
{
if(!data.is_object())
return true;
const json_objectt &data_object = to_json_object(data);
return (
!(data.is_object() && data.object.find("regions") != data.object.end() &&
data.object.find("addresses") != data.object.end() &&
!(data_object.find("regions") != data_object.end() &&
data_object.find("addresses") != data_object.end() &&
data["regions"].is_array() && data["addresses"].is_array() &&
std::all_of(
data["addresses"].array.begin(),
data["addresses"].array.end(),
to_json_array(data["addresses"]).begin(),
to_json_array(data["addresses"]).end(),
[](const jsont &j) {
return j.is_object() && j.object.find("val") != j.object.end() &&
j.object.find("sym") != j.object.end() &&
j["val"].is_number() && j["sym"].is_string();
if(!j.is_object())
return false;
const json_objectt &address = to_json_object(j);
return address.find("val") != address.end() &&
address.find("sym") != address.end() &&
address["val"].is_number() && address["sym"].is_string();
}) &&
std::all_of(
data["regions"].array.begin(),
data["regions"].array.end(),
to_json_array(data["regions"]).begin(),
to_json_array(data["regions"]).end(),
[](const jsont &j) {
return j.is_object() && j.object.find("start") != j.object.end() &&
j.object.find("size") != j.object.end() &&
j.object.find("annot") != j.object.end() &&
j.object.find("commt") != j.object.end() &&
j.object.find("start-symbol") != j.object.end() &&
j.object.find("has-end-symbol") != j.object.end() &&
j.object.find("section") != j.object.end() &&
j["start"].is_number() && j["size"].is_number() &&
j["annot"].is_string() && j["start-symbol"].is_string() &&
j["section"].is_string() && j["commt"].is_string() &&
((j["has-end-symbol"].is_true() &&
j.object.find("end-symbol") != j.object.end() &&
j["end-symbol"].is_string()) ||
(j["has-end-symbol"].is_false() &&
j.object.find("size-symbol") != j.object.end() &&
j.object.find("end-symbol") == j.object.end() &&
j["size-symbol"].is_string()));
if(!j.is_object())
return false;
const json_objectt &region = to_json_object(j);
return region.find("start") != region.end() &&
region.find("size") != region.end() &&
region.find("annot") != region.end() &&
region.find("commt") != region.end() &&
region.find("start-symbol") != region.end() &&
region.find("has-end-symbol") != region.end() &&
region.find("section") != region.end() &&
region["start"].is_number() && region["size"].is_number() &&
region["annot"].is_string() &&
region["start-symbol"].is_string() &&
region["section"].is_string() && region["commt"].is_string() &&
((region["has-end-symbol"].is_true() &&
region.find("end-symbol") != region.end() &&
region["end-symbol"].is_string()) ||
(region["has-end-symbol"].is_false() &&
region.find("size-symbol") != region.end() &&
region.find("end-symbol") == region.end() &&
region["size-symbol"].is_string()));
})));
}

2
src/json-symtab-language/json_symbol.cpp
View File

@ -48,7 +48,7 @@ symbolt symbol_from_json(const jsont &in)
throw deserialization_exceptiont("symbol_from_json takes an object");
symbolt result;
json_irept json2irep(true);
for(const auto &kv : in.object)
for(const auto &kv : to_json_object(in))
{
if(kv.first == "type")
{

2
src/json-symtab-language/json_symbol_table.cpp
View File

@ -18,7 +18,7 @@ void symbol_table_from_json(const jsont &in, symbol_tablet &symbol_table)
if(!in.is_array())
throw deserialization_exceptiont(
"symbol_table_from_json: JSON input must be an array");
for(const auto &js_symbol : in.array)
for(const auto &js_symbol : to_json_array(in))
{
symbolt deserialized = symbol_from_json(js_symbol);
if(symbol_table.add(deserialized))

4
src/json/parser.y
View File

@ -90,7 +90,7 @@ key_value_pair:
{
jsont tmp;
json_parser.pop(tmp);
json_parser.top().object[json_parser.top().value].swap(tmp);
to_json_object(json_parser.top())[json_parser.top().value].swap(tmp);
json_parser.top().value.clear(); // end abuse
}
;
@ -109,7 +109,7 @@ array_value:
{
jsont tmp;
json_parser.pop(tmp);
json_parser.top().array.push_back(tmp);
to_json_array(json_parser.top()).push_back(tmp);
}
;

116
src/util/json.h
View File

@ -22,6 +22,10 @@ class json_arrayt;
class jsont
{
protected:
typedef std::vector<jsont> arrayt;
typedef std::map<std::string, jsont> objectt;
public:
enum class kindt
{
@ -112,7 +116,17 @@ public:
static const jsont null_json_object;
static void output_key(std::ostream &out, const std::string &key);
static void
output_object(std::ostream &out, const objectt &object, unsigned indent);
std::string value;
protected:
arrayt array;
objectt object;
static void escape_string(const std::string &, std::ostream &);
explicit jsont(kindt _kind):kind(_kind)
@ -122,19 +136,6 @@ protected:
jsont(kindt _kind, std::string _value) : kind(_kind), value(std::move(_value))
{
}
public:
// should become protected
typedef std::vector<jsont> arrayt;
arrayt array;
typedef std::map<std::string, jsont> objectt;
objectt object;
static void
output_object(std::ostream &out, const objectt &object, unsigned indent);
static void output_key(std::ostream &out, const std::string &key);
std::string value;
};
inline std::ostream &operator<<(std::ostream &out, const jsont &src)
@ -160,12 +161,23 @@ public:
return array.size();
}
bool empty() const
{
return array.empty();
}
jsont &push_back(const jsont &json)
{
array.push_back(json);
return array.back();
}
jsont &push_back(jsont &&json)
{
array.push_back(std::move(json));
return array.back();
}
jsont &push_back()
{
array.push_back(jsont());
@ -178,32 +190,32 @@ public:
array.emplace_back(std::forward<argumentst>(arguments)...);
}
std::vector<jsont>::iterator begin()
arrayt::iterator begin()
{
return array.begin();
}
std::vector<jsont>::const_iterator begin() const
arrayt::const_iterator begin() const
{
return array.begin();
}
std::vector<jsont>::const_iterator cbegin() const
arrayt::const_iterator cbegin() const
{
return array.cbegin();
}
std::vector<jsont>::iterator end()
arrayt::iterator end()
{
return array.end();
}
std::vector<jsont>::const_iterator end() const
arrayt::const_iterator end() const
{
return array.end();
}
std::vector<jsont>::const_iterator cend() const
arrayt::const_iterator cend() const
{
return array.cend();
}
@ -261,6 +273,48 @@ public:
else
return it->second;
}
objectt::iterator find(const std::string &key)
{
return object.find(key);
}
objectt::const_iterator find(const std::string &key) const
{
return object.find(key);
}
objectt::iterator begin()
{
return object.begin();
}
objectt::const_iterator begin() const
{
return object.begin();
}
objectt::const_iterator cbegin() const
{
return object.cbegin();
}
objectt::iterator end()
{
return object.end();
}
objectt::const_iterator end() const
{
return object.end();
}
objectt::const_iterator cend() const
{
return object.cend();
}
typedef jsont value_type; // NOLINT(readability/identifiers)
};
class json_truet:public jsont
@ -287,10 +341,34 @@ inline json_arrayt &jsont::make_array()
return static_cast<json_arrayt &>(*this);
}
inline json_arrayt &to_json_array(jsont &json)
{
PRECONDITION(json.kind == jsont::kindt::J_ARRAY);
return static_cast<json_arrayt &>(json);
}
inline const json_arrayt &to_json_array(const jsont &json)
{
PRECONDITION(json.kind == jsont::kindt::J_ARRAY);
return static_cast<const json_arrayt &>(json);
}
inline json_objectt &jsont::make_object()
{
kind=kindt::J_OBJECT;
return static_cast<json_objectt &>(*this);
}
inline json_objectt &to_json_object(jsont &json)
{
PRECONDITION(json.kind == jsont::kindt::J_OBJECT);
return static_cast<json_objectt &>(json);
}
inline const json_objectt &to_json_object(const jsont &json)
{
PRECONDITION(json.kind == jsont::kindt::J_OBJECT);
return static_cast<const json_objectt &>(json);
}
#endif // CPROVER_UTIL_JSON_H

8
src/util/json_irep.cpp
View File

@ -98,7 +98,7 @@ void json_irept::convert_named_sub_tree(
irept json_irept::convert_from_json(const jsont &in) const
{
std::vector<std::string> have_keys;
for(const auto &keyval : in.object)
for(const auto &keyval : to_json_object(in))
have_keys.push_back(keyval.first);
std::sort(have_keys.begin(), have_keys.end());
if(have_keys!=std::vector<std::string>{"comment", "id", "namedSub", "sub"})
@ -110,13 +110,13 @@ irept json_irept::convert_from_json(const jsont &in) const
irept out(in["id"].value);
for(const auto &sub : in["sub"].array)
for(const auto &sub : to_json_array(in["sub"]))
out.get_sub().push_back(convert_from_json(sub));
for(const auto &named_sub : in["namedSub"].object)
for(const auto &named_sub : to_json_object(in["namedSub"]))
out.add(named_sub.first)=convert_from_json(named_sub.second);
for(const auto &comment : in["comment"].object)
for(const auto &comment : to_json_object(in["comment"]))
out.add(comment.first)=convert_from_json(comment.second);
return out;

12
unit/json/json_parser.cpp
View File

@ -49,8 +49,10 @@ SCENARIO("Loading JSON files")
{
REQUIRE_FALSE(valid_parse_error);
REQUIRE(valid_json.is_object());
REQUIRE(valid_json.object.find("hello") != valid_json.object.end());
REQUIRE(valid_json.object["hello"].value == "world");
const json_objectt &json_object = to_json_object(valid_json);
REQUIRE(json_object.find("hello") != json_object.end());
REQUIRE(json_object["hello"].value == "world");
}
}
}
@ -64,8 +66,10 @@ SCENARIO("Loading JSON files")
{
REQUIRE_FALSE(valid_parse_error);
REQUIRE(valid_json.is_object());
REQUIRE(valid_json.object.find("hello") != valid_json.object.end());
REQUIRE(valid_json.object["hello"].value == "world");
const json_objectt &json_object = to_json_object(valid_json);
REQUIRE(json_object.find("hello") != json_object.end());
REQUIRE(json_object["hello"].value == "world");
AND_WHEN("Loading the invalid JSON file")
{
jsont invalid_json;