symbolic simulation in c c++

Question

I am wondering if i could see the loop unrolled form of a C program. For example i have the following for loop

// 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;
    }

The question is that "is it possible to see the loop unrolled form of this program in a readable format". I am interested in seeing how the gcc compiler expresses h99, g99, n99, f99, j99 and k99 (values of h, g, n, f, j and k in the 99th loop iteration) if it can do so? Or what should be done to see expressions for h99, g99, n99, f99, j99 and k99 in terms of the inputs a99,b99,c99,d99 down to a1,b1,c1 and d1?

In nutshell, i want to do symbolic simulation at every iteration "i" i.e., express the outputs hi, gi, ni, fi, ji and ki in terms of inputs ai,bi,ci,di down to a1,b1,c1 and d1.

Please let me know if you have any questions.

AFAIK, this isn't possible. If you want to do it, I'd write a small preprocessor to do it yourself. — slugonamission, Feb 12 '13 at 15:45
You mean, [like this](http://stackoverflow.com/questions/2391442/how-to-see-the-optimized-code-in-c)? — netcoder, Feb 12 '13 at 15:49
you mean that you want to display the series of values for each symbol? Have you considered printf? ie print a simple header row with symbol names, and include a print statement in your for loop to display the data? — Simon Bergot, Feb 12 '13 at 15:59
`a`, `b`, `c`, `d` are not modified inside this loop. Therefore, `h`, `g`, and `n` are not modified inside the loop. So the very first "optimization" would be to move these out of the loop. Also, `j` is unused, and can trivially be replaced with `k`. — Jongware, Aug 09 '14 at 21:34

score 0 · Answer 1 · answered Aug 09 '14 at 21:17

You should consider writing a recursive version of your loop in a formal reasoning tool, like ACL2 (search for ACL2 to download it, there's also a primitive interactive version at tryacl2.org). Then ask the theorem prover to unroll the loop for you by asking it to prove that a call of the function equals something unknown and :expand hints. Something like the following:

(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))))

You might need 100 expand hints, as ACL2 doesn't open up recursive calls by default. Anyway, you can contact the acl2-help list if you actually start going down this road. See wikipedia for a statement of ACL2's reputability.

David C. Rankin · Answer 2 · 2014-08-09T23:02:25.647

I am interested in seeing how the gcc compiler expresses h99, g99, n99, f99, j99 and k99 (values of h, g, n, f, j and k in the 99th loop iteration) if it can do so? Or what should be done to see expressions for h99, g99, n99, f99, j99 and k99 in terms of the inputs a99,b99,c99,d99 down to a1,b1,c1 and d1?

There is nothing you can do from a compiler standpoint to see what is to be done on iteration 99 specifically. About the best you can do to see exactly how it will be treated is twofold. First, if you can read assembler, you can compile the program to assembler using the gcc -S option. You may also want to inclue the -masm=intel to output the assembler in intel as opposed to ATT format. I.e.:

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

Second, for value comparison, you will want to dump the input and output values on the 99th iteration and compare the input/outputs to what you expect to happen on paper. You can write a small function to provide formatted output similar to:

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);
}

example output:

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;

The most bewildering issue is what you expect to see differently between iterations 0-98? Nothing in the loop is dependent on the loop iteration variable i, so it is simply going to print the same thing 100 times.

I hope this provides you with some of what you were looking for. It was somewhat unclear exactly what you were expecting to be about to do as far as unrolling is concerned. Looking at how the compiler treats your code and then validating the input/output is about the best you can do.

symbolic simulation in c c++

2 Answers2