Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove all references to optionalt #8099

Merged
merged 1 commit into from
Dec 15, 2023
Merged

Remove all references to optionalt #8099

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion .clang-format-ignore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
jbmc/src/miniz/miniz.cpp
src/cprover/wcwidth.c
src/nonstd/optional.hpp
unit/catch/catch.hpp
2 changes: 1 addition & 1 deletion jbmc/src/janalyzer/janalyzer_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -445,7 +445,7 @@ int janalyzer_parse_optionst::perform_analysis(
}
else
{
optionalt<std::string> json_file;
std::optional<std::string> json_file;
if(cmdline.isset("json"))
json_file = cmdline.get_value("json");
bool result = taint_analysis(
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -677,7 +677,7 @@ used. Under eager loading
\ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, lazy_class_to_declared_symbols_mapt &, message_handlert &)
is called once for each method listed in method_bytecode (described above). This
then calls
\ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, optionalt<ci_lazy_methods_neededt>, lazy_class_to_declared_symbols_mapt &, message_handlert &);
\ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, std::optional<ci_lazy_methods_neededt>, lazy_class_to_declared_symbols_mapt &, message_handlert &);

without a ci_lazy_methods_neededt object, which calls
\ref java_bytecode_convert_method, passing in the method parse tree. This in
Expand Down
28 changes: 14 additions & 14 deletions jbmc/src/java_bytecode/assignments_from_json.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ struct object_creation_infot

/// Where runtime types differ from compile-time types, we need to mark the
/// runtime types as needed by lazy methods.
optionalt<ci_lazy_methods_neededt> &needed_lazy_methods;
std::optional<ci_lazy_methods_neededt> &needed_lazy_methods;

/// Map to keep track of reference-equal objects. Each entry has an ID (such
/// that any two reference-equal objects have the same ID) and the expression
Expand Down Expand Up @@ -117,7 +117,7 @@ static bool is_enum_with_type_equal_to_declaring_type(
/// A runtime type that is different from the objects compile-time type should
/// be specified in `json` in this way.
/// Type values are of the format "my.package.name.ClassName".
static optionalt<std::string> get_type(const jsont &json)
static std::optional<std::string> get_type(const jsont &json)
{
if(!json.is_object())
return {};
Expand Down Expand Up @@ -267,9 +267,9 @@ static jsont get_untyped_string(const jsont &json)
/// \param symbol_table: used to look up the type given its name.
/// \return runtime type of the object, if specified by at least one of the
/// parameters.
static optionalt<java_class_typet> runtime_type(
static std::optional<java_class_typet> runtime_type(
const jsont &json,
const optionalt<std::string> &type_from_array,
const std::optional<std::string> &type_from_array,
const symbol_table_baset &symbol_table)
{
const auto type_from_json = get_type(json);
Expand Down Expand Up @@ -304,9 +304,9 @@ static optionalt<java_class_typet> runtime_type(
/// field, this takes priority over \p type_from_array.
/// \param type_from_array: may contain a type name from a containing array.
/// \return if the type of an array was given, the type of its elements.
static optionalt<std::string> element_type_from_array_type(
static std::optional<std::string> element_type_from_array_type(
const jsont &json,
const optionalt<std::string> &type_from_array)
const std::optional<std::string> &type_from_array)
{
if(const auto json_array_type = get_type(json))
{
Expand All @@ -332,7 +332,7 @@ static optionalt<std::string> element_type_from_array_type(
code_with_references_listt assign_from_json_rec(
const exprt &expr,
const jsont &json,
const optionalt<std::string> &type_from_array,
const std::optional<std::string> &type_from_array,
object_creation_infot &info);

/// One of the base cases (primitive case) of the recursion.
Expand Down Expand Up @@ -392,7 +392,7 @@ static code_frontend_assignt assign_null(const exprt &expr)
static code_with_references_listt assign_array_data_component_from_json(
const exprt &expr,
const jsont &json,
const optionalt<std::string> &type_from_array,
const std::optional<std::string> &type_from_array,
object_creation_infot &info)
{
const auto &java_class_type = followed_class_type(expr, info.symbol_table);
Expand All @@ -411,7 +411,7 @@ static code_with_references_listt assign_array_data_component_from_json(
code_frontend_assignt{array_init_data, data_member_expr, info.loc});

size_t index = 0;
const optionalt<std::string> inferred_element_type =
const std::optional<std::string> inferred_element_type =
element_type_from_array_type(json, type_from_array);
const json_arrayt json_array = get_untyped_array(json, element_type);
for(auto it = json_array.begin(); it < json_array.end(); it++, index++)
Expand Down Expand Up @@ -457,7 +457,7 @@ static std::pair<code_with_references_listt, exprt>
assign_det_length_array_from_json(
const exprt &expr,
const jsont &json,
const optionalt<std::string> &type_from_array,
const std::optional<std::string> &type_from_array,
object_creation_infot &info)
{
PRECONDITION(is_java_array_type(expr.type()));
Expand Down Expand Up @@ -486,7 +486,7 @@ static code_with_references_listt assign_nondet_length_array_from_json(
const exprt &array,
const jsont &json,
const exprt &given_length_expr,
const optionalt<std::string> &type_from_array,
const std::optional<std::string> &type_from_array,
object_creation_infot &info)
{
PRECONDITION(is_java_array_type(array.type()));
Expand Down Expand Up @@ -793,7 +793,7 @@ static get_or_create_reference_resultt get_or_create_reference(
static code_with_references_listt assign_reference_from_json(
const exprt &expr,
const jsont &json,
const optionalt<std::string> &type_from_array,
const std::optional<std::string> &type_from_array,
object_creation_infot &info)
{
const std::string &id = has_enum_type(expr, info.symbol_table)
Expand Down Expand Up @@ -849,7 +849,7 @@ static code_with_references_listt assign_reference_from_json(
code_with_references_listt assign_from_json_rec(
const exprt &expr,
const jsont &json,
const optionalt<std::string> &type_from_array,
const std::optional<std::string> &type_from_array,
object_creation_infot &info)
{
code_with_references_listt result;
Expand Down Expand Up @@ -915,7 +915,7 @@ code_with_references_listt assign_from_json(
const jsont &json,
const irep_idt &function_id,
symbol_table_baset &symbol_table,
optionalt<ci_lazy_methods_neededt> &needed_lazy_methods,
std::optional<ci_lazy_methods_neededt> &needed_lazy_methods,
size_t max_user_array_length,
std::unordered_map<std::string, object_creation_referencet> &references)
{
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/assignments_from_json.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,7 @@ code_with_references_listt assign_from_json(
const jsont &json,
const irep_idt &function_id,
symbol_table_baset &symbol_table,
optionalt<ci_lazy_methods_neededt> &needed_lazy_methods,
std::optional<ci_lazy_methods_neededt> &needed_lazy_methods,
size_t max_user_array_length,
std::unordered_map<std::string, object_creation_referencet> &references);

Expand Down
3 changes: 2 additions & 1 deletion jbmc/src/java_bytecode/ci_lazy_methods.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,8 @@ class method_bytecodet
const java_bytecode_parse_treet::methodt &method;
};

typedef optionalt<std::reference_wrapper<const class_method_and_bytecodet>>
typedef std::optional<
std::reference_wrapper<const class_method_and_bytecodet>>
opt_reft;

private:
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ void ci_lazy_methods_neededt::add_cprover_nondet_initialize_if_it_exists(
const irep_idt &class_id)
{
resolve_inherited_componentt resolve_inherited_component{symbol_table};
optionalt<resolve_inherited_componentt::inherited_componentt>
std::optional<resolve_inherited_componentt::inherited_componentt>
cprover_nondet_initialize = resolve_inherited_component(
class_id, "cproverNondetInitialize:()V", true);

Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/code_with_references.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ struct object_creation_referencet
/// This should only be set once the actual elements of the array have been
/// seen, not the first time an `@ref` have been seen, only when `@id` is
/// seen.
optionalt<exprt> array_length;
std::optional<exprt> array_length;
};

/// Base class for code which can contain references which can get replaced
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/generic_parameter_specialization_map.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ void generic_parameter_specialization_mapt::pop(std::size_t container_index)
container_to_specializations.at(container_index).pop();
}

optionalt<reference_typet>
std::optional<reference_typet>
generic_parameter_specialization_mapt::pop(const irep_idt &parameter_name)
{
const auto types_it = param_to_container.find(parameter_name);
Expand Down
4 changes: 2 additions & 2 deletions jbmc/src/java_bytecode/generic_parameter_specialization_map.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,8 +53,8 @@ class generic_parameter_specialization_mapt
/// a given type parameter
/// \param parameter_name: The name of the type parameter
/// \returns: The specialization for the given type parameter, if there was
/// one before the pop, or an empty optionalt if the stack was empty
optionalt<reference_typet> pop(const irep_idt &parameter_name);
/// one before the pop, or an empty std::optional if the stack was empty
std::optional<reference_typet> pop(const irep_idt &parameter_name);

/// A wrapper for a generic_parameter_specialization_mapt and a namespacet
/// that can be output to a stream
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ class generic_parameter_specialization_map_keyst
/// Generic parameter specialization map to modify
generic_parameter_specialization_mapt &generic_parameter_specialization_map;
/// Key of the container to pop on destruction
optionalt<std::size_t> container_id;
std::optional<std::size_t> container_id;

public:
/// Initialize a generic-parameter-specialization-map entry owner operating
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/jar_file.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ jar_filet &jar_filet::operator=(jar_filet &&other)
return *this;
}

optionalt<std::string> jar_filet::get_entry(const std::string &name)
std::optional<std::string> jar_filet::get_entry(const std::string &name)
{
const auto entry=m_name_to_index.find(name);
if(entry==m_name_to_index.end())
Expand Down
11 changes: 5 additions & 6 deletions jbmc/src/java_bytecode/jar_file.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,14 +9,13 @@ Author: Diffblue Ltd
#ifndef CPROVER_JAVA_BYTECODE_JAR_FILE_H
#define CPROVER_JAVA_BYTECODE_JAR_FILE_H

#include <unordered_map>
#include "mz_zip_archive.h"

#include <optional>
#include <string>
#include <unordered_map>
#include <vector>

#include <util/optional.h>
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⛏️ Shouldn't this be replaced by #include <optional>? If this is working at the moment, I'd guess it was down to transitive includes.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seemed to work fine on my Ubuntu 20.04, but other OS/compiler combinations indeed make those includes necessary. I had naively assumed that standard library headers would likely (transitively) include that anyway, but as experimenting shows that's not always the case. So, yes, I may well end up putting this back in.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good to see this being fixed.

I'd prefer to avoid relying on transitive header includes where possible. With optional as an example my reasoning goes something like -

  1. Header "A" depends on optional so #include <optional> is added to it.
  2. .cpp file "B" depends on header "A" and uses std::optional in its implementation. It therefore depends on optional, but as this .cpp already includes header "A" #include <optional> is not added to it.
  3. Maintainer of header "A" decides they no longer need to depend on optional. Lets say they were using it for the type of a private member function rather than as part of the exposed API. They remove the #include <optional> from header "A", because it no longer needs it itself.
  4. The compilation of .cpp "B" now fails. This means that the maintainer of header "A" now needs to either add the include to the .cpp file, or to leave the extra include in their header.

Leaving the extra include in could potentially extend compile times. Adding it to the .cpp increases the number of changes in their PR and potentially requires approval from more code owners. The decision and additional work could have been avoided if the reliance on transitive includes had been avoided.


#include "mz_zip_archive.h"

/// Class representing a .jar archive. Uses miniz to decompress and index
/// archive.
class jar_filet final
Expand All @@ -42,7 +41,7 @@ class jar_filet final
/// Get contents of a file in the jar archive.
/// Returns nullopt if file doesn't exist.
/// \param filename: Name of the file in the archive
optionalt<std::string> get_entry(const std::string &filename);
std::optional<std::string> get_entry(const std::string &filename);

/// Get contents of the Manifest file in the jar archive as a key-value map
/// (both as strings)
Expand Down
12 changes: 6 additions & 6 deletions jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -186,8 +186,8 @@ class java_bytecode_convert_classt
/// \param signature: Signature of the class
/// \return Reference of the generic superclass, or empty if the superclass
/// is not generic
static optionalt<std::string>
extract_generic_superclass_reference(const optionalt<std::string> &signature)
static std::optional<std::string> extract_generic_superclass_reference(
const std::optional<std::string> &signature)
{
if(signature.has_value())
{
Expand Down Expand Up @@ -226,8 +226,8 @@ extract_generic_superclass_reference(const optionalt<std::string> &signature)
/// \param interface_name: The interface name
/// \return Reference of the generic interface, or empty if the interface
/// is not generic
static optionalt<std::string> extract_generic_interface_reference(
const optionalt<std::string> &signature,
static std::optional<std::string> extract_generic_interface_reference(
const std::optional<std::string> &signature,
const std::string &interface_name)
{
if(signature.has_value())
Expand Down Expand Up @@ -355,7 +355,7 @@ void java_bytecode_convert_classt::convert(
// including the generic info in its signature
// e.g., signature for class 'A<T>' that extends
// 'Generic<Integer>' is '<T:Ljava/lang/Object;>LGeneric<LInteger;>;'
const optionalt<std::string> &superclass_ref =
const std::optional<std::string> &superclass_ref =
extract_generic_superclass_reference(c.signature);
if(superclass_ref.has_value())
{
Expand Down Expand Up @@ -397,7 +397,7 @@ void java_bytecode_convert_classt::convert(
// including the generic info in its signature
// e.g., signature for class 'A implements GenericInterface<Integer>' is
// 'Ljava/lang/Object;LGenericInterface<LInteger;>;'
const optionalt<std::string> interface_ref =
const std::optional<std::string> interface_ref =
extract_generic_interface_reference(c.signature, id2string(interface));
if(interface_ref.has_value())
{
Expand Down
12 changes: 6 additions & 6 deletions jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -228,7 +228,7 @@ exprt java_bytecode_convert_methodt::variable(
/// \return the constructed member type
java_method_typet member_type_lazy(
const std::string &descriptor,
const optionalt<std::string> &signature,
const std::optional<std::string> &signature,
const std::string &class_name,
const std::string &method_name,
message_handlert &message_handler)
Expand Down Expand Up @@ -534,7 +534,7 @@ void create_parameter_symbols(
void java_bytecode_convert_methodt::convert(
const symbolt &class_symbol,
const methodt &m,
const optionalt<prefix_filtert> &method_context)
const std::optional<prefix_filtert> &method_context)
{
// Construct the fully qualified method name
// (e.g. "my.package.ClassName.myMethodName:(II)I") and query the symbol table
Expand Down Expand Up @@ -1263,7 +1263,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
}
}

optionalt<codet> catch_instruction;
std::optional<codet> catch_instruction;

if(catch_type!=typet())
{
Expand Down Expand Up @@ -3083,7 +3083,7 @@ code_blockt java_bytecode_convert_methodt::convert_astore(
return block;
}

optionalt<exprt> java_bytecode_convert_methodt::convert_invoke_dynamic(
std::optional<exprt> java_bytecode_convert_methodt::convert_invoke_dynamic(
const source_locationt &location,
std::size_t instruction_address,
const exprt &arg0,
Expand Down Expand Up @@ -3282,11 +3282,11 @@ void java_bytecode_convert_method(
message_handlert &message_handler,
size_t max_array_length,
bool throw_assertion_error,
optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
std::optional<ci_lazy_methods_neededt> needed_lazy_methods,
java_string_library_preprocesst &string_preprocess,
const class_hierarchyt &class_hierarchy,
bool threading_support,
const optionalt<prefix_filtert> &method_context,
const std::optional<prefix_filtert> &method_context,
bool assert_no_exceptions_thrown)

{
Expand Down
4 changes: 2 additions & 2 deletions jbmc/src/java_bytecode/java_bytecode_convert_method.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,11 +31,11 @@ void java_bytecode_convert_method(
message_handlert &message_handler,
size_t max_array_length,
bool throw_assertion_error,
optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
std::optional<ci_lazy_methods_neededt> needed_lazy_methods,
java_string_library_preprocesst &string_preprocess,
const class_hierarchyt &class_hierarchy,
bool threading_support,
const optionalt<prefix_filtert> &method_context,
const std::optional<prefix_filtert> &method_context,
bool assert_no_exceptions_thrown);

void create_method_stub_symbol(
Expand Down
10 changes: 5 additions & 5 deletions jbmc/src/java_bytecode/java_bytecode_convert_method_class.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ class java_bytecode_convert_methodt
message_handlert &_message_handler,
size_t _max_array_length,
bool throw_assertion_error,
optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
std::optional<ci_lazy_methods_neededt> needed_lazy_methods,
java_string_library_preprocesst &_string_preprocess,
const class_hierarchyt &class_hierarchy,
bool threading_support,
Expand Down Expand Up @@ -69,7 +69,7 @@ class java_bytecode_convert_methodt
void operator()(
const symbolt &class_symbol,
const methodt &method,
const optionalt<prefix_filtert> &method_context)
const std::optional<prefix_filtert> &method_context)
{
convert(class_symbol, method, method_context);
}
Expand All @@ -84,7 +84,7 @@ class java_bytecode_convert_methodt
const bool throw_assertion_error;
const bool assert_no_exceptions_thrown;
const bool threading_support;
optionalt<ci_lazy_methods_neededt> needed_lazy_methods;
std::optional<ci_lazy_methods_neededt> needed_lazy_methods;

/// Fully qualified name of the method under translation.
/// Initialized by `convert`.
Expand Down Expand Up @@ -319,7 +319,7 @@ class java_bytecode_convert_methodt
void convert(
const symbolt &class_symbol,
const methodt &,
const optionalt<prefix_filtert> &method_context);
const std::optional<prefix_filtert> &method_context);

code_blockt convert_parameter_annotations(
const methodt &method,
Expand Down Expand Up @@ -368,7 +368,7 @@ class java_bytecode_convert_methodt
std::vector<java_bytecode_parse_treet::instructiont>::const_iterator>
&ret_instructions) const;

optionalt<exprt> convert_invoke_dynamic(
std::optional<exprt> convert_invoke_dynamic(
const source_locationt &location,
std::size_t instruction_address,
const exprt &arg0,
Expand Down
Loading