Skip to content

Commit

Permalink
fix: crab variable linked to WeakVH instead of Value
Browse files Browse the repository at this point in the history
WeakVH is a smart pointer that knows when the tracked Value* becomes
invalid.  This makes the code more robust if LLVM IR changes.

This solves issue#99
  • Loading branch information
caballa committed Apr 19, 2024
1 parent 4497e6f commit d089f8c
Show file tree
Hide file tree
Showing 5 changed files with 27 additions and 12 deletions.
20 changes: 16 additions & 4 deletions include/clam/crab/crab_lang.hh
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,11 @@
*/

#include "llvm/IR/BasicBlock.h"
#include "llvm/IR/Value.h"
#include "llvm/IR/ValueHandle.h"
#include "llvm/Support/raw_ostream.h"

#include "clam/Support/Debug.hh"

#include "crab/analysis/dataflow/liveness.hpp"
#include "crab/cfg/cfg.hpp"
#include "crab/cg/cg.hpp"
Expand Down Expand Up @@ -110,11 +112,21 @@ template <> struct hash<clam::llvm_basic_block_wrapper> {
return bb.hash();
}
};

template <> struct hash<llvm::WeakVH> {
size_t operator()(const llvm::WeakVH &VH) const {
if (VH == nullptr) {
CLAM_ERROR("Trying to hash an invalid WeakVH");
}
return std::hash<llvm::Value*>{}(VH);
}
};
} // namespace std


namespace clam {
/** Define a Crab CFG and call graph over integers **/
using variable_factory_t = crab::var_factory_impl::variable_factory<const llvm::Value*>;
using variable_factory_t = crab::var_factory_impl::variable_factory<llvm::WeakVH>;
using varname_t = typename variable_factory_t::varname_t;
using number_t = ikos::z_number;
using var_t = crab::variable<number_t, varname_t>;
Expand Down Expand Up @@ -148,9 +160,9 @@ using varset_t = typename liveness_t::varset_domain_t;
} // end namespace clam

namespace crab {
template <> class variable_name_traits<const llvm::Value *> {
template <> class variable_name_traits<llvm::WeakVH> {
public:
static std::string to_string(const llvm::Value *v) {
static std::string to_string(llvm::WeakVH v) {
return v->getName().str();
}
};
Expand Down
9 changes: 6 additions & 3 deletions lib/Clam/CfgBuilderLit.cc
Original file line number Diff line number Diff line change
Expand Up @@ -386,7 +386,8 @@ Optional<crabBoolLit> crabLitFactoryImpl::getBoolLit(const Value &v) {
// nondeterministic value.
return crabBoolLit(var_t(m_vfac.get(), BOOL_TYPE, 1));
} else {
return crabBoolLit(var_t(m_vfac[&v], BOOL_TYPE, 1));
WeakVH VH(const_cast<Value*>(&v));
return crabBoolLit(var_t(m_vfac[VH], BOOL_TYPE, 1));
}
}
}
Expand All @@ -404,7 +405,8 @@ Optional<crabRefLit> crabLitFactoryImpl::getRefLit(const Value &v) {
// nondeterministic value.
return crabRefLit(var_t(m_vfac.get(), REF_TYPE));
} else {
return crabRefLit(var_t(m_vfac[&v], REF_TYPE));
WeakVH VH(const_cast<Value*>(&v));
return crabRefLit(var_t(m_vfac[VH], REF_TYPE));
}
}
return None;
Expand All @@ -428,7 +430,8 @@ Optional<crabIntLit> crabLitFactoryImpl::getIntLit(const Value &v, bool IntCstAs
// nondeterministic value.
return crabIntLit(var_t(m_vfac.get(), INT_TYPE, bitwidth));
} else {
return crabIntLit(var_t(m_vfac[&v], INT_TYPE, bitwidth));
WeakVH VH(const_cast<Value*>(&v));
return crabIntLit(var_t(m_vfac[VH], INT_TYPE, bitwidth));
}
}
}
Expand Down
3 changes: 2 additions & 1 deletion lib/Clam/ClamQueryCache.cc
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,8 @@ static const Instruction* getInstruction(statement_t &s) {
if (s.get_live().num_defs() == 1) {
var_t v = *(s.get_live().defs_begin());
if (v.name().get()) {
if (auto I = dyn_cast<const Instruction>(*(v.name().get()))) {
// The result of the cast can be null if llvm Value handler becomes invalid.
if (auto I = dyn_cast_or_null<const Instruction>(*(v.name().get()))) {
return I;
}
}
Expand Down
4 changes: 2 additions & 2 deletions lib/Clam/Optimizer/Optimizer.cc
Original file line number Diff line number Diff line change
Expand Up @@ -136,7 +136,7 @@ class CodeExpander {
}

static Value *mkVar(varname_t v) {
return (v.get() ? const_cast<Value *>(*(v.get())) : nullptr);
return (v.get() ? *(v.get()) : nullptr);
}

static Value *mkBool(LLVMContext &ctx, bool val) {
Expand All @@ -147,7 +147,7 @@ class CodeExpander {
if (!var.get()) {
return nullptr;
} else {
Type *Ty = (const_cast<Value *>(*(var.get())))->getType();
Type *Ty = (*(var.get()))->getType();
if (IntegerType *ITy = dyn_cast<IntegerType>(Ty)) {
return ITy;
}
Expand Down
3 changes: 1 addition & 2 deletions lib/Clam/crab/output/json/write_json.cc
Original file line number Diff line number Diff line change
Expand Up @@ -111,8 +111,7 @@ void json_report_impl::write_invariants(cfg_ref_t cfg,
std::vector<var_t> out;
for (auto const&cst: csts) {
for (auto v : cst.variables()) {
boost::optional<const llvm::Value*> llvm_v = v.name().get();
if (llvm_v == boost::none) {
if (v.name().get() == boost::none) {
out.push_back(v);
}
}
Expand Down

0 comments on commit d089f8c

Please sign in to comment.