Hi,

Apologies if this is misplaced as an "issue" - I couldn't locate any discussion groups and I doubt there's an active tis-interpreter tag on SO. If there's a better place to take this, please let me know.

I've been running against the Argon2 library. After some code changes so that it didn't fail on pthreads, I'm seeing this error:

/code/src/blake2/blake2b.c:195:[kernel] warning: accessing uninitialized left-value:
                  assert \initialized(&m[blake2b_sigma[r][2*0+0]]);
                  stack: blake2b_compress :: /code/src/blake2/blake2b.c:229 <-
                         blake2b_update :: /code/src/blake2/blake2b.c:339 <-
                         blake2b_long :: /code/src/core.c:145 <-
                         finalize :: /code/src/argon2.c:75 <-

The file in question is here:

https://github.com/P-H-C/phc-winner-argon2/blob/master/src/blake2/blake2b.c

And the line in question reduces down to:

v[0] = v[0] + v[1] + m[0];

Both v[0] and m[0] are initialised earlier in that function, so every possible interpretation I have of this is that it's a false positive. Unfortunately the analyser then refuses to go on and analyse the rest of the codebase.

• Have I read this error correctly? Could it be referring to a genuine bug in a way I am not seeing?
• If this is a false positive, how can I go on to analyse the rest of the application? I have played around with using memset to zero out m[] and the error did not go away (further suggesting there is something else going on).

Finally, thank you for this product. It's something the industry has needed.

Source code:

#include <limits.h>
#include <stdio.h>

int main()
{
  printf(">%*d", INT_MAX, 1);
}

tis-interpreter (3615ce825dfb8a5e66ba60c0e62e9c2131f1cd2d) output:

[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
Segmentation fault

Source code:

#include <stdio.h>

int main()
{
  _Bool b;
  *(char *)&b = 123;
  printf("%d\n", *(char *)&b);
}

tis-interpreter (d4961d3fa420ebd5b895e7c54636acae8ada344e) output:

[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed

123

[value] done for function main

gcc (GCC) 7.0.0 20160528 (experimental):

$ gcc -std=c11 -pedantic -Wall -Wextra -O3 test.c && ./a.out
1

clang version 3.9.0 (trunk 271117):

$ clang -std=c11 -Weverything -O3 test.c && ./a.out
123

Source code:

#include <stdio.h>

int main()
{
  _Bool b;
  *(char *)&b = 123;
  printf("b = %d\n", b);
}

tis-interpreter (d68f7f3c395cd46ca84b9c10c54ce800b7052c2d) output:

[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed

b = 123

[value] done for function main

gcc 6 w/ubsan output:

bool-repr.c:7:3: runtime error: load of value 123, which is not a valid value for type '_Bool'
b = 1

clang 3.9 w/ubsan output:

bool-repr.c:7:22: runtime error: load of value 123, which is not a valid value for type '_Bool'
b = 1

It seems that some files have been shuffled around, causing tis-interpreter/tis-interpreter.sh to fail when running the example commands given in tis-interpreter/EXAMPLES.md. It looks like both the markdown doc and the shell script will have to be changed. I started tweaking the shell script, but I'm off to bed for now. I thought I'd mention it - I'm happy to finish it tomorrow if someone hasn't taken care of it by then.

Best, Mike

I'm getting the following message:

rec_layer_s3.c:204:[value] warning: The following sub-expression cannot be evaluated:
                 (align - (size_t)1) % (unsigned long)8

                 All sub-expressions with their values:
                 size_t  (size_t)1 ∈ {1}
                 unsigned long  (unsigned long)8 ∈ {8}
                 size_t  align - (size_t)1 ∈ {{ (size_t)&__malloc_CRYPTO_malloc_l92_3251[4] }}
                 size_t  align ∈ {{ (size_t)&__malloc_CRYPTO_malloc_l92_3251[5] }}
                 int  1 ∈ {1}
                 int  8 ∈ {8}

I'm guessing that you don't really assign a real address to what malloc returned, preventing you to actually do any calculation with those pointers. It seems we're using a size_t for it, but I guess using an (u)intptr_t will not make any difference.

$ tis-interpreter.sh test.c
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed

100

[value] done for function main
$ 
$ cat test.c
int printf (const char *, ...); 

int a = 100; 

void foo (int p)
{
  a = 0;
}

int main ()
{
  foo (a);
  printf ("%d\n", a); 
  return 0; 
}
$ 

Source code:

#include <string.h>

int main()
{
  char s[1] = "";
  strcpy(s, s);
}

tis-interpreter (274be6de79973f11ab62a3c77d0981882734cb2d) output:

[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] done for function main

Source code:

#include <stdio.h>

int main()
{
  struct s {
    char s[3];
  } ab = {"ab"};

  union {
    struct {
      struct s s1;
      char eol1;
    };
    struct {
      char c;
      struct s s2;
      char eol2;
    };
  } u;

  u.s1 = ab;
  printf("%s -> ", u.s1.s);
  u.s2 = u.s1; // (1)
  u.eol2 = 0;
  printf("%s\n", u.s2.s);

  u.s2 = ab;
  printf("%s -> ", u.s2.s);
  u.s1 = u.s2; // (2)
  u.eol1 = 0;
  printf("%s\n", u.s1.s);
}

tis-interpreter (429543c4b7e9e4751f9e29b5a2f9686594e0b322) output:

[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed

ab -> 

ab


ab -> 

ab

[value] done for function main

gcc 7 w/ubsan output:

ab -> abb
ab -> ab

clang 3.9 w/ubsan output:

ab -> ab
ab -> a

C11, 6.5.16.1p3: "If the value being stored in an object is read from another object that overlaps in any way the storage of the first object, then the overlap shall be exact and the two objects shall have qualified or unqualified versions of a compatible type; otherwise, the behavior is undefined."

We see that the code from gcc is wrong for (1) and the code from clang is wrong for (2) so this UB is a problem in practice.

The code doesn't compile on my Linux machine. The make step fails:

ocamlc.opt: don't know what to do with src/plugins/callgraph.
Usage: ocamlc <options> <files>
...
share/Makefile.generic:70: recipe for target 'src/plugins/callgraph/options.cmi' failed
make: *** [src/plugins/callgraph/options.cmi] Error 2

It's invoking:

ocamlc.opt -c -w @a-3-4-6-9-41-44-45-48-50 -bin-annot -warn-error +a-32-33-34-35-36-37-38-39 -g -I src/plugins/slicing_types \
  -I src/plugins/pdg_types -I src/plugins/value_types -I src/libraries/stdlib -I src/libraries/utils -I src/libraries/project \
  -I src/libraries/datatype -I src/kernel_internals/parsing -I src/kernel_internals/typing -I src/kernel_internals/runtime \
  -I src/kernel_services/parsetree -I src/kernel_services/ast_data -I src/kernel_services/ast_queries -I src/kernel_services/ast_printing \
  -I src/kernel_services/cmdline_parameters -I src/kernel_services/plugin_entry_points -I src/kernel_services/abstract_interp \
  -I src/kernel_services/visitors -I src/kernel_services/analysis -I src/kernel_services/ast_transformations \
  -I src/plugins/gui -I /home/rprichard/work/tis-interpreter/lib/plugins -I lib -I devel_tools \
  -I /home/rprichard/.opam/system/lib/findlib -I /home/rprichard/.opam/system/lib/zarith \
  -I -I -I -I src/plugins/callgraph -I /home/rprichard/work/tis-interpreter/lib/plugins src/plugins/callgraph/options.mli

Notice the -I -I -I -I src/plugins/callgraph.

I suspect the problem comes from these lines in the Makefile:

##########
# Zarith #
##########

ifeq ($(HAS_ZARITH),yes)
BYTE_LIBS+= zarith.cma easy_format.cmo biniou.cma yojson.cmo
OPT_LIBS+= zarith.cmxa easy_format.cmx biniou.cmxa yojson.cmx
EASYFORMAT_PATH=$(shell ocamlfind query easy-format)
BINIOU_PATH=$(shell ocamlfind query biniou)
YOJSON_PATH=$(shell ocamlfind query yojson)
INCLUDES+= -I $(ZARITH_PATH) -I $(EASYFORMAT_PATH) -I $(BINIOU_PATH) -I $(YOJSON_PATH)
src/libraries/stdlib/integer.ml: \
        src/libraries/stdlib/integer.zarith.ml share/Makefile.config
    $(REPLACE) $< [email protected]
    $(CHMOD_RO) [email protected]
else
src/libraries/stdlib/integer.ml: \
        src/libraries/stdlib/integer.bigint.ml share/Makefile.config
    $(REPLACE) $< [email protected]
    $(CHMOD_RO) [email protected]
endif
GENERATED += src/libraries/stdlib/integer.ml

I don't have the easy-format, biniou, or yojson packages installed.

Here's my full build output: https://gist.github.com/rprichard/053db9cdcffccef8ae07673082cf31a9

I'm using 64-bit Debian Jessie with the system OCaml (4.01.0-5) and OPAM 1.2.0. I installed the zarith OPAM package, and I have these OPAM packages:

[email protected]:~/work/tis-interpreter$ opam list
# Installed packages for system:
base-bigarray     base  Bigarray library distributed with the OCaml compiler
base-threads      base  Threads library distributed with the OCaml compiler
base-unix         base  Unix library distributed with the OCaml compiler
conf-gmp             1  Virtual package relying on a GMP lib system installation.
conf-m4              1  Virtual package relying on m4
conf-ncurses         1  Virtual package relying on ncurses
conf-perl            1  Virtual package relying on perl
conf-pkg-config    1.0  Virtual package relying on pkg-config installation.
ocamlfind        1.6.2  A library manager for OCaml
zarith           1.4.1  Implements arithmetic and logical operations over arbitrary-precision integers

I tried using the TIS Interpreter on libsecp256k1, it didn't work because of lacking uint128_t support. I know this is not standard C, but since GCC supports it, I wonder if it could be added.

We are currently studying the usage of GCC builtins by GitHub projects and how well various tools support them. To that end, we are also developing a test suite for the most frequently used machine-independent GCC builtins (available at https://github.com/gcc-builtins/tests/tree/master/test-cases). We'd be glad to contribute the test suite (or parts of it) to the project, if you are interested.

While evaluating the builtin support in Frama-C, I was advised to use the -machdep gcc_x86_32 flag to enable support for compiler extensions. When turning on this flag for the tis-interpreter, it successfully executed 88 out of 100 builtin test cases. Surprisingly (to me at least), it correctly executed the __sync builtin test cases and the __builtin_object_size test case which seem to be a problem for Frama-C.

In terms of failing test cases, 11 tests failed since the NAN and INFINITY macros were not implemented, which is not related to builtin support itself (they are also not supported by Frama-C). However, 10 of these test cases also failed because the builtins were not recognized; these builtins provided operations to compare floating point numbers (__builtin_isinf, __builtin_islessgreater, __builtin_isless, __builtin_copysign, __builtin_islessequal, __builtin_isgreaterequal, __builtin_isnan, __builtin_signbit, __builtin_isunordered, __builtin_isgreater). Furthermore, __builtin_memchr was not supported. The test case below results in the warning warning: Calling undeclared function __builtin_memchr. Old style K&R code?:

#include <assert.h>
#include <string.h>

char* str = "hello test!";

int main() {
  char needle = '!';
  assert(__builtin_memchr(str, needle, strlen(str)) == &str[10]);
}

Note: I realized that the latest binary snapshop is from 2016. I will try to test with a newer version.

Hello,

I have a parser and a lot of generated test cases. Every test case have it's own main entry point. How do i catch issues/errors from tis-interpreter.sh?

I have a script similar to:

#!/bin/sh

for file in $(find generated_test_cases -type f -name '*.c');
do
    echo "tis-interpreter analyzing file: $file"
    if ! output=$(/home/developer/tis-interpreter/tis-interpreter.sh my_parser.c $file --cc "-I."); then
        echo "File $file had some problems:"
        echo $output
        exit 1
    fi
done

exit 0

However, the tis-interpreter.sh script always returns 0 even if i add a bug in the code. Are there any other ways of catching this?

$ ./configure

$ ocaml --version

The OCaml toplevel, version 4.06.0

...

$ make

Copying to   src/plugins/value/domains/apron/apron_domain.ml
Building     ocamlgraph
make[1]: Entering directory '/home/guest/Gits/Compiler/tis-interpreter/ocamlgraph'
ocamlc.opt -c -I src -I lib -g -dtypes lib/bitv.ml
File "lib/bitv.ml", line 464, characters 27-39:
Warning 3: deprecated: String.set
Use Bytes.set instead.
File "lib/bitv.ml", line 464, characters 27-28:
Error: This expression has type string but an expression was expected of type
         bytes
make[1]: *** [Makefile:553: lib/bitv.cmo] Error 2
make[1]: Leaving directory '/home/guest/Gits/Compiler/tis-interpreter/ocamlgraph'
Ocamlc       src/libraries/project/state_builder.cmi
File "src/libraries/project/state_builder.mli", line 38, characters 21-28:
Error: Unbound module State
make: *** [share/Makefile.generic:71: src/libraries/project/state_builder.cmi] Error 2

how fix?

Tried building it on OS X 10.10.5 with Xcode 7.2.1

Ocamlc       src/libraries/utils/hook.cmi
Ocamlc       src/libraries/utils/hook.cmo
File "src/libraries/utils/hook.ml", line 1:
Error: The implementation src/libraries/utils/hook.ml
       does not match the interface src/libraries/utils/hook.cmi:
       ...
       At position module Build(P) : <here>
       Values do not match:
         val extend : ('_a -> unit) -> unit
       is not included in
         val extend : (param -> result) -> unit
       File "src/libraries/utils/hook.ml", line 61, characters 6-12:
         Actual declaration
make: *** [src/libraries/utils/hook.cmo] Error 2

Configured it like this (just copy/pasted from INSTALL.md)

./configure --prefix=`pwd`/tis-interpreter/tis-interpreter --disable-from_analysis --disable-gui --disable-impact --disable-inout --disable-metrics --disable-occurrence --disable-pdg --disable-postdominators --enable-rtegen --disable-scope --disable-slicing --disable-sparecode --enable-users --disable-aorai --disable-obfuscator --disable-report --disable-security_slicing --disable-wp --disable-wp-coq --disable-wp-why3 --disable-print_api --with-all-static
configure: ******************
configure: * CONFIGURE MAKE *
configure: ******************
checking for make... make
checking version of make... 3.81
configure: *****************************
configure: * CONFIGURE OCAML COMPILERS *
configure: *****************************
checking for ocamlc... ocamlc
checking version of OCaml... 4.05.0
checking OCaml library path... /usr/local/lib/ocaml
checking for ocamlopt... ocamlopt
checking ocamlopt version and standard library... ok
checking for ocamlc.opt... ocamlc.opt
checking ocamlc.opt version and standard library... ok
checking for ocamlopt.opt... ocamlopt.opt
checking ocamlc.opt version and standard library... ok
configure: *******************************************
configure: * CONFIGURE MANDATORY TOOLS AND LIBRARIES *
configure: *******************************************
checking for ocamldep... ocamldep
checking for ocamldep.opt... ocamldep.opt
checking for ocamllex... ocamllex
checking for ocamllex.opt... ocamllex.opt
checking for ocamlyacc... ocamlyacc
checking for ocamlfind... ocamlfind
configure: ******************************************
configure: * CONFIGURE OPTIONAL TOOLS AND LIBRARIES *
configure: ******************************************
checking for ocamldoc... ocamldoc
checking for ocamldoc.opt... ocamldoc.opt
checking for ocamlmktop... ocamlmktop
checking for ocamlcp... ocamlcp
checking for otags... no
configure: no package ocamlgraph in ocamlfind
configure: switching to OcamlGraph provided by Frama-C
checking for ocamlgraph... no
checking for ocamlgraph.tar.gz... yes
configure: unarchiving ocamlgraph.tar.gz
configure: configuring ocamlgraph...
ocamlfind: Package `lablgtk2' not found
configure: WARNING: lablgnomecanvas not found: the graph editor and view_graph will not be compiled
checking for Zarith... configure: WARNING: Zarith not found: will use the default less efficient library instead
checking for Apron... not found. The corresponding domains won't be available in Eva
configure: **********************
configure: * CONFIGURE PLATFORM *
configure: **********************
checking platform... Unix
checking OCaml native threads... ok.
checking for gcc... gcc
checking whether the C compiler works... yes
checking for C compiler default output file name... a.out
checking for suffix of executables... 
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether we are using the GNU C compiler... yes
checking whether gcc accepts -g... yes
checking for gcc option to accept ISO C89... none needed
checking how to run the C preprocessor... gcc -E
checking for grep that handles long lines and -e... /usr/bin/grep
checking for egrep... /usr/bin/grep -E
checking for ANSI C header files... yes
checking for sys/types.h... yes
checking for sys/stat.h... yes
checking for stdlib.h... yes
checking for string.h... yes
checking for memory.h... yes
checking for strings.h... yes
checking for inttypes.h... yes
checking for stdint.h... yes
checking for unistd.h... yes
checking for stdlib.h... (cached) yes
checking assert.h usability... yes
checking assert.h presence... yes
checking for assert.h... yes
checking float.h usability... yes
checking float.h presence... yes
checking for float.h... yes
checking math.h usability... yes
checking math.h presence... yes
checking for math.h... yes
checking signal.h usability... yes
checking signal.h presence... yes
checking for signal.h... yes
checking for unistd.h... (cached) yes
checking how to run the C preprocessor... gcc -E
/* Check whether comments are kept in output */
Default preprocessor is 'gcc -E -C -I.'.
configure: ***************************
configure: * WISHED FRAMA-C PLUG-INS *
configure: ***************************
checking for src/plugins/callgraph... yes
callgraph... yes
checking for src/plugins/constant_propagation... yes
semantic_constant_folding... yes
checking for src/plugins/from... yes
from_analysis... no
checking for src/plugins/gui... yes
gui... no
checking for src/plugins/impact... yes
impact... no
checking for src/plugins/inout... yes
inout... no
checking for src/plugins/metrics... yes
metrics... no
checking for src/plugins/occurrence... yes
occurrence... no
checking for src/plugins/pdg... yes
pdg... no
checking for src/plugins/postdominators... yes
postdominators... no
checking for src/plugins/rte... yes
rtegen... yes
checking for src/plugins/scope... yes
scope... no
checking for src/plugins/slicing... yes
slicing... no
checking for src/plugins/sparecode... yes
sparecode... no
checking for src/plugins/users... yes
users... yes
checking for src/plugins/value... yes
value_analysis... yes
checking for src/plugins/aorai/Makefile.in... yes
aorai... no
checking for src/plugins/obfuscator/Makefile.in... yes
obfuscator... no
checking for src/plugins/print_api... yes
print_api... no
checking for src/plugins/report/Makefile.in... yes
report... no
checking for src/plugins/security_slicing/Makefile.in... yes
security_slicing... no
checking for src/plugins/wp/Makefile.in... yes
wp... no
configure: *******************************************************
configure: * CONFIGURE TOOLS AND LIBRARIES USED BY SOME PLUG-INS *
configure: *******************************************************
ocamlfind: Package `lablgtk2' not found
Ocamlfind -> using +lablgtk2.(,/usr/local/lib/ocaml/lablgtk2)
checking for /usr/local/lib/ocaml/lablgtk2/lablgtksourceview2.cmxa... no
checking for /usr/local/lib/ocaml/lablgtk2/lablgnomecanvas.cmxa... no
checking for /usr/local/lib/ocaml/lablgtk2/lablgtk.cmxa... no
checking for dot... yes
checking for /usr/local/lib/ocaml/dynlink.cmxa... yes
native dynlink works fine. Great.
configure: *************************************
configure: * CHECKING FOR PLUG-IN DEPENDENCIES *
configure: *************************************
configure: WARNING: lablgtksourceview2.cmxa not found
configure: WARNING: lablgnomecanvas.cmxa not found
configure: WARNING: /usr/local/lib/ocaml/lablgtk2/lablgtk.cmxa not found.
configure: WARNING: callgraph partially enabled because gui not enabled.
configure: WARNING: value_analysis only partially enabled because gui not enabled.
configure: *********************
configure: * CREATING MAKEFILE *
configure: *********************
configure: creating ./config.status
config.status: creating src/plugins/obfuscator/Makefile
config.status: creating src/plugins/report/Makefile
config.status: creating src/plugins/aorai/Makefile
config.status: creating src/plugins/security_slicing/Makefile
config.status: creating src/plugins/wp/Makefile
config.status: creating share/Makefile.config
configure: *******************************
configure: * SUMMARY: PLUG-INS AVAILABLE *
configure: *******************************
configure: callgraph: partial, static, gui not enabled
configure: semantic_constant_folding: yes, static
configure: from_analysis: no
configure: gui: no
configure: impact: no
configure: inout: no
configure: metrics: no
configure: occurrence: no
configure: pdg: no
configure: postdominators: no
configure: rtegen: yes
configure: scope: no
configure: slicing: no
configure: sparecode: no
configure: users: yes, static
configure: value_analysis: partial, static, gui not enabled
configure: aorai: no
configure: obfuscator: no
configure: print_api: no
configure: report: no
configure: security_slicing: no
configure: wp: no

make output:

Linking     bin/toplevel.byte
File "_none_", line 1:
Error: Cannot find file yojson.cmo
Makefile:1358: recipe for target 'bin/toplevel.byte' failed

.opam/system/install/yojson.install output:

lib: [
  "_build/install/default/lib/yojson/META" {"META"}
  "_build/install/default/lib/yojson/opam" {"opam"}
  "_build/install/default/lib/yojson/yojson.cmi"
  "_build/install/default/lib/yojson/yojson.cmx"
  "_build/install/default/lib/yojson/yojson.cmt"
  "_build/install/default/lib/yojson/yojson.cmti"
  "_build/install/default/lib/yojson/yojson.mli"
  "_build/install/default/lib/yojson/yojson_biniou.cmi"
  "_build/install/default/lib/yojson/yojson_biniou.cmx"
  "_build/install/default/lib/yojson/yojson_biniou.cmt"
  "_build/install/default/lib/yojson/yojson_biniou.cmti"
  "_build/install/default/lib/yojson/yojson_biniou.mli"
  "_build/install/default/lib/yojson/yojson.cma"
  "_build/install/default/lib/yojson/yojson.cmxa"
  "_build/install/default/lib/yojson/yojson.a"
  "_build/install/default/lib/yojson/yojson.cmxs"
]