-
Notifications
You must be signed in to change notification settings - Fork 139
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add points-to set using aliasing properties
Summary: This diff adds a `PointsToSet` domain. This domain will be used as an element of the PointsToTree in the following diffs. `PointsToSet` tracks a set of target memory locations that an alias may point-to. This is implemented as a Map from `MemoryLocation` to `AliasingProperties` where the `AliasingProperties` provides additional information that needs to be added when reading the memorylocation through this alias. Reviewed By: arthaud Differential Revision: D65186106 fbshipit-source-id: ab6fc067b48bb9064aa542cf54c26953eb3e625f
- Loading branch information
1 parent
6ce0758
commit 099f2c1
Showing
2 changed files
with
168 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,69 @@ | ||
/* | ||
* Copyright (c) Meta Platforms, Inc. and affiliates. | ||
* | ||
* This source code is licensed under the MIT license found in the | ||
* LICENSE file in the root directory of this source tree. | ||
*/ | ||
|
||
#include <Show.h> | ||
|
||
#include <mariana-trench/PointsToSet.h> | ||
|
||
namespace marianatrench { | ||
|
||
PointsToSet::PointsToSet(MemoryLocation* memory_location) { | ||
set_internal(memory_location, AliasingProperties::empty()); | ||
} | ||
|
||
PointsToSet::PointsToSet( | ||
MemoryLocation* memory_location, | ||
AliasingProperties properties) { | ||
set_internal(memory_location, std::move(properties)); | ||
} | ||
|
||
PointsToSet::PointsToSet( | ||
std::initializer_list<MemoryLocation*> memory_locations) { | ||
for (auto* memory_location : memory_locations) { | ||
set_internal(memory_location, AliasingProperties::empty()); | ||
} | ||
} | ||
|
||
PointsToSet::PointsToSet(const MemoryLocationsDomain& memory_locations) { | ||
for (auto* memory_location : memory_locations) { | ||
set_internal(memory_location, AliasingProperties::empty()); | ||
} | ||
} | ||
|
||
void PointsToSet::add_local_position(const Position* position) { | ||
map_.transform([position](AliasingProperties properties) { | ||
properties.add_local_position(position); | ||
return properties; | ||
}); | ||
} | ||
|
||
void PointsToSet::add_locally_inferred_features( | ||
const FeatureMayAlwaysSet& features) { | ||
if (features.empty()) { | ||
return; | ||
} | ||
|
||
map_.transform([&features](AliasingProperties properties) { | ||
properties.add_locally_inferred_features(features); | ||
return properties; | ||
}); | ||
} | ||
|
||
std::ostream& operator<<(std::ostream& out, const PointsToSet& points_to_set) { | ||
mt_assert(!points_to_set.is_top()); | ||
|
||
out << "PointsToSet{"; | ||
for (const auto& [memory_location, properties] : | ||
points_to_set.map_.bindings()) { | ||
out << "memory_location=" << show(memory_location) << ",properties={" | ||
<< properties << "}"; | ||
} | ||
|
||
return out << "}"; | ||
} | ||
|
||
} // namespace marianatrench |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,99 @@ | ||
/* | ||
* Copyright (c) Meta Platforms, Inc. and affiliates. | ||
* | ||
* This source code is licensed under the MIT license found in the | ||
* LICENSE file in the root directory of this source tree. | ||
*/ | ||
|
||
#pragma once | ||
|
||
#include <sparta/AbstractDomain.h> | ||
#include <sparta/PatriciaTreeMapAbstractPartition.h> | ||
|
||
#include <mariana-trench/AliasingProperties.h> | ||
#include <mariana-trench/IncludeMacros.h> | ||
#include <mariana-trench/MemoryLocation.h> | ||
#include <mariana-trench/MemoryLocationEnvironment.h> | ||
|
||
namespace marianatrench { | ||
|
||
class PointsToSet final : public sparta::AbstractDomain<PointsToSet> { | ||
private: | ||
using Map = sparta:: | ||
PatriciaTreeMapAbstractPartition<MemoryLocation*, AliasingProperties>; | ||
|
||
public: | ||
// C++ container concept member types | ||
using key_type = MemoryLocation*; | ||
using mapped_type = AliasingProperties; | ||
using value_type = std::pair<const MemoryLocation*, AliasingProperties>; | ||
using iterator = typename Map::MapType::iterator; | ||
using const_iterator = iterator; | ||
using difference_type = std::ptrdiff_t; | ||
using size_type = std::size_t; | ||
using const_reference = const value_type&; | ||
using const_pointer = const value_type*; | ||
|
||
private: | ||
explicit PointsToSet(Map map) : map_(std::move(map)) {} | ||
|
||
public: | ||
PointsToSet() : map_(Map::bottom()) {} | ||
|
||
explicit PointsToSet(MemoryLocation* memory_location); | ||
|
||
explicit PointsToSet( | ||
MemoryLocation* memory_location, | ||
AliasingProperties properties); | ||
|
||
explicit PointsToSet(std::initializer_list<MemoryLocation*> memory_locations); | ||
|
||
explicit PointsToSet(const MemoryLocationsDomain& memory_locations); | ||
|
||
INCLUDE_ABSTRACT_DOMAIN_METHODS(PointsToSet, Map, map_) | ||
|
||
void difference_with(const PointsToSet& other) { | ||
map_.difference_like_operation( | ||
other.map_, | ||
[](const AliasingProperties& left, const AliasingProperties& right) { | ||
if (left.leq(right)) { | ||
return AliasingProperties::empty(); | ||
} | ||
return left; | ||
}); | ||
} | ||
|
||
std::size_t size() const { | ||
return map_.size(); | ||
} | ||
|
||
iterator begin() const { | ||
return map_.bindings().begin(); | ||
} | ||
|
||
iterator end() const { | ||
return map_.bindings().end(); | ||
} | ||
|
||
void add_local_position(const Position* position); | ||
|
||
void add_locally_inferred_features(const FeatureMayAlwaysSet& features); | ||
|
||
private: | ||
void set_internal( | ||
MemoryLocation* memory_location, | ||
AliasingProperties&& properties) { | ||
mt_assert(!properties.is_top()); | ||
mt_assert(!memory_location->is<FieldMemoryLocation>()); | ||
map_.set(memory_location, std::move(properties)); | ||
} | ||
|
||
friend std::ostream& operator<<( | ||
std::ostream& out, | ||
const PointsToSet& points_to_set); | ||
|
||
private: | ||
Map map_; | ||
}; | ||
|
||
} // namespace marianatrench |