如何在嵌入式C代码库中查找与数据一致性相关的问题？

Question

让我解释数据一致性问题的含义.以下面的场景为例

uint16 x,y;
x=0x01FF;
y=x;

显然,这些变量是16位,但如果这个代码使用8位CPU,则读或写操作不会是原子的.因此,中间可能发生中断并改变值.这是可能导致数据不一致的一种情况.

这是另一个例子,

if(x>7) //x is global variable
{
 switch(x)
        {
           case 8://do something
                   break;
           case 10://do something
                   break;
           default: //do default
        }
}

在上面的摘录代码中,如果中断在if语句之后但在switch语句之前将x的值从8更改为5,那么我们最终会出现默认情况,而不是情况8.

请注意,我正在寻找方法来检测这种情况(但不是解决方案)

是否有任何工具可以检测嵌入式C中的此类问题？

Answer 1

上下文（线程/中断）感知的静态分析工具可以确定共享数据的使用，并且这样的工具可以识别保护此类数据（或缺乏）的特定机制。

Polyspace Code Prover就是这样的工具之一；它非常昂贵且非常复杂，并且除了上述之外还可以做更多的事情。具体引用（省略）此处的白皮书：

通过抽象解释，以下程序元素可以以新的方式解释：

[...]

• 在多任务程序中，任何全局共享数据都可能随时更改，除非应用了保护机制（例如内存锁或临界区）

[...]

自从我使用它以来，它可能在很长一段时间内有所改进，但我遇到的一个问题是它适用于锁定-访问-解锁习惯用法，您可以在其中向工具指定锁定/解锁调用或宏是什么。问题在于，我从事的 C++ 项目使用了一种更智能的方法，其中锁定对象（例如互斥锁、调度程序锁或中断禁用）在实例化时锁定（在构造函数中）并在析构函数中解锁，以便它自动解锁当对象超出范围时（按范围惯用语锁定）。这意味着解锁对于 Polyspace 来说是隐式且不可见的。然而，它至少可以识别所有共享数据。

该工具的另一个问题是，您必须指定所有线程和中断入口点以进行并发分析，在我的例子中，这些是任务和中断类中的私有虚拟函数，再次使它们对 Polyspace 不可见。这是通过有条件地将入口点公开以仅用于抽象分析来解决的，但这意味着正在测试的代码不具有要运行的代码的确切语义。

当然，这些对于 C 代码来说不是问题，而且根据我的经验，Polyspace 在任何情况下都更成功地应用于 C；您不太可能以适合该工具的风格编写代码，而不是使用适合您现有代码库的工具。