c - CMBC 未报告看似无效的内存访问

Question

我有以下代码片段。

#include<stdio.h>
#include<stdlib.h>
int main()
{
        char *c = malloc(1);
        printf("%p\n", c);
        c = c + 20;

        printf("%p\n", c);
        printf("%d\n", *c);

        free(c - 20);
        return 0;
}

在此代码中，我将 1 个字节的内存分配给指针。然后我正在访问分配内存后 20 个单元的内存位置。当我取消引用该指针时，我预计会收到内存访问冲突错误或段错误或类似的错误。我没有收到任何此类错误。

让我们假设这是一个未定义行为的情况。所以我尝试使用CBMC来验证这个程序，一个著名的模型检查器，使用以下命令。

cbmc test01.c --pointer-check

CBMC 报告该程序是安全的。这是 CBMC 的问题还是我遗漏了什么？

Answer 1

正如您在问题中所说，声明 printf("%d\n", *c);暴露未定义的行为。由于未定义，您对它的任何期望都是错误的。这包括收到特定错误或任何错误。

C 运行时库不会检查程序访问内存的方式。如果这样做的话，程序的运行速度就会慢得多。对于堆，C 运行时库会进行一些基本检查；例如，它在地址 0 处放置某个值在程序启动期间并检查程序结束时该值是否仍然存在。如果值发生更改，则空指针将被取消引用以进行写入，并且它会警告您这一点。

c = c + 20;之后, c最有可能指向属于您的程序的内存块。它可以是堆上的空闲区域，也可以位于堆管理器用来处理堆的数据结构内部，但很有可能它仍然位于同一内存页上。

如果你运气不好并且c + 20落在存储 c 的内存页之外然后发生由操作系统处理的异常情况。它终止程序并显示一条与您在问题中列出的错误消息类似的错误消息(想法相同，每个操作系统上的文字和演示文稿有所不同)。

<小时/>

更新

分配内存并不是某种魔法。程序以一 block 内存块(称为“堆”)开始，操作系统为此目的将内存块分配给程序。

C 运行时库包含管理堆的代码。此代码使用该内存的一小部分进行簿记。常见的实现使用双链表，列表中每个节点的有效负载是程序使用 <memory.h> 中声明的函数“分配”的内存块。 ( malloc() 、 calloc() 等)。当调用malloc()时发生这种情况时，此代码将运行，在列表中创建一个新节点并返回该节点有效负载的地址(堆内的地址)。

程序按照需要使用这个指针。您的程序可以免费编写在 c-1 ， 例如。其实里面malloc()它实际上在那里写了信息。之后malloc()返回c ，你的代码也可以写在 c-1 。来自OS从角度来看，这两个写操作没有区别。因为C不是托管或解释语言，您的程序中不包含任何代码来监视您编写的代码的作用或控制它不要写在错误的地方。

如果您写在 c-1您很有可能破坏堆管理器使用的数据结构。不会立即发生任何错误。没有显示错误消息，并且您的程序继续运行，看起来很正常。但是，在下次调用处理堆的函数(无论是内存分配还是释放)时，程序将开始造成严重破坏。堆数据结构被破坏任何事情都可能发生。

<小时/>

关于CBMC，我不知道它是如何运作的。也许它无法检测到这种情况。或者它可能会报告您的程序是安全的，因为它没有写入 c增加后。