Skip to content

Commit e9a67bd

Browse files
author
Owen
committed
Factor out value_sett::get_entry_for_symbol
Make this a separate function so it can be used from other places. No change in behaviour.
1 parent b54448c commit e9a67bd

File tree

3 files changed

+87
-36
lines changed

3 files changed

+87
-36
lines changed

src/goto-symex/goto_symex.h

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -308,6 +308,28 @@ class goto_symext
308308
virtual void symex_other(statet &state);
309309

310310
void symex_assert(const goto_programt::instructiont &, statet &);
311+
312+
/// Try to filter value sets based on whether possible values of a
313+
/// pointer-typed symbol make the condition true or false. We only do this
314+
/// when there is only one pointer-typed symbol in \p condition.
315+
/// \param state: The current state
316+
/// \param condition: The condition which is being evaluated, which it expects
317+
/// will not have been cleaned or renamed. In practice, it's fine if it has
318+
/// been cleaned and renamed up to level L1.
319+
/// \param value_set_for_true_case: A pointer to the value set that possible
320+
/// values should be removed from if they make the condition false, or
321+
/// nullptr if this shouldn't be done
322+
/// \param value_set_for_false_case: A pointer to the value set that possible
323+
/// values should be removed from if they make the condition true, or
324+
/// nullptr if this shouldn't be done
325+
/// \param ns: A namespace
326+
void try_filter_value_sets(
327+
goto_symex_statet &state,
328+
exprt condition,
329+
value_sett *value_set_for_true_case,
330+
value_sett *value_set_for_false_case,
331+
const namespacet &ns);
332+
311333
virtual void vcc(
312334
const exprt &,
313335
const std::string &msg,

src/pointer-analysis/value_set.cpp

Lines changed: 52 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -367,6 +367,54 @@ static std::string strip_first_field_from_suffix(
367367
return suffix.substr(field.length() + 1);
368368
}
369369

370+
const value_sett::entryt *value_sett::get_entry_for_symbol(
371+
const irep_idt identifier,
372+
const typet &type,
373+
const std::string &suffix,
374+
const namespacet &ns) const
375+
{
376+
if(
377+
type.id() != ID_pointer && type.id() != ID_signedbv &&
378+
type.id() != ID_unsignedbv && type.id() != ID_array &&
379+
type.id() != ID_struct && type.id() != ID_struct_tag &&
380+
type.id() != ID_union && type.id() != ID_union_tag)
381+
{
382+
return nullptr;
383+
}
384+
385+
const typet &followed_type = type.id() == ID_struct_tag
386+
? ns.follow_tag(to_struct_tag_type(type))
387+
: type.id() == ID_union_tag
388+
? ns.follow_tag(to_union_tag_type(type))
389+
: type;
390+
391+
// look it up
392+
const value_sett::entryt *entry = find_entry(id2string(identifier) + suffix);
393+
394+
// try first component name as suffix if not yet found
395+
if(
396+
!entry &&
397+
(followed_type.id() == ID_struct || followed_type.id() == ID_union))
398+
{
399+
const struct_union_typet &struct_union_type =
400+
to_struct_union_type(followed_type);
401+
402+
const irep_idt &first_component_name =
403+
struct_union_type.components().front().get_name();
404+
405+
entry = find_entry(
406+
id2string(identifier) + "." + id2string(first_component_name) + suffix);
407+
}
408+
409+
if(!entry)
410+
{
411+
// not found? try without suffix
412+
entry = find_entry(identifier);
413+
}
414+
415+
return entry;
416+
}
417+
370418
void value_sett::get_value_set_rec(
371419
const exprt &expr,
372420
object_mapt &dest,
@@ -414,43 +462,11 @@ void value_sett::get_value_set_rec(
414462
}
415463
else if(expr.id()==ID_symbol)
416464
{
417-
irep_idt identifier=to_symbol_expr(expr).get_identifier();
418-
419-
// is it a pointer, integer, array or struct?
420-
if(expr_type.id()==ID_pointer ||
421-
expr_type.id()==ID_signedbv ||
422-
expr_type.id()==ID_unsignedbv ||
423-
expr_type.id()==ID_struct ||
424-
expr_type.id()==ID_union ||
425-
expr_type.id()==ID_array)
426-
{
427-
// look it up
428-
const entryt *entry =
429-
find_entry(id2string(identifier) + suffix);
430-
431-
// try first component name as suffix if not yet found
432-
if(!entry && (expr_type.id() == ID_struct || expr_type.id() == ID_union))
433-
{
434-
const struct_union_typet &struct_union_type=
435-
to_struct_union_type(expr_type);
465+
const entryt *entry = get_entry_for_symbol(
466+
to_symbol_expr(expr).get_identifier(), expr_type, suffix, ns);
436467

437-
const irep_idt &first_component_name =
438-
struct_union_type.components().front().get_name();
439-
440-
entry = find_entry(
441-
id2string(identifier) + "." + id2string(first_component_name) +
442-
suffix);
443-
}
444-
445-
// not found? try without suffix
446-
if(!entry)
447-
entry = find_entry(identifier);
448-
449-
if(entry)
450-
make_union(dest, entry->object_map);
451-
else
452-
insert(dest, exprt(ID_unknown, original_type));
453-
}
468+
if(entry)
469+
make_union(dest, entry->object_map);
454470
else
455471
insert(dest, exprt(ID_unknown, original_type));
456472
}

src/pointer-analysis/value_set.h

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -455,6 +455,19 @@ class value_sett
455455
exprt &expr,
456456
const namespacet &ns) const;
457457

458+
/// Get the entry for the symbol and suffix
459+
/// \param identifier: The identifier for the symbol
460+
/// \param type: The type of the symbol
461+
/// \param suffix: The suffix for the entry
462+
/// \param ns: The global namespace, for following \p type if it is a
463+
/// struct tag type or a union tag type
464+
/// \return The entry for the symbol and suffix
465+
const value_sett::entryt *get_entry_for_symbol(
466+
const irep_idt identifier,
467+
const typet &type,
468+
const std::string &suffix,
469+
const namespacet &ns) const;
470+
458471
protected:
459472
/// Reads the set of objects pointed to by `expr`, including making
460473
/// recursive lookups for dereference operations etc.

0 commit comments

Comments
 (0)