cbmc/src/goto-instrument/skip_loops.cpp at develop · diffblue/cbmc · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
/*******************************************************************\

Module: Skip over selected loops by adding gotos

Author: Michael Tautschnig

Date: January 2016

\*******************************************************************/

/// \file
/// Skip over selected loops by adding gotos

#include "skip_loops.h"

#include <util/message.h>
#include <util/string2int.h>

#include <goto-programs/goto_model.h>

typedef std::set<unsigned> loop_idst;
typedef std::map<irep_idt, loop_idst> loop_mapt;

static bool skip_loops(
  goto_programt &goto_program,
  const loop_idst &loop_ids,
  messaget &message)
{
  loop_idst::const_iterator l_it=loop_ids.begin();
  Forall_goto_program_instructions(it, goto_program)
  {
    if(l_it==loop_ids.end())
      break;
    if(!it->is_backwards_goto())
      continue;

    const unsigned loop_id=it->loop_number;
    if(*l_it<loop_id)
      break; // error handled below
    if(*l_it>loop_id)
      continue;

    goto_programt::targett loop_head=it->get_target();
    goto_programt::targett next=it;
    ++next;
    CHECK_RETURN(next != goto_program.instructions.end());

    goto_program.insert_before(
      loop_head,
      goto_programt::make_goto(
        next, true_exprt(), loop_head->source_location()));

    ++l_it;
  }
  if(l_it!=loop_ids.end())
  {
    message.error() << "Loop " << *l_it << " not found"
                    << messaget::eom;
    return true;
  }

  return false;
}

static bool parse_loop_ids(
  const std::string &loop_ids,
  loop_mapt &loop_map)
{
  std::string::size_type length=loop_ids.length();

  for(std::string::size_type idx=0; idx<length; idx++)
  {
    std::string::size_type next=loop_ids.find(",", idx);
    std::string val=loop_ids.substr(idx, next-idx);
    std::string::size_type delim=val.rfind(".");

    if(delim==std::string::npos)
      return true;

    std::string fn=val.substr(0, delim);
    unsigned nr = safe_string2unsigned(std::string_view{val}.substr(delim + 1));

    loop_map[fn].insert(nr);

    if(next==std::string::npos)
      break;
    idx=next;
  }

  return false;
}

bool skip_loops(
  goto_modelt &goto_model,
  const std::string &loop_ids,
  message_handlert &message_handler)
{
  messaget message(message_handler);

  loop_mapt loop_map;
  if(parse_loop_ids(loop_ids, loop_map))
  {
    message.error() << "Failed to parse loop ids" << messaget::eom;
    return true;
  }

  loop_mapt::const_iterator it=loop_map.begin();
  for(auto &gf_entry : goto_model.goto_functions.function_map)
  {
    if(it == loop_map.end() || it->first < gf_entry.first)
      break; // possible error handled below
    else if(it->first == gf_entry.first)
    {
      if(skip_loops(gf_entry.second.body, it->second, message))
        return true;
      ++it;
    }
  }
  if(it!=loop_map.end())
  {
    message.error() << "No function " << it->first << " in goto program"
                    << messaget::eom;
    return true;
  }

  // update counters etc.
  goto_model.goto_functions.update();

  return false;
}