Help with running examples

[jsburke]

Hi Everyone,

I'm working with your work here a bit but can tell I'm struggling a bit. I'm hoping you can help a bit. Currently, this is what I've gotten

~/verifying-constant-time/examples/sort master$ ../../tools/smack/bin/smack.py --verifier=boogie --entry-points sort3_wrapper --unroll 1 --loop-limit 1 -bpl /home/john/verifying-constant-time/examples/sort/sort_multiplex.bpl  /home/john/verifying-constant-time/examples/sort/sort_multiplex.c
SMACK program verifier version 1.5.1
llvm2bpl: Unknown command line argument '-enable-type-inference-opts'.  Try: 'llvm2bpl --help'
llvm2bpl: Did you mean '--enable-objc-arc-opts'?
llvm2bpl: Unknown command line argument '-enable-type-inference-opts'.  Try: 'llvm2bpl --help'
llvm2bpl: Did you mean '--enable-objc-arc-opts'?

Error invoking command:
llvm2bpl /home/john/verifying-constant-time/examples/sort/a-1MYgHL.bc -bpl /home/john/verifying-constant-time/examples/sort/sort_multiplex.bpl -source-loc-syms -enable-type-inference-opts -entry-points sort3_wrapper -mem-mod-impls
llvm2bpl returned non-zero.

I'm calling smack.py via the submodule to ease things on the device I'm using. It looks like I may need some update to llvm2bpl but I'm unsure. I also am not sure what I should see on the last line (returning non-zero) if the code is constant time or not.

I didn't do any software installs to run this, and I think maybe I need to? Any guidance for getting good results from this would be very appreciated.

Thanks John

[fdupress]

Thanks John.

The setup for ct-verif is not robust, and requires very precise versions of llvm and smack, and possibly of bam as well. A student of mine recently put together a container definition file that seems to set everything up right, and I'm asking him how he prefers to contribute it.

Depending on exactly what you want to do, it might be worth considering whether a more robust solution—perhaps without the complex partial product—would be sufficient. Are you able to share what kind of code you're looking to verify?

[zh-yming]

Hi John, I've met the same problem as you described when trying to verify the example file(sort.c). Have you solved it?