Skip to content

JBMC: enable model and SSA equation verification #3747

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 11 commits into from
Jan 14, 2019
Merged

JBMC: enable model and SSA equation verification #3747

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
249fb3f
Method stubs: add missing type
smowton Jan 10, 2019
eda5f14
JBMC: support validation
smowton Jan 10, 2019
c203ef2
Lazy goto model: support validation
smowton Jan 10, 2019
738fbde
Don't validate Java symbols' base names for now
smowton Jan 10, 2019
555ff9a
Revert "strengthen assignment type consistency"
smowton Jan 14, 2019
03277d6
Add name to namespace parameter
smowton Jan 14, 2019
5867785
Enable model validation in all JBMC regression tests
smowton Jan 10, 2019
0f1abe1
DECL VCCs: don't check non-existent SSA-rhs
smowton Jan 10, 2019
d53bf4b
Equation validation: use base_type_eq on types, not exprs
smowton Jan 10, 2019
b2fe035
JBMC: enable SSA equation validation in all regression tests
smowton Jan 10, 2019
4232b15
Pacify clang-format
smowton Jan 14, 2019
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
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-concurrency/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
add_test_pl_tests(
"$<TARGET_FILE:jbmc>"
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
)
4 changes: 2 additions & 2 deletions jbmc/regression/jbmc-concurrency/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,10 @@ default: tests.log
include ../../src/config.inc

test:
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"

tests.log: ../$(CPROVER_DIR)/regression/test.pl
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"

show:
@for dir in *; do \
Expand Down
4 changes: 2 additions & 2 deletions jbmc/regression/jbmc-generics/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
add_test_pl_tests(
"$<TARGET_FILE:jbmc>"
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
)

add_test_pl_profile(
"jbmc-generics-symex-driven-lazy-loading"
"$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
"-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
"CORE"
)
8 changes: 4 additions & 4 deletions jbmc/regression/jbmc-generics/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,12 @@ default: tests.log
include ../../src/config.inc

test:
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading

tests.log: ../$(CPROVER_DIR)/regression/test.pl
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading

show:
@for dir in *; do \
Expand Down
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc-inheritance/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
add_test_pl_tests(
"$<TARGET_FILE:jbmc>"
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
)
4 changes: 2 additions & 2 deletions jbmc/regression/jbmc-inheritance/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,10 @@ default: tests.log
include ../../src/config.inc

test:
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"

tests.log: ../$(CPROVER_DIR)/regression/test.pl
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"

show:
@for dir in *; do \
Expand Down
4 changes: 2 additions & 2 deletions jbmc/regression/jbmc-strings/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
add_test_pl_tests(
"$<TARGET_FILE:jbmc>"
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
)

add_test_pl_profile(
"jbmc-strings-symex-driven-lazy-loading"
"$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
"-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
"CORE"
)
16 changes: 8 additions & 8 deletions jbmc/regression/jbmc-strings/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,20 +3,20 @@ default: tests.log
include ../../src/config.inc

test:
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading

testfuture:
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CF
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading

testall:
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CFTK
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading

tests.log: ../$(CPROVER_DIR)/regression/test.pl
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading

show:
@for dir in *; do \
Expand Down
4 changes: 2 additions & 2 deletions jbmc/regression/jbmc/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
add_test_pl_tests(
"$<TARGET_FILE:jbmc>"
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
)

add_test_pl_profile(
"jbmc-symex-driven-lazy-loading"
"$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
"-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
"CORE"
)
8 changes: 4 additions & 4 deletions jbmc/regression/jbmc/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,12 @@ default: tests.log
include ../../src/config.inc

test:
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading

tests.log: ../$(CPROVER_DIR)/regression/test.pl
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading

show:
@for dir in *; do \
Expand Down
4 changes: 2 additions & 2 deletions jbmc/regression/strings-smoke-tests/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
add_test_pl_tests(
"$<TARGET_FILE:jbmc>"
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
)

add_test_pl_profile(
"strings-smoke-tests-symex-driven-lazy-loading"
"$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
"-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
"CORE"
)
16 changes: 8 additions & 8 deletions jbmc/regression/strings-smoke-tests/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,20 +3,20 @@ default: tests.log
include ../../src/config.inc

test:
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading

testfuture:
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CF
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading

testall:
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CFTK
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading

tests.log: ../$(CPROVER_DIR)/regression/test.pl
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading

show:
@for dir in *; do \
Expand Down
3 changes: 2 additions & 1 deletion jbmc/src/java_bytecode/simple_method_stubbing.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -170,7 +170,8 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
symbol_table);
const symbol_exprt &init_symbol_expression = init_symbol.symbol_expr();
code_assignt get_argument(
init_symbol_expression, symbol_exprt(this_argument.get_identifier()));
init_symbol_expression,
symbol_exprt(this_argument.get_identifier(), this_type));
Copy link
Collaborator

Choose a reason for hiding this comment

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

We should really remove the single-argument constructor.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

In another PR, sure

Copy link
Collaborator

Choose a reason for hiding this comment

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

Sure, that was not meant as a request for work.

get_argument.add_source_location() = synthesized_source_location;
new_instructions.add(get_argument);
create_method_stub_at(
Expand Down
21 changes: 21 additions & 0 deletions jbmc/src/jbmc/jbmc_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -369,6 +369,16 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
"symex-coverage-report",
cmdline.get_value("symex-coverage-report"));

if(cmdline.isset("validate-ssa-equation"))
{
options.set_option("validate-ssa-equation", true);
}

if(cmdline.isset("validate-goto-model"))
{
options.set_option("validate-goto-model", true);
}

PARSE_OPTIONS_GOTO_TRACE(cmdline, options);

if(cmdline.isset("no-lazy-methods"))
Expand Down Expand Up @@ -553,6 +563,11 @@ int jbmc_parse_optionst::doit()
if(set_properties(goto_model))
return 7; // should contemplate EX_USAGE from sysexits.h

if(cmdline.isset("validate-goto-model"))
{
goto_model.validate(validation_modet::INVARIANT);
}

// The `configure_bmc` callback passed will enable enum-unwind-static if
// applicable.
return bmct::do_language_agnostic_bmc(
Expand Down Expand Up @@ -585,6 +600,11 @@ int jbmc_parse_optionst::doit()
// particular function:
add_failed_symbols(lazy_goto_model.symbol_table);

if(cmdline.isset("validate-goto-model"))
{
lazy_goto_model.validate(validation_modet::INVARIANT);
}

// Provide show-goto-functions and similar dump functions after symex
// executes. If --paths is active, these dump routines run after every
// paths iteration. Its return value indicates that if we ran any dump
Expand Down Expand Up @@ -1141,6 +1161,7 @@ void jbmc_parse_optionst::help()
" --version show version and exit\n"
" --xml-ui use XML-formatted output\n"
" --json-ui use JSON-formatted output\n"
HELP_VALIDATE
HELP_GOTO_TRACE
HELP_FLUSH
" --verbosity # verbosity level\n"
Expand Down
4 changes: 3 additions & 1 deletion jbmc/src/jbmc/jbmc_parse_options.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,9 +12,10 @@ Author: Daniel Kroening, [email protected]
#ifndef CPROVER_JBMC_JBMC_PARSE_OPTIONS_H
#define CPROVER_JBMC_JBMC_PARSE_OPTIONS_H

#include <util/ui_message.h>
#include <util/parse_options.h>
#include <util/timestamper.h>
#include <util/ui_message.h>
#include <util/validation_interface.h>

#include <langapi/language.h>

Expand Down Expand Up @@ -80,6 +81,7 @@ class optionst;
"(localize-faults)(localize-faults-method):" \
"(java-threading)" \
OPT_GOTO_TRACE \
OPT_VALIDATE \
"(symex-driven-lazy-loading)"
// clang-format on

Expand Down
6 changes: 6 additions & 0 deletions src/goto-programs/abstract_goto_model.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,12 @@ class abstract_goto_modelt
/// underneath them, so this should only be used to lend a reference to code
/// that cannot also call get_goto_function.
virtual const symbol_tablet &get_symbol_table() const = 0;

/// Check that the goto model is well-formed
///
/// The validation mode indicates whether well-formedness check failures are
/// reported via DATA_INVARIANT violations or exceptions.
virtual void validate(const validation_modet vm) const = 0;
};

#endif
14 changes: 13 additions & 1 deletion src/goto-programs/goto_model.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,7 @@ class goto_modelt : public abstract_goto_modelt
///
/// The validation mode indicates whether well-formedness check failures are
/// reported via DATA_INVARIANT violations or exceptions.
void validate(const validation_modet vm) const
void validate(const validation_modet vm) const override
{
symbol_table.validate(vm);

Expand Down Expand Up @@ -138,6 +138,18 @@ class wrapper_goto_modelt : public abstract_goto_modelt
goto_functions.function_map.end();
}

/// Check that the goto model is well-formed
///
/// The validation mode indicates whether well-formedness check failures are
/// reported via DATA_INVARIANT violations or exceptions.
void validate(const validation_modet vm) const override
{
symbol_table.validate(vm);

const namespacet ns(symbol_table);
goto_functions.validate(ns, vm);
}

private:
const symbol_tablet &symbol_table;
const goto_functionst &goto_functions;
Expand Down
9 changes: 9 additions & 0 deletions src/goto-programs/lazy_goto_model.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -243,6 +243,15 @@ class lazy_goto_modelt : public abstract_goto_modelt
return goto_functions.at(id);
}

/// Check that the goto model is well-formed
///
/// The validation mode indicates whether well-formedness check failures are
/// reported via DATA_INVARIANT violations or exceptions.
void validate(const validation_modet vm) const override
{
goto_model->validate(vm);
}

private:
std::unique_ptr<goto_modelt> goto_model;

Expand Down
8 changes: 6 additions & 2 deletions src/goto-symex/symex_target_equation.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -961,15 +961,19 @@ void symex_target_equationt::SSA_stept::validate(
case goto_trace_stept::typet::CONSTRAINT:
validate_full_expr(cond_expr, ns, vm);
break;
case goto_trace_stept::typet::ASSIGNMENT:
case goto_trace_stept::typet::DECL:
validate_full_expr(ssa_lhs, ns, vm);
validate_full_expr(ssa_full_lhs, ns, vm);
validate_full_expr(original_full_lhs, ns, vm);
break;
case goto_trace_stept::typet::ASSIGNMENT:
validate_full_expr(ssa_lhs, ns, vm);
validate_full_expr(ssa_full_lhs, ns, vm);
validate_full_expr(original_full_lhs, ns, vm);
validate_full_expr(ssa_rhs, ns, vm);
DATA_CHECK(
vm,
base_type_eq(ssa_lhs.get_original_expr(), ssa_rhs, ns),
base_type_eq(ssa_lhs.get_original_expr().type(), ssa_rhs.type(), ns),
"Type inequality in SSA assignment\nlhs-type: " +
ssa_lhs.get_original_expr().type().id_string() +
"\nrhs-type: " + ssa_rhs.type().id_string());
Expand Down
4 changes: 2 additions & 2 deletions src/util/std_code.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -296,14 +296,14 @@ class code_assignt:public codet

static void validate(
const codet &code,
const namespacet &,
const namespacet &ns,
const validation_modet vm = validation_modet::INVARIANT)
{
check(code, vm);

DATA_CHECK(
vm,
code.op0().type() == code.op1().type(),
base_type_eq(code.op0().type(), code.op1().type(), ns),
Copy link
Collaborator

Choose a reason for hiding this comment

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

To be debated with @kroening as this appears to work against the effort going on in other PRs.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Fair enough if we want the strict same-level-of-indirection condition in the future, but we certainly don't even try to do that at present.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Can this commit be dropped from the PR? I understand that this would mean it doesn't work for Java at the moment, but then we can get all the other improvements in the meantime.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Well, my intent was to use this as the means of testing the other improvements, by showing particular programs begin to satisfy this constraint when the fixes are applied, so I'd much prefer to have this statement of our current intended guarantee available, then we can chase after a future attempted standard later?

"lhs and rhs of assignment must have same type");
}

Expand Down
7 changes: 4 additions & 3 deletions src/util/symbol.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -137,10 +137,11 @@ bool symbolt::is_well_formed() const
// Well-formedness criterion number 2 is for a symbol
// to have it's base name as a suffix to it's more
// general name.
if(!has_suffix(id2string(name), id2string(base_name)))
{
// Exception: Java symbols' base names do not have type signatures
// (for example, they can have name "someclass.method:(II)V" and base name
// "method")
if(!has_suffix(id2string(name), id2string(base_name)) && mode != ID_java)
Copy link
Member

Choose a reason for hiding this comment

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

Can we check that method is between . and : instead?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

It also differs for field symbols, and generics, and... I'd like to leave (a) setting a convention and (b) enforcing it for a different PR!

return false;
}

return true;
}
Expand Down