Skip to content

Commit 3cf4e3a

Browse files
author
Daniel Kroening
authored
Merge pull request #2178 from thomasspriggs/remove_java_bytecode_parse_treet_swap
 Remove `java_bytecode_parse_treet::classt::swap` and return using `optionalt` instead.
2 parents e5e0897 + eeb732f commit 3cf4e3a

File tree

6 files changed

+65
-83
lines changed

6 files changed

+65
-83
lines changed

‎jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp

Lines changed: 0 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -18,28 +18,6 @@ Author: Daniel Kroening, [email protected]
1818

1919
#include "expr2java.h"
2020

21-
void java_bytecode_parse_treet::classt::swap(
22-
classt &other)
23-
{
24-
other.name.swap(name);
25-
other.extends.swap(extends);
26-
std::swap(other.is_enum, is_enum);
27-
std::swap(other.enum_elements, enum_elements);
28-
std::swap(other.is_abstract, is_abstract);
29-
std::swap(other.is_public, is_public);
30-
std::swap(other.is_protected, is_protected);
31-
std::swap(other.is_private, is_private);
32-
std::swap(other.is_final, is_final);
33-
std::swap(other.signature, signature);
34-
other.implements.swap(implements);
35-
other.fields.swap(fields);
36-
other.methods.swap(methods);
37-
other.annotations.swap(annotations);
38-
std::swap(
39-
other.attribute_bootstrapmethods_read, attribute_bootstrapmethods_read);
40-
std::swap(other.lambda_method_handle_map, lambda_method_handle_map);
41-
}
42-
4321
void java_bytecode_parse_treet::output(std::ostream &out) const
4422
{
4523
parsed_class.output(out);

‎jbmc/src/java_bytecode/java_bytecode_parse_tree.h

Lines changed: 21 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,16 @@ Author: Daniel Kroening, [email protected]
2222
class java_bytecode_parse_treet
2323
{
2424
public:
25+
// Disallow copy construction and copy assignment, but allow move construction
26+
// and move assignment.
27+
#ifndef _MSC_VER // Ommit this on MS VC2013 as move is not supported.
28+
java_bytecode_parse_treet(const java_bytecode_parse_treet &) = delete;
29+
java_bytecode_parse_treet &
30+
operator=(const java_bytecode_parse_treet &) = delete;
31+
java_bytecode_parse_treet(java_bytecode_parse_treet &&) = default;
32+
java_bytecode_parse_treet &operator=(java_bytecode_parse_treet &&) = default;
33+
#endif
34+
2535
virtual ~java_bytecode_parse_treet() = default;
2636
class annotationt
2737
{
@@ -178,6 +188,17 @@ class java_bytecode_parse_treet
178188
class classt
179189
{
180190
public:
191+
classt() = default;
192+
193+
// Disallow copy construction and copy assignment, but allow move
194+
// construction and move assignment.
195+
#ifndef _MSC_VER // Ommit this on MS VC2013 as move is not supported.
196+
classt(const classt &) = delete;
197+
classt &operator=(const classt &) = delete;
198+
classt(classt &&) = default;
199+
classt &operator=(classt &&) = default;
200+
#endif
201+
181202
irep_idt name, extends;
182203
bool is_abstract=false;
183204
bool is_enum=false;
@@ -261,17 +282,10 @@ class java_bytecode_parse_treet
261282

262283
void output(std::ostream &out) const;
263284

264-
void swap(classt &other);
265285
};
266286

267287
classt parsed_class;
268288

269-
void swap(java_bytecode_parse_treet &other)
270-
{
271-
other.parsed_class.swap(parsed_class);
272-
other.class_refs.swap(class_refs);
273-
std::swap(loading_successful, other.loading_successful);
274-
}
275289

276290
void output(std::ostream &out) const;
277291

‎jbmc/src/java_bytecode/java_bytecode_parser.cpp

Lines changed: 11 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1688,26 +1688,25 @@ void java_bytecode_parsert::rmethod(classt &parsed_class)
16881688
rmethod_attribute(method);
16891689
}
16901690

1691-
bool java_bytecode_parse(
1692-
std::istream &istream,
1693-
java_bytecode_parse_treet &parse_tree,
1694-
message_handlert &message_handler)
1691+
optionalt<class java_bytecode_parse_treet>
1692+
java_bytecode_parse(std::istream &istream, message_handlert &message_handler)
16951693
{
16961694
java_bytecode_parsert java_bytecode_parser;
16971695
java_bytecode_parser.in=&istream;
16981696
java_bytecode_parser.set_message_handler(message_handler);
16991697

17001698
bool parser_result=java_bytecode_parser.parse();
17011699

1702-
parse_tree.swap(java_bytecode_parser.parse_tree);
1700+
if(parser_result)
1701+
{
1702+
return {};
1703+
}
17031704

1704-
return parser_result;
1705+
return std::move(java_bytecode_parser.parse_tree);
17051706
}
17061707

1707-
bool java_bytecode_parse(
1708-
const std::string &file,
1709-
java_bytecode_parse_treet &parse_tree,
1710-
message_handlert &message_handler)
1708+
optionalt<class java_bytecode_parse_treet>
1709+
java_bytecode_parse(const std::string &file, message_handlert &message_handler)
17111710
{
17121711
std::ifstream in(file, std::ios::binary);
17131712

@@ -1716,10 +1715,10 @@ bool java_bytecode_parse(
17161715
messaget message(message_handler);
17171716
message.error() << "failed to open input file `"
17181717
<< file << '\'' << messaget::eom;
1719-
return true;
1718+
return {};
17201719
}
17211720

1722-
return java_bytecode_parse(in, parse_tree, message_handler);
1721+
return java_bytecode_parse(in, message_handler);
17231722
}
17241723

17251724
/// Parses the local variable type table of a method. The LVTT holds generic

‎jbmc/src/java_bytecode/java_bytecode_parser.h

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -12,15 +12,12 @@ Author: Daniel Kroening, [email protected]
1212

1313
#include <iosfwd>
1414
#include <string>
15+
#include <util/optional.h>
1516

16-
bool java_bytecode_parse(
17-
const std::string &file,
18-
class java_bytecode_parse_treet &,
19-
class message_handlert &);
17+
optionalt<class java_bytecode_parse_treet>
18+
java_bytecode_parse(const std::string &file, class message_handlert &);
2019

21-
bool java_bytecode_parse(
22-
std::istream &,
23-
class java_bytecode_parse_treet &,
24-
class message_handlert &);
20+
optionalt<class java_bytecode_parse_treet>
21+
java_bytecode_parse(std::istream &, class message_handlert &);
2522

2623
#endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSER_H

‎jbmc/src/java_bytecode/java_class_loader.cpp

Lines changed: 8 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -97,11 +97,8 @@ optionalt<java_bytecode_parse_treet> java_class_loadert::get_class_from_jar(
9797
if(!data.has_value())
9898
return {};
9999

100-
java_bytecode_parse_treet parse_tree;
101100
std::istringstream istream(*data);
102-
if(java_bytecode_parse(istream, parse_tree, get_message_handler()))
103-
return {};
104-
return parse_tree;
101+
return java_bytecode_parse(istream, get_message_handler());
105102
}
106103

107104
static bool is_overlay_class(const java_bytecode_parse_treet::classt &c)
@@ -136,7 +133,7 @@ java_class_loadert::get_parse_tree(
136133
optionalt<java_bytecode_parse_treet> parse_tree =
137134
get_class_from_jar(class_name, jar_file, *index, class_loader_limit);
138135
if(parse_tree)
139-
parse_trees.push_back(*parse_tree);
136+
parse_trees.emplace_back(std::move(*parse_tree));
140137
}
141138

142139
// Then add core models
@@ -156,7 +153,7 @@ java_class_loadert::get_parse_tree(
156153
optionalt<java_bytecode_parse_treet> parse_tree =
157154
get_class_from_jar(class_name, core_models, *index, class_loader_limit);
158155
if(parse_tree)
159-
parse_trees.push_back(*parse_tree);
156+
parse_trees.emplace_back(std::move(*parse_tree));
160157
}
161158
}
162159

@@ -171,7 +168,7 @@ java_class_loadert::get_parse_tree(
171168
optionalt<java_bytecode_parse_treet> parse_tree =
172169
get_class_from_jar(class_name, cp_entry, *index, class_loader_limit);
173170
if(parse_tree)
174-
parse_trees.push_back(*parse_tree);
171+
parse_trees.emplace_back(std::move(*parse_tree));
175172
}
176173
else
177174
{
@@ -192,9 +189,10 @@ java_class_loadert::get_parse_tree(
192189
debug()
193190
<< "Getting class `" << class_name << "' from file " << full_path
194191
<< eom;
195-
java_bytecode_parse_treet parse_tree;
196-
if(!java_bytecode_parse(full_path, parse_tree, get_message_handler()))
197-
parse_trees.push_back(std::move(parse_tree));
192+
optionalt<java_bytecode_parse_treet> parse_tree =
193+
java_bytecode_parse(full_path, get_message_handler());
194+
if(parse_tree)
195+
parse_trees.emplace_back(std::move(*parse_tree));
198196
}
199197
}
200198
}

‎jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp

Lines changed: 20 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -33,17 +33,16 @@ SCENARIO(
3333
GIVEN(
3434
"A class with a static lambda variables from " + compiler + " compiler.")
3535
{
36-
java_bytecode_parse_treet parse_tree;
37-
java_bytecode_parse(
36+
optionalt<java_bytecode_parse_treet> parse_tree = java_bytecode_parse(
3837
"./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" +
3938
compiler + "_classes/StaticLambdas.class",
40-
parse_tree,
4139
message_handler);
4240
WHEN("Parsing that class")
4341
{
44-
REQUIRE(parse_tree.loading_successful);
45-
const java_bytecode_parse_treet::classt parsed_class =
46-
parse_tree.parsed_class;
42+
REQUIRE(parse_tree);
43+
REQUIRE(parse_tree->loading_successful);
44+
const java_bytecode_parse_treet::classt &parsed_class =
45+
parse_tree->parsed_class;
4746
REQUIRE(parsed_class.attribute_bootstrapmethods_read);
4847
REQUIRE(parsed_class.lambda_method_handle_map.size() == 12);
4948

@@ -345,17 +344,16 @@ SCENARIO(
345344
null_message_handlert message_handler;
346345
GIVEN("A method with local lambdas from " + compiler + " compiler.")
347346
{
348-
java_bytecode_parse_treet parse_tree;
349-
java_bytecode_parse(
347+
optionalt<java_bytecode_parse_treet> parse_tree = java_bytecode_parse(
350348
"./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" +
351349
compiler + "_classes/LocalLambdas.class",
352-
parse_tree,
353350
message_handler);
354351
WHEN("Parsing that class")
355352
{
356-
REQUIRE(parse_tree.loading_successful);
357-
const java_bytecode_parse_treet::classt parsed_class =
358-
parse_tree.parsed_class;
353+
REQUIRE(parse_tree);
354+
REQUIRE(parse_tree->loading_successful);
355+
const java_bytecode_parse_treet::classt &parsed_class =
356+
parse_tree->parsed_class;
359357
REQUIRE(parsed_class.attribute_bootstrapmethods_read);
360358
REQUIRE(parsed_class.lambda_method_handle_map.size() == 12);
361359

@@ -655,17 +653,16 @@ SCENARIO(
655653
"A class that has lambdas as member variables from " + compiler +
656654
" compiler.")
657655
{
658-
java_bytecode_parse_treet parse_tree;
659-
java_bytecode_parse(
656+
optionalt<java_bytecode_parse_treet> parse_tree = java_bytecode_parse(
660657
"./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" +
661658
compiler + "_classes/MemberLambdas.class",
662-
parse_tree,
663659
message_handler);
664660
WHEN("Parsing that class")
665661
{
666-
REQUIRE(parse_tree.loading_successful);
667-
const java_bytecode_parse_treet::classt parsed_class =
668-
parse_tree.parsed_class;
662+
REQUIRE(parse_tree);
663+
REQUIRE(parse_tree->loading_successful);
664+
const java_bytecode_parse_treet::classt &parsed_class =
665+
parse_tree->parsed_class;
669666
REQUIRE(parsed_class.attribute_bootstrapmethods_read);
670667
REQUIRE(parsed_class.lambda_method_handle_map.size() == 12);
671668

@@ -991,17 +988,16 @@ SCENARIO(
991988
"variables from " +
992989
compiler + " compiler.")
993990
{
994-
java_bytecode_parse_treet parse_tree;
995-
java_bytecode_parse(
991+
optionalt<java_bytecode_parse_treet> parse_tree = java_bytecode_parse(
996992
"./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" +
997993
compiler + "_classes/OuterMemberLambdas$Inner.class",
998-
parse_tree,
999994
message_handler);
1000995
WHEN("Parsing that class")
1001996
{
1002-
REQUIRE(parse_tree.loading_successful);
1003-
const java_bytecode_parse_treet::classt parsed_class =
1004-
parse_tree.parsed_class;
997+
REQUIRE(parse_tree);
998+
REQUIRE(parse_tree->loading_successful);
999+
const java_bytecode_parse_treet::classt &parsed_class =
1000+
parse_tree->parsed_class;
10051001
REQUIRE(parsed_class.attribute_bootstrapmethods_read);
10061002
REQUIRE(parsed_class.lambda_method_handle_map.size() == 3);
10071003

0 commit comments

Comments
 (0)