ufo documentation / basic how-to

[charlie....@gmail.com]

Greetings,

I was able to build ufo on a fresh ubuntu 13 platform (hurray!). I tried to run an smt benchmark, but run-bench.py said I needed a config file. What is the basic usage for ufo? Could you provide any documentation? We are very interested in using ufo.

I've attached the rudimentary shell script I came up with in case it helps others. I ran into problems trying to build llvm 2.6 with gcc 4.7, and used gcc 4.4 instead.

Thanks,

Charlie Jacobsen
University of Utah

[Arie Gurfinkel]

(replying through the group)

Hey Charlie, thanks for the build script!

First, a comment and a question:
  1. You can use git version of LDD library from SF. It is more current than the tar distro. For me, it compiles out of the box on Ubuntu 12.04, 13.04 and OSX Mountain Lion. Let me know if it does not for you and I'll update the repo.

  2. Have you tried using llvm-gcc to compile llvm-2.6? It is annoying to have to install so many versions of gcc. I am able to compile it with gcc-4.6 on Ubuntu 12.04 and llvm-gcc-4.2 on OSX.

On Tue, May 21, 2013 at 2:34 AM,  <> wrote:
> Greetings,
>
> I was able to build ufo on a fresh ubuntu 13 platform (hurray!). I tried to
> run an smt benchmark, but run-bench.py said I needed a config file. What is
> the basic usage for ufo? Could you provide any documentation? We are very
> interested in using ufo.

The easiest way to run ufo is to use the sv-comp settings. See here: https://bitbucket.org/arieg/ufo/wiki/svcomp13

PATH_TO_UFO/bin/ufo-svcomp-par.py [OPTIONS] file

Should do the trick.

run-bench.py is a script I use to run regression tests. It is not intendent to be used by others and is not documented. For quick runs, you would be better to use sv-scomp scripts that run the tool and generate nice graphical output. None-the-less, here is my command line for run-bench.py:

time $(arch) -R ../bin/run-bench.py --cpu=200 --ufo=../bin/ufo-svcomp-par.py --config=empty --svcomp=/home/arie/sv-benchmarks /home/arie/sv-benchmarks/ControlFlowInteger.set

time           prints total runtime at the end

$(arch) -R   disables ASLR ( http://en.wikipedia.org/wiki/Address_space_layout_randomization )

empty        is an empty file. The content of file specified by --config is appended to command line arguments of executable specified in --ufo

the rest are self-explanatory

This will generate an output directory out.<SOMETHING>. The directory contains a file 'stats' that is a csv list of results. Furthermore, for each input X, it contains X.stdout and X.stderr that are logs of stdout and stderr streams produced while running X.

Hope this helps,

cheers,

arie

[charlie....@gmail.com]

Thanks Arie :)

On Tuesday, May 21, 2013 9:12:43 AM UTC-6, Arie Gurfinkel wrote:

(replying through the group)

Hey Charlie, thanks for the build script!

First, a comment and a question:
  1. You can use git version of LDD library from SF. It is more current than the tar distro. For me, it compiles out of the box on Ubuntu 12.04, 13.04 and OSX Mountain Lion. Let me know if it does not for you and I'll update the repo.

Good to know, I'll do that.
 

  2. Have you tried using llvm-gcc to compile llvm-2.6? It is annoying to have to install so many versions of gcc. I am able to compile it with gcc-4.6 on Ubuntu 12.04 and llvm-gcc-4.2 on OSX.

I point to llvm-gcc when I configure the build for llvm 2.6, but it still seemed to use gcc/g++ for at least part of the build. I'll confirm that, it might be an error in the build script.

On Tue, May 21, 2013 at 2:34 AM,  <> wrote:
> Greetings,
>
> I was able to build ufo on a fresh ubuntu 13 platform (hurray!). I tried to
> run an smt benchmark, but run-bench.py said I needed a config file. What is
> the basic usage for ufo? Could you provide any documentation? We are very
> interested in using ufo.

The easiest way to run ufo is to use the sv-comp settings. See here: https://bitbucket.org/arieg/ufo/wiki/svcomp13

PATH_TO_UFO/bin/ufo-svcomp-par.py [OPTIONS] file

Should do the trick.

run-bench.py is a script I use to run regression tests. It is not intendent to be used by others and is not documented. For quick runs, you would be better to use sv-scomp scripts that run the tool and generate nice graphical output. None-the-less, here is my command line for run-bench.py:

time $(arch) -R ../bin/run-bench.py --cpu=200 --ufo=../bin/ufo-svcomp-par.py --config=empty --svcomp=/home/arie/sv-benchmarks /home/arie/sv-benchmarks/ControlFlowInteger.set

time           prints total runtime at the end

$(arch) -R   disables ASLR ( http://en.wikipedia.org/wiki/Address_space_layout_randomization )

empty        is an empty file. The content of file specified by --config is appended to command line arguments of executable specified in --ufo

the rest are self-explanatory

This will generate an output directory out.<SOMETHING>. The directory contains a file 'stats' that is a csv list of results. Furthermore, for each input X, it contains X.stdout and X.stderr that are logs of stdout and stderr streams produced while running X.

Great! I'll try it out.
 

[Arie Gurfinkel]

On Tue, May 21, 2013 at 11:51 AM, <charlie....@gmail.com> wrote:
> Thanks Arie :)
>
>
> On Tuesday, May 21, 2013 9:12:43 AM UTC-6, Arie Gurfinkel wrote:
>>
>> (replying through the group)
>>
>> Hey Charlie, thanks for the build script!
>>
>> First, a comment and a question:
>> 1. You can use git version of LDD library from SF. It is more current
>> than the tar distro. For me, it compiles out of the box on Ubuntu 12.04,
>> 13.04 and OSX Mountain Lion. Let me know if it does not for you and I'll
>> update the repo.
>
>
> Good to know, I'll do that.
>
>>
>>
>> 2. Have you tried using llvm-gcc to compile llvm-2.6? It is annoying to
>> have to install so many versions of gcc. I am able to compile it with
>> gcc-4.6 on Ubuntu 12.04 and llvm-gcc-4.2 on OSX.
>
>
> I point to llvm-gcc when I configure the build for llvm 2.6, but it still
> seemed to use gcc/g++ for at least part of the build. I'll confirm that, it
> might be an error in the build script.

llvm-2.6 needs to know where llvm-gcc is for its compilation process.
However, this does not affect the compiler that configure picks to
compile llvm itself. To change the compiler you have to set CC and CXX
variables (as you do in the script). I am suggesting to set them to
llvm-gcc. So it will look like:

<PATH_TO_LLVM>/configure CC=llvm-gcc CXX=llvm-g++ <REST OF CONFIG OPTIONS>

assuming that some version of llvm-gcc is in the path (otherwise give
full paths to the tools above).

cheers,
arie

> --
> You received this message because you are subscribed to the Google Groups
> "UFO General Discussion Group" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to ufo-discuss...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.
>
>

[charlie....@gmail.com]

Ah, right, okay, I'll do that. Once I iron out everything in the build script, I'll re-post

[charlie....@gmail.com]

Okay, got it! Thanks for your help.

I've attached an updated build script. It appears to work on a fresh minimal ubuntu 13. I ended up using gcc-4.4/g++-4.4 for all builds, I had the most luck with it (llvm-gcc still gave build errors that required extra fixes). I was able to run ufo on a SystemC benchmark file. It appears to be working correctly.

[Arie Gurfinkel]

Thank you!

sincerely,

arie