Skip to content

Java frontend: don't advertise ignored methods #2265

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

Merged
merged 1 commit into from
Jun 5, 2018
Merged

Java frontend: don't advertise ignored methods #2265

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
25 changes: 3 additions & 22 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 @@ -2824,32 +2824,13 @@ void java_bytecode_convert_method(
java_string_library_preprocesst &string_preprocess,
const class_hierarchyt &class_hierarchy)
{
static const std::unordered_set<std::string> methods_to_ignore
{
"nondetBoolean",
"nondetByte",
"nondetChar",
"nondetShort",
"nondetInt",
"nondetLong",
"nondetFloat",
"nondetDouble",
"nondetWithNull",
"nondetWithoutNull",
"notModelled",
"atomicBegin",
"atomicEnd",
"startThread",
"endThread",
"getCurrentThreadID"
};

if(std::regex_match(
id2string(class_symbol.name),
std::regex(".*org\\.cprover\\.CProver.*")) &&
methods_to_ignore.find(id2string(method.name))!=methods_to_ignore.end())
cprover_methods_to_ignore.count(id2string(method.name)))
{
// Ignore these methods, rely on default stubbing behaviour.
// Ignore these methods; fall back to the driver program's
// stubbing behaviour.
return;
}

Expand Down
25 changes: 25 additions & 0 deletions jbmc/src/java_bytecode/java_bytecode_language.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -843,11 +843,36 @@ const select_pointer_typet &
void java_bytecode_languaget::methods_provided(
std::unordered_set<irep_idt> &methods) const
{
static std::string cprover_class_prefix = "java::org.cprover.CProver.";
Copy link
Contributor

Choose a reason for hiding this comment

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

const ?


// Add all string solver methods to map
string_preprocess.get_all_function_names(methods);
// Add all concrete methods to map
for(const auto &kv : method_bytecode)
{
const std::string &method_id = id2string(kv.first);

// Avoid advertising org.cprover.CProver methods that the Java frontend will
// never provide bodies for (java_bytecode_convert_method always leaves them
// bodyless with intent for the driver program to stub them):
if(has_prefix(method_id, cprover_class_prefix))
{
std::size_t method_name_end_offset =
method_id.find(':', cprover_class_prefix.length());
INVARIANT(
method_name_end_offset != std::string::npos,
"org.cprover.CProver method should have a postfix type descriptor");

const std::string method_name =
method_id.substr(
cprover_class_prefix.length(),
method_name_end_offset - cprover_class_prefix.length());

if(cprover_methods_to_ignore.count(method_name))
continue;
}
methods.insert(kv.first);
}
// Add all synthetic methods to map
for(const auto &kv : synthetic_methods)
methods.insert(kv.first);
Expand Down
22 changes: 22 additions & 0 deletions jbmc/src/java_bytecode/java_utils.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -426,3 +426,25 @@ bool is_non_null_library_global(const irep_idt &symbolid)
"java::java.lang.System.in"};
return non_null_globals.count(symbolid);
}

/// Methods belonging to the class org.cprover.CProver that should be ignored
/// (not converted), leaving the driver program to stub them if it wishes.
const std::unordered_set<std::string> cprover_methods_to_ignore
{
"nondetBoolean",
"nondetByte",
"nondetChar",
"nondetShort",
"nondetInt",
"nondetLong",
"nondetFloat",
"nondetDouble",
"nondetWithNull",
"nondetWithoutNull",
"notModelled",
"atomicBegin",
"atomicEnd",
"startThread",
"endThread",
"getCurrentThreadID"
};
4 changes: 4 additions & 0 deletions jbmc/src/java_bytecode/java_utils.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,8 @@ Author: Daniel Kroening, [email protected]
#ifndef CPROVER_JAVA_BYTECODE_JAVA_UTILS_H
#define CPROVER_JAVA_BYTECODE_JAVA_UTILS_H

#include <unordered_set>

#include <util/message.h>
#include <util/std_expr.h>
#include <util/symbol_table.h>
Expand Down Expand Up @@ -108,4 +110,6 @@ resolve_inherited_componentt::inherited_componentt get_inherited_component(

bool is_non_null_library_global(const irep_idt &);

extern const std::unordered_set<std::string> cprover_methods_to_ignore;

#endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H