跟踪未初始化的静态变量

Question

我需要调试一个丑陋而庞大的数学C库,可能是由f2c生成的.代码滥用局部静态变量,不幸的是它似乎在某处利用了这些自动初始化为0的事实.如果使用相同的输入两次调用其入口函数,则它会给出不同的结果.如果我卸载库并重新加载它,它可以正常工作.它需要很快,所以我想摆脱加载/卸载.

我的问题是如何使用valgrind或任何其他工具发现这些错误,而无需手动遍历整个代码.

我正在寻找声明本地静态变量的地方,先读取,然后再写.由于静态变量有时会通过指针进一步传递(是的 - 它太丑了),这个问题更加复杂了.

我理解有人可以说这样的错误不应该被自动工具检测到,因为在某些情况下这恰好是预期的行为.还有,有没有办法让自动初始化的本地静态变量"脏"？

Answer 1

魔鬼在细节中,但这可能对你有用:

首先,获得Frama-C.如果您使用的是Unix,那么您的发行版可能包含一个包.该软件包不会是最后一个版本,但它可能已经足够好了,如果以这种方式安装它会节省一些时间.

假设您的示例如下所示,只有这么大,以至于不明显出现了什么问题:

int add(int x, int y)
{
  static int state;
  int result = x + y + state; // I tested it once and it worked.
  state++;
  return result;
}

输入如下命令:

frama-c -lib-entry -main add -deps ugly.c

选项-lib-entry -main add意味着"看功能add".选项-deps计算功能依赖性.您将在日志中找到这些"功能依赖项":

[from] Function add:
     state FROM state; (and default:false)
     \result FROM x; y; state; (and default:false)

这列出了依赖的结果的实际输入add,以及从这些输入计算的实际输出,包括从中读取和修改的静态变量.在使用之前正确初始化的静态变量通常不会显示为输入,除非分析器在读取之前无法确定它始终是初始化的.

日志显示state为依赖关系\result.如果您希望返回的结果仅依赖于参数(意味着具有相同参数的两个调用产生相同的结果),那么这里提示可能存在错误state.

上面几行中显示的另一个提示是函数修改state.

这可能有所帮助.选项-lib-entry意味着分析器不会假设任何非常量静态变量在调用分析函数时保持其值,因此对于代码来说可能过于不精确.有很多方法可以解决这个问题,但是你是否想赌博学习这些方法的时间取决于你.

编辑:这是一个更复杂的例子:

void initialize_1(int *p)
{
  *p = 0;
}

void initialize_2(int *p)
{
  *p; // I made a mistake here.
}

int add(int x, int y)
{
  static int state1;
  static int state2;

  initialize_1(&state1);
  initialize_2(&state2);

  // This is safe because I have initialized state1 and state2:
  int result = x + y + state1 + state2; 

  state1++;
  state2++;
  return result;
}

在此示例中,相同的命令会生成结果:

[from] Function initialize_1:
         state1 FROM p
[from] Function initialize_2:
[from] Function add:
         state1 FROM \nothing
         state2 FROM state2
         \result FROM x; y; state2

你看到的initialize_2是一个空的依赖列表,这意味着该函数没有任何指定.我将通过显示一个显式消息而不仅仅是一个空列表来使这个案例更清楚.如果你知道任何的功能initialize_1,initialize_2或者add是应该做的,你可以比较这先验知识的分析结果,看到的东西是错误的initialize_2和add.

第二次编辑:现在我的例子显示了一些奇怪的东西initialize_1,所以也许我应该解释一下.变量state1取决于用于写入p的意义,如果不同,则最终值将不同.这是最后一个例子:pstate1pstate1

int t[10];

void initialize_index(int i)
{
  t[i] = 1;
}

int main(int argc, char **argv)
{
  initialize_index(argv[1][0]-'0');
}

使用该命令frama-c -deps t.c,计算的依赖项为initialize_index:

[from] Function initialize_index:
         t[0..9] FROM i (and SELF)

这意味着每个单元依赖于i(如果i是特定单元的索引,则可以修改它).每个单元格也可以保留其值(如果i指示另一个单元格):这(and SELF)在最新版本中提及时表示,并且(and default:true)在先前版本中更加模糊.