Skip to content

remove usage of typet::subtype() #6599

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.

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
Jan 31, 2022
Merged

remove usage of typet::subtype() #6599

merged 1 commit into from
Jan 31, 2022

Conversation

kroening
Copy link
Member

This commit replaces invocations of typet::subtype() by the appropriate
methods offered by the more specific types, e.g., pointer_typet,
array_typet, and so on.

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

Comment on lines 128 to 134
to_pointer_type(*target_type).base_type(), source_type->subtype());
// We have a pointer to something, but the thing it is pointing to can't be
// modified normally, but can through this pointer
if(!direct_subtypes_at_least_as_const)
return false;
// Check the subtypes if they are pointers
target_type=&target_type->subtype();
target_type = &to_pointer_type(*target_type).base_type();
Copy link
Collaborator

Choose a reason for hiding this comment

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

May I suggest a temporary to avoid the repeated to_pointer_type(*target_type) in this code branch?

Copy link
Member Author

Choose a reason for hiding this comment

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

done

#include <util/base_type.h>
#include <util/pointer_expr.h>
#include <util/std_code.h>
#include <util/type.h>
Copy link
Collaborator

Choose a reason for hiding this comment

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

Nit pick: I'm pretty sure util/type.h does not need to be included explicitly here.

Copy link
Member Author

Choose a reason for hiding this comment

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

done

Comment on lines 25 to 30
{
PRECONDITION(type.id()==ID_pointer);

if(type.subtype().id() == ID_struct_tag)
return to_struct_tag_type(type.subtype()).get_identifier();
if(to_pointer_type(type).base_type().id() == ID_struct_tag)
return to_struct_tag_type(to_pointer_type(type).base_type())
.get_identifier();
Copy link
Collaborator

Choose a reason for hiding this comment

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

Could we please change the interface here to just take a const pointer_typet &?

Copy link
Member Author

Choose a reason for hiding this comment

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

done

Comment on lines 89 to 94
if(src_type_id==ID_c_bit_field)
return check_c_implicit_typecast(src_type.subtype(), dest_type);
return check_c_implicit_typecast(
to_c_bit_field_type(src_type).underlying_type(), dest_type);
Copy link
Collaborator

Choose a reason for hiding this comment

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

Nit pick: would appreciate a pair of { ... } around the multi-line body.

Comment on lines 93 to 100
if(dest_type.id()==ID_c_bit_field)
return check_c_implicit_typecast(src_type, dest_type.subtype());
return check_c_implicit_typecast(
src_type, to_c_bit_field_type(dest_type).underlying_type());
Copy link
Collaborator

Choose a reason for hiding this comment

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

Nit pick: would appreciate a pair of { ... } around the multi-line body.

Comment on lines 788 to 792
if(
to_reference_type(parameter1_type).base_type().get(ID_identifier) !=
symbol.name)
continue;
Copy link
Collaborator

Choose a reason for hiding this comment

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

Nit pick: would appreciate a pair of { ... } given the multi-line condition.

Comment on lines +840 to 845
if(
to_reference_type(arg1_type).base_type().get(ID_identifier) !=
symbol.name)
continue;
Copy link
Collaborator

Choose a reason for hiding this comment

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

Nit pick: would appreciate a pair of { ... } given the multi-line condition.

Comment on lines 787 to 792
if(
type.id() == ID_array &&
to_array_type(type).element_type().get_bool(ID_C_constant))
return true;

return type.get_bool(ID_C_constant);
Copy link
Collaborator

Choose a reason for hiding this comment

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

Nit pick: would appreciate a pair of { ... } given the multi-line condition. Or perhaps just rewrite this function to just have a return statement.

Copy link
Member Author

Choose a reason for hiding this comment

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

done

Comment on lines 25 to 29
if(
expr.type().id() == ID_array &&
boolbv_width(to_array_type(expr.type()).element_type()) != 0)
return bvt();
Copy link
Collaborator

Choose a reason for hiding this comment

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

Nit pick: would appreciate a pair of { ... } given the multi-line condition.

Comment on lines 3329 to 3338
if(to_pointer_type(expr.type()).base_type().id() == ID_empty)
{
// This is a gcc extension.
// https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
element_size = 1;
}
else
{
auto element_size_opt = pointer_offset_size(expr.type().subtype(), ns);
auto element_size_opt =
pointer_offset_size(to_pointer_type(expr.type()).base_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.

A temporary may be useful here to avoid the repeated to_pointer_type.

Copy link
Member Author

Choose a reason for hiding this comment

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

done

@codecov
Copy link

codecov bot commented Jan 20, 2022

Codecov Report

Merging #6599 (3b27b76) into develop (57e7b2c) will decrease coverage by 0.00%.
The diff coverage is 72.59%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #6599      +/-   ##
===========================================
- Coverage    76.65%   76.64%   -0.01%     
===========================================
  Files         1579     1579              
  Lines       181294   181480     +186     
===========================================
+ Hits        138973   139098     +125     
- Misses       42321    42382      +61     
Impacted Files Coverage Δ
src/analyses/goto_rw.cpp 52.30% <0.00%> (-0.13%) ⬇️
src/analyses/uncaught_exceptions_analysis.h 100.00% <ø> (ø)
src/ansi-c/ansi_c_parser.cpp 88.39% <0.00%> (ø)
src/cpp/cpp_declarator_converter.h 100.00% <ø> (ø)
src/cpp/cpp_exception_id.cpp 0.00% <0.00%> (ø)
src/cpp/cpp_template_type.h 64.28% <0.00%> (-17.54%) ⬇️
src/cpp/cpp_typecheck.cpp 79.22% <0.00%> (ø)
src/cpp/cpp_typecheck_initializer.cpp 29.09% <0.00%> (-0.36%) ⬇️
src/goto-programs/interpreter.cpp 52.29% <0.00%> (ø)
src/goto-programs/interpreter_evaluate.cpp 33.77% <0.00%> (-0.06%) ⬇️
... and 89 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 59155f9...3b27b76. Read the comment docs.

@kroening kroening force-pushed the typet_subtype_const branch 2 times, most recently from ad15521 to 19c3981 Compare January 20, 2022 15:22
This commit replaces invocations of typet::subtype() by the appropriate
methods offered by the more specific types, e.g., pointer_typet,
array_typet, and so on.
@kroening kroening force-pushed the typet_subtype_const branch from 19c3981 to 3b27b76 Compare January 31, 2022 09:50
@kroening kroening merged commit 637f138 into develop Jan 31, 2022
@kroening kroening deleted the typet_subtype_const branch January 31, 2022 14:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants