c - 如何在嵌入式 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；它非常昂贵且非常复杂，并且除了上面描述的之外还有很多其他功能。特别引用(省略)白皮书 here :

With abstract interpretation the following program elements are interpreted in new ways:

[...]

• Any global shared data may change at any time in a multitask program, except when protection mechanisms, such as memory locks or critical sections, have been applied

[...]

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

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

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