C Semantics in K Framework

[Chucky Ellison <celliso2 AT illinois.edu>]

That's a terribly creative and inefficient way to compute Fibonacci
numbers :)  I'm glad it seems to be working in principle though.

Disabling the GRAPH option will simply prevent the .pdf and .ps files
from being generated.  It will still generate all the other files
(including the huge log file and a .dot file).  It will also not
delete old .pdf or .ps files.

Unless you have GRAPH set on your system, it will be disabled by
default.  On linux machines (at least) you can check by doing a `set |
grep GRAPH`

If it is still trying to generate the pdf and ps, we can try to track
down the bug offline.

In order to get rid of the huge log file, I will have to do some
additional development work.  I created an issue for this.

-Chucky

On Sat, Jun 18, 2011 at 7:47 AM, Derek M Jones 
<derek AT knosof.co.uk>
 wrote:
> Chucky,
>
>> Also, just leave out the GRAPH option and it should be disabled.  You
>> can also disable an option by setting it to nothing, e.g.,
>> SEARCH=1 GRAPH= ./a.out
>
> Neither of those work.
>
> The following has F_n possible outputs where n
> is the n'th Fibonacci number.
>
> n=5 takes under an hour and produces a 4G log file
> n=6 takes 11 hours and filled up the disc partition (I estimate
> the log file at around 50G).
>
>
> #include <stdio.h>
>
> int x;
>
>
> int set_x(int ret_val)
> {
> x=1;
> return ret_val;
> }
>
>
> int two_unspec(void)
> {
> x=0;
> return x + set_x(1);
> }
>
>
> int add_zero(val)
> {
> x=0;
> return val - x + set_x(0);
> }
>
>
> int fib(int fib_num)
> {
> if (fib_num > 3)
>    return fib(fib_num-2) + add_zero(fib(fib_num-1));
> else
>    if (fib_num == 3)
>       return two_unspec();
>    else
>       return 1;
> }
>
> int main(void)
> {
> int n;
>
> // scanf("%d", &n);
> n=5;
> printf("Fibonacci %d = %d\n", n, fib(n));
> }
>
>> the GRAPH option is just for the .pdf and .ps generation though.
>>
>> Thanks Derek,
>> -Chucky
>>
>> On Fri, Jun 17, 2011 at 7:18 AM, Derek M 
>> Jones<derek AT knosof.co.uk>
>>   wrote:
>>> Chucky,
>>>
>>>> The tmpSearchResults.txt is the raw search graph.  This has to get
>>>> generated for me to create the summaries, like the one I print to the
>>>> screen just showing final states.  However, I might be able to process
>>>
>>> A lot of this information appears to be present right at the start of
>>> the tmp... file, it looks like it just needs some reformatting.
>>>
>>> I have tried (not very hard) to switch off graph production.
>>> Using GRAPH=0 did not have the desired effect.
>>> graphviv is installed on my machine, but I have not configured
>>> c-semantics to use it and so get lots of error messages.
>>>
>>>> it on the fly so there is no file generated.  Is that an option you'd
>>>> be interested in?
>>>
>>> It would enable me to try larger values of fib.  Not a particularly
>>> good reason, but others might have filesize problems with more
>>> realistic programs.
>>>
>>>>
>>>> -Chucky
>>>>
>>>> On Thu, Jun 16, 2011 at 9:43 PM, Derek M 
>>>> Jones<derek AT knosof.co.uk>
>>>>     wrote:
>>>>> Chucky,
>>>>>
>>>>>    >>    Did you specify the '-n' option when you compiled?
>>>>>
>>>>> No, but I was thinking very hard that I wanted a complete search :-O
>>>>>
>>>>>> I should add, it really helps to use the -s option as well.  There is
>>>>>> still some nondeterminism kicking around when in linking in the
>>>>>> standard library.  Using the -s option brings the search time down
>>>>>> from 50s to 20 seconds for me.
>>>>>
>>>>> The -s option also reduced the 1.1G tmpSearchResults.txt file by around
>>>>> 70%, obtained when incrementing x to the next 'fib' number.
>>>>>
>>>>> Is there a way to summarise the contents of tmpSearchResults.txt
>>>>> without having to generate it?
>>>>>
>>>>>>
>>>>>> I'll have to look in to it to see if that nondeterminism is necessary
>>>>>> or if it's just slowing things down.
>>>>>>
>>>>>> When the tests finish running and the version gets tagged, r826 should
>>>>>> contain fixes to any spurious "you need to run with -n option"
>>>>>> warnings that were being generated, even if you used the -n option.
>>>>>>
>>>>>> -Chucky
>>>>>>
>>>>>> On Thu, Jun 16, 2011 at 9:02 PM, Chucky 
>>>>>> Ellison<celliso2 AT illinois.edu>
>>>>>>       wrote:
>>>>>>> Unless I'm missing something more subtle, it seems to work for me.
>>>>>>> Did you specify the '-n' option when you compiled?  This is the only
>>>>>>> way SEARCH will return a complete search.  I've attached the .pdf
>>>>>>> graph it generates as well.
>>>>>>>
>>>>>>> $ kcc -n fib.c
>>>>>>> $ ./a.out
>>>>>>> fib = 4
>>>>>>> $ SEARCH=1 GRAPH=1 ./a.out
>>>>>>> Performing the search...
>>>>>>> Generated tmpSearchResults.txt
>>>>>>> Examining the output...
>>>>>>> ========================================================================
>>>>>>> 7 solutions found
>>>>>>> ------------------------------------------------------------------------
>>>>>>> Solution 1
>>>>>>> Program completed successfully
>>>>>>> Return value: 0
>>>>>>> Output:
>>>>>>> fib = 4
>>>>>>> ------------------------------------------------------------------------
>>>>>>> Solution 2
>>>>>>> Program completed successfully
>>>>>>> Return value: 0
>>>>>>> Output:
>>>>>>> fib = 5
>>>>>>> ------------------------------------------------------------------------
>>>>>>> Solution 3
>>>>>>> Program completed successfully
>>>>>>> Return value: 0
>>>>>>> Output:
>>>>>>> fib = 6
>>>>>>> ------------------------------------------------------------------------
>>>>>>> Solution 4
>>>>>>> Program completed successfully
>>>>>>> Return value: 0
>>>>>>> Output:
>>>>>>> fib = 7
>>>>>>> ------------------------------------------------------------------------
>>>>>>> Solution 5
>>>>>>> Program completed successfully
>>>>>>> Return value: 0
>>>>>>> Output:
>>>>>>> fib = 8
>>>>>>> ------------------------------------------------------------------------
>>>>>>> Solution 6
>>>>>>> Program completed successfully
>>>>>>> Return value: 0
>>>>>>> Output:
>>>>>>> fib = 9
>>>>>>> ------------------------------------------------------------------------
>>>>>>> Solution 7
>>>>>>> Program completed successfully
>>>>>>> Return value: 0
>>>>>>> Output:
>>>>>>> fib = 10
>>>>>>> ========================================================================
>>>>>>> 7 solutions found
>>>>>>>
>>>>>>> Generated tmpSearchResults.dot.
>>>>>>> Generating graph...
>>>>>>> Generated tmpSearchResults.ps.
>>>>>>> Generated tmpSearchResults.pdf
>>>>>>>
>>>>>>>
>>>>>>> -Chucky
>>>>>>>
>>>>>>> On Thu, Jun 16, 2011 at 7:26 PM, Derek M 
>>>>>>> Jones<derek AT knosof.co.uk>
>>>>>>>       wrote:
>>>>>>>> Chucky,
>>>>>>>>
>>>>>>>> No programming system is complete without being able
>>>>>>>> to generate the Fibonacci sequence.
>>>>>>>>
>>>>>>>> I was expecting some different orders of evaluation in the
>>>>>>>> following, even if the number of orders is not yet the Fibonacci
>>>>>>>> sequence.
>>>>>>>>
>>>>>>>> #include<stdio.h>
>>>>>>>> int x;
>>>>>>>>
>>>>>>>> int fib(void)
>>>>>>>> {
>>>>>>>> x--;
>>>>>>>> if (x<= 1)
>>>>>>>>       return 1;
>>>>>>>> else
>>>>>>>>       return x + fib();
>>>>>>>> }
>>>>>>>>
>>>>>>>> int main(void)
>>>>>>>> {
>>>>>>>> x=4+1;
>>>>>>>> printf("fib = %dn", fib());
>>>>>>>> }
>>>>>>>>
>>>>>>>>
>>>>>>>> --
>>>>>>>> Derek M. Jones                         tel: +44 (0) 1252 520 667
>>>>>>>> Knowledge Software Ltd                 
>>>>>>>> mailto:derek AT knosof.co.uk
>>>>>>>> Source code analysis                   http://www.knosof.co.uk
>>>>>>>> _______________________________________________
>>>>>>>> c-semantics mailing list
>>>>>>>> c-semantics AT cs.illinois.edu
>>>>>>>> http://lists.cs.uiuc.edu/mailman/listinfo/c-semantics
>>>>>>>>
>>>>>>>
>>>>>>
>>>>>
>>>>> --
>>>>> Derek M. Jones                         tel: +44 (0) 1252 520 667
>>>>> Knowledge Software Ltd                 
>>>>> mailto:derek AT knosof.co.uk
>>>>> Source code analysis                   http://www.knosof.co.uk
>>>>> _______________________________________________
>>>>> c-semantics mailing list
>>>>> c-semantics AT cs.illinois.edu
>>>>> http://lists.cs.uiuc.edu/mailman/listinfo/c-semantics
>>>>>
>>>>
>>>
>>> --
>>> Derek M. Jones                         tel: +44 (0) 1252 520 667
>>> Knowledge Software Ltd                 
>>> mailto:derek AT knosof.co.uk
>>> Source code analysis                   http://www.knosof.co.uk
>>> _______________________________________________
>>> c-semantics mailing list
>>> c-semantics AT cs.illinois.edu
>>> http://lists.cs.uiuc.edu/mailman/listinfo/c-semantics
>>>
>>
>
> --
> Derek M. Jones                         tel: +44 (0) 1252 520 667
> Knowledge Software Ltd                 
> mailto:derek AT knosof.co.uk
> Source code analysis                   http://www.knosof.co.uk
> _______________________________________________
> c-semantics mailing list
> c-semantics AT cs.illinois.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/c-semantics
>