is_threaded.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Over-approximate Concurrency for Threaded Goto Programs
 
Author: Daniel Kroening
 
Date: October 2012
 
\*******************************************************************/
 
 
#include "is_threaded.h"
 
#include "ai.h"
 
class is_threaded_domaint:public ai_domain_baset
{
public:
  bool reachable;
  bool is_threaded;
 
  is_threaded_domaint():
    reachable(false),
    is_threaded(false)
  {
    // this is bottom
  }
 
  bool merge(const is_threaded_domaint &src, trace_ptrt, trace_ptrt)
  {
    INVARIANT(src.reachable,
              "Abstract states are only merged at reachable locations");
 
    bool old_reachable=reachable;
    bool old_is_threaded=is_threaded;
 
    reachable=true;
    is_threaded|=src.is_threaded;
 
    return old_reachable!=reachable ||
           old_is_threaded!=is_threaded;
  }
 
  void transform(
    const irep_idt &,
    trace_ptrt trace_from,
    const irep_idt &,
    trace_ptrt,
    ai_baset &,
    const namespacet &) override
  {
    locationt from{trace_from->current_location()};
 
    INVARIANT(reachable,
              "Transformers are only applied at reachable locations");
 
    if(from->is_start_thread())
      is_threaded=true;
  }
 
  void make_bottom() final override
  {
    reachable=false;
    is_threaded=false;
  }
 
  void make_top() final override
  {
    reachable=true;
    is_threaded=true;
  }
 
  void make_entry() final override
  {
    reachable=true;
    is_threaded=false;
  }
 
  bool is_bottom() const override final
  {
    DATA_INVARIANT(reachable || !is_threaded,
                   "A location cannot be threaded if it is not reachable.");
 
    return !reachable;
  }
 
  bool is_top() const override final
  {
    return reachable && is_threaded;
  }
};
 
void is_threadedt::compute(const goto_functionst &goto_functions)
{
  // the analysis doesn't actually use the namespace, fake one
  symbol_tablet symbol_table;
  const namespacet ns(symbol_table);
 
  ait<is_threaded_domaint> is_threaded_analysis;
 
  is_threaded_analysis(goto_functions, ns);
 
  for(const auto &gf_entry : goto_functions.function_map)
  {
    forall_goto_program_instructions(i_it, gf_entry.second.body)
    {
      auto domain_ptr = is_threaded_analysis.abstract_state_before(i_it);
      if(static_cast<const is_threaded_domaint &>(*domain_ptr).is_threaded)
        is_threaded_set.insert(i_it);
    }
  }
}