c c++中的符号模拟答案

【问题标题】：symbolic simulation in c c++c c++中的符号模拟
【发布时间】：2026-01-17 17:05:01
【问题描述】：

我想知道我是否可以看到 C 程序的循环展开形式。例如我有以下 for 循环

// The following code mimics functionality of a logic circuit whose
//inputs are a,b,c and d
//output f
//At every for loop iteration, fresh values of a,b,c and d are input
//to the code whereas k value is used from the previous iteration.

    bool k = 0;
    bool a,b,c,d;
    bool g,h,n,j,f;

    for(i = 1; i < 100; i++)
    {
    h = !(a | b);  //nor gate
    g =  (b & c);  //and gate
    n = !(c & d);  //nand gate
    f = (k==0) ? h : g;  //mux
    j = n ^ f;    //xor gate
    k = j;
    }

问题是“是否可以以可读格式查看该程序的循环展开形式”。我有兴趣了解 gcc 编译器如何表达 h99、g99、n99、f99、j99 和 k99（第 99 次循环迭代中的 h、g、n、f、j 和 k 的值）是否可以这样做？或者应该怎么做才能从输入 a99、b99、c99、d99 到 a1、b1、c1 和 d1 中查看 h99、g99、n99、f99、j99 和 k99 的表达式？

简而言之，我想在每次迭代“i”时进行符号模拟即，将输出 hi、gi、ni、fi、ji 和 ki 用输入 ai、bi、ci、di 表示为 a1、b1、c1 和 d1。

如果您有任何问题，请告诉我。

【问题讨论】：

AFAIK，这是不可能的。如果你想做，我会写一个小预处理器自己做。
你的意思是，like this?
您的意思是要显示每个符号的一系列值？你考虑过printf吗？即打印带有符号名称的简单标题行，并在 for 循环中包含打印语句以显示数据？
a, b, c, d 在这个循环中不会被修改。因此，h、g 和 n 在循环内不会被修改。因此，第一个“优化”是将这些移出循环。此外，j 未使用，可以简单地替换为 k。

标签： c loops simulation unroll

【解决方案1】：

我有兴趣了解 gcc 编译器如何表达 h99、g99、 n99、f99、j99 和 k99（第 99 个循环中的 h、g、n、f、j 和 k 的值迭代）如果它可以这样做？或者应该怎么做才能看到表达式就输入而言，对于 h99、g99、n99、f99、j99 和 k99 a99,b99,c99,d99 降到 a1,b1,c1 和 d1？

从编译器的角度来看，您无法具体查看迭代 99 上要做什么。您可以做的最好的事情是确切地了解如何处理它是双重的。首先，如果你会读汇编程序，你可以使用gcc -S 选项将程序编译成汇编程序。您可能还想包含 -masm=intel 以 intel 格式而不是 ATT 格式输出汇编程序。即：

gcc -S -o prog.asm prog.c -masm=intel

第二，对于值比较，您需要在 第 99 次迭代中转储输入和输出值，并将输入/输出与您期望发生的情况进行比较纸。您可以编写一个小函数来提供类似于以下格式的输出：

void dumpIO (bool a, bool b, bool c, bool d, bool g, bool h, bool n, bool j, bool f)
{
    printf ("%-20s : %d = !(%d | %d);\n", "h = !(a | b)", h, a, b);
    printf ("%-20s : %d = (%d & %d);\n", "g =  (b & c)", g, b, c);
    printf ("%-20s : %d = !(%d & %d);\n", "n = !(c & d)", n, c, d);
    printf ("%-20s : %d = (%d == 0) ? %d : %d;\n", "f = (k==0) ? h : g", f, k, h, g);
    printf ("%-20s : %d = %d ^ %d;\n", "j = n ^ f", j, n, f);
    printf ("%-20s : %d = %d;\n", "k = j", k, j);
}


bool k = 0;
bool a,b,c,d;
bool g,h,n,j,f;

for(i = 1; i < 100; i++)
{
    h = !(a | b);  //nor gate
    g =  (b & c);  //and gate
    n = !(c & d);  //nand gate
    f = (k==0) ? h : g;  //mux
    j = n ^ f;    //xor gate
    k = j;
    if (i == 99) dumpIO(a, b, c, d, g, h, n, j, f);
}

示例输出：

h = !(a | b)        :  0 = !(0 | 1);
g =  (b & c)        :  1 = (1 & 1);
n = !(c & d)        :  1 = !(1 & 0);
f = (k==0) ? h : g  :  0 = (1 == 0) ? 0 : 1;
j = n ^ f           :  1 = 1 ^ 0;
k = j               :  1 = 1;

最令人困惑的问题是您期望在迭代0-98 之间看到的不同？循环中没有任何东西依赖于循环迭代变量i，所以它只是简单地打印相同的东西100次。

我希望这可以为您提供一些您正在寻找的东西。就unrolling 而言，您究竟期望做什么还不太清楚。查看编译器如何处理您的代码，然后验证输入/输出是您能做的最好的事情。

【讨论】：

【解决方案2】：

您应该考虑在正式的推理工具中编写循环的递归版本，例如 ACL2（搜索 ACL2 以下载它，tryacl2.org 上还有一个原始的交互式版本）。然后要求定理证明者通过要求它证明函数的调用等于未知数和 :expand 提示来为您展开循环。类似于以下内容：

(defthm unroll-it
  (equal (my-fun 1 nil nil nil nil nil nil nil nil nil)
         xxx)
  :hints (("Goal" :expand (...some term that you need expanded))))

您可能需要 100 个展开提示，因为默认情况下 ACL2 不会打开递归调用。无论如何，如果你真的开始走这条路，你可以联系 acl2-help 列表。有关 ACL2 声誉的声明，请参见 wikipedia。

【讨论】：