2

我想知道我是否可以看到 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”时进行符号模拟，即用输入 ai、bi、ci、di 表示输出 hi、gi、ni、fi、ji 和 ki，直到 a1、b1、c1 和d1。

请让我知道，如果你有任何问题。

4

2 回答 2

0

我有兴趣了解 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 的表达式？

从编译器的角度来看，您无法做任何事情来具体了解在第99次迭代中要做什么。您可以做的最好的事情是确切地了解如何处理它是双重的。首先，如果您可以阅读汇编程序，则可以使用该gcc -S选项将程序编译为汇编程序。您可能还希望包含以-masm=intelintel 格式而不是 ATT 格式输出汇编程序。IE：

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。查看编译器如何处理您的代码然后验证输入/输出是您能做的最好的事情。

于 2014-08-09T22:22:33.210 回答
0

您应该考虑在正式推理工具中编写循环的递归版本，例如 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。

于 2014-08-09T21:17:03.757 回答