Add a class for code with references
This will be use in assign_from_json for json files in which the "@ref" and "@id" entries are used, so that we can easily substitute code marked by "@ref" by the code corresponding to the object marked by "@id". This also move object_creation_referencet to the new header file since it will be used there, and the allocate_array is now declared in the new header and defined in the corresponding cpp file.
This commit is contained in:
parent
4879a7458b
commit
b40ac5956e
|
@ -23,3 +23,48 @@ codet allocate_array(
|
|||
java_new_array.type().subtype().set(ID_element_type, element_type);
|
||||
return code_assignt{expr, java_new_array, loc};
|
||||
}
|
||||
|
||||
code_blockt
|
||||
reference_allocationt::to_code(reference_substitutiont &references) const
|
||||
{
|
||||
const object_creation_referencet &reference = references(reference_id);
|
||||
INVARIANT(reference.array_length, "Length of reference array must be known");
|
||||
if(can_cast_expr<constant_exprt>(*reference.array_length))
|
||||
{
|
||||
return code_blockt(
|
||||
{allocate_array(reference.expr, *reference.array_length, loc)});
|
||||
}
|
||||
// Fallback in case the array definition has not been seen yet, this can
|
||||
// happen if `to_code` is called before the whole json file has been processed
|
||||
// or the "@id" json field corresponding to `reference_id` doesn't appear in
|
||||
// the file.
|
||||
code_blockt code;
|
||||
code.add(code_assignt{*reference.array_length,
|
||||
side_effect_expr_nondett{java_int_type()}});
|
||||
code.add(code_assumet{binary_predicate_exprt{
|
||||
*reference.array_length, ID_ge, from_integer(0, java_int_type())}});
|
||||
code.add(allocate_array(reference.expr, *reference.array_length, loc));
|
||||
return code;
|
||||
}
|
||||
|
||||
void code_with_references_listt::add(code_without_referencest code)
|
||||
{
|
||||
auto ptr = std::make_shared<code_without_referencest>(std::move(code));
|
||||
list.emplace_back(std::move(ptr));
|
||||
}
|
||||
|
||||
void code_with_references_listt::add(codet code)
|
||||
{
|
||||
add(code_without_referencest{std::move(code)});
|
||||
}
|
||||
|
||||
void code_with_references_listt::add(reference_allocationt ref)
|
||||
{
|
||||
auto ptr = std::make_shared<reference_allocationt>(std::move(ref));
|
||||
list.emplace_back(std::move(ptr));
|
||||
}
|
||||
|
||||
void code_with_references_listt::append(code_with_references_listt &&other)
|
||||
{
|
||||
list.splice(list.end(), other.list);
|
||||
}
|
||||
|
|
|
@ -33,4 +33,74 @@ struct object_creation_referencet
|
|||
optionalt<exprt> array_length;
|
||||
};
|
||||
|
||||
/// Base class for code which can contain references which can get replaced
|
||||
/// before generating actual codet.
|
||||
/// Currently only references in array allocations are supported, because this
|
||||
/// is currently the only use required by \ref assign_from_json.
|
||||
class code_with_referencest
|
||||
{
|
||||
public:
|
||||
using reference_substitutiont =
|
||||
std::function<const object_creation_referencet &(const std::string &)>;
|
||||
|
||||
virtual code_blockt to_code(reference_substitutiont &) const = 0;
|
||||
|
||||
virtual ~code_with_referencest() = default;
|
||||
};
|
||||
|
||||
/// Code that should not contain reference
|
||||
class code_without_referencest : public code_with_referencest
|
||||
{
|
||||
public:
|
||||
codet code;
|
||||
|
||||
explicit code_without_referencest(codet code) : code(std::move(code))
|
||||
{
|
||||
}
|
||||
|
||||
code_blockt to_code(reference_substitutiont &) const override
|
||||
{
|
||||
return code_blockt({code});
|
||||
}
|
||||
};
|
||||
|
||||
/// Allocation code which contains a reference.
|
||||
/// The generated code will be of the form:
|
||||
///
|
||||
/// array_length = nondet(int)
|
||||
/// assume(array_length >= 0)
|
||||
/// array_expr = new array_type[array_length];
|
||||
///
|
||||
/// Where array_length and array_expr are given by the reference substitution
|
||||
/// function.
|
||||
class reference_allocationt : public code_with_referencest
|
||||
{
|
||||
public:
|
||||
std::string reference_id;
|
||||
source_locationt loc;
|
||||
|
||||
reference_allocationt(std::string reference_id, source_locationt loc)
|
||||
: reference_id(std::move(reference_id)), loc(std::move(loc))
|
||||
{
|
||||
}
|
||||
|
||||
code_blockt to_code(reference_substitutiont &references) const override;
|
||||
};
|
||||
|
||||
/// Wrapper around a list of shared pointer to code_with_referencest objects,
|
||||
/// which provides a nicer interface.
|
||||
class code_with_references_listt
|
||||
{
|
||||
public:
|
||||
std::list<std::shared_ptr<code_with_referencest>> list;
|
||||
|
||||
void add(code_without_referencest code);
|
||||
|
||||
void add(codet code);
|
||||
|
||||
void add(reference_allocationt ref);
|
||||
|
||||
void append(code_with_references_listt &&other);
|
||||
};
|
||||
|
||||
#endif // CPROVER_JAVA_BYTECODE_CODE_WITH_REFERENCES_H
|
||||
|
|
Loading…
Reference in New Issue