In the Readme Run section you use LL files as inputs.

Does it support BC and LL files as input? Or only LL?

Does it make a difference from performance, memory usage to have one big LL file/BC file or numerous BC/LL files?

What are the best practices, best approach?

Thanks,

Hi,

the README.md claims that llvm-8 is a dependency for building sys. In fact from looking at stack.yaml it becomes clear that LLVM 9 is needed (the llvm-hs dependencies are all for LLVM 9).

Also, I've whipped up a Dockerfile -- based on Debian testing -- that can be used to effortlessly build a working version of sys:

https://gist.github.com/rpw/289afe7d01fb82533f7a839c8e1689bd

Feel free to integrate if you find it suitable.

Hi,

I'm trying to run Sys from the Docker image on a large code base I built using wllvm, but I'm getting this error when I run any of the checkers:

unhandled function attribute enum value: FunctionAttributeKind 26
CallStack (from HasCallStack):
error, called at src/LLVM/Internal/Attribute.hs:210:17 in llvm-hs-9.0.1-GdcY7lIsVQ6GWzw7sPUMKI:LLVM.Internal.Attribute

Not sure if this is a result of something I'm doing wrong or if llvm-hs is the problem. Any help would be greatly appreciated.

Thanks!

I spend some time to build this and it is quite a hassle especially for the boolector part.
For future use - could you supply a Dockerfile? That would make using this much easier :)

Working on project where I got the ll (assembly language format files) files for arm architecture.

Will it also work on it?

Do I have to specify some extra flags?

I think it is architecture independent, but got some errors like below:

DecodeException "Unknown DW_OP 4097"
DecodeException "Unknown DW_OP 148" 

Thanks,

Tell me if I am insane or if this has a chance at detecting CVE-2020-15999 style bugs.

Writing a static checker that marks 16 bit magnitude allocated mallocs and warns when they get 32 bit magnitude accesses?

I tried to use WLLVM to compile a huge program. Then I got a excuteable file , and I used the command 'extract-bc' which was came from WLLVM to get the *.ll file. Finally, I used sys to check bugs, but I got a error "DecodeException "Unknown subclass id for DINode: MDSubclassID 26".
I found some clue about the problem in the llvm-hs project.
"Comparing LLVM Specialized Metadata Nodes with llvm-hs supported Metadata subclasses "
llvm-hs/llvm-hs#307
Is there anyone knows how to slove the isssue? or, Is there any other way to get the ll file in a huge program?
Thanks!

Right now, we do thread walking through the function to build paths.
This is kind of insane.
We should instead have a simple Kildall pass, which will make things a ton faster.
(We can keep the thread walking approach just in case its still helpful for people)

Hi,

experiencing some OOM issues while running in Docker on powerful box with 84 GB Ram.

[431166.569778] Out of memory: Killed process 3400451 (sys) total-vm:1160377588kB, anon-rss:77285872kB, file-rss:0kB, shmem-rss:0kB, UID:1000 pgtables:164212kB oom_score_adj:0

Tried to set stack.yml

jobs: 1

Is this setting it to one job? I see all CPU cores are in use ....

Anything else I can do to reduce memory usage, slow down the processing but avoid OOM?

How many threads is it actually starting? As many as cores? Can you reference some code link?

Sorry if this is little bit off topic/general, but there is little info about Haskell and your project, or is it me that is Haskell beginner. Those question can help folks running it.

Thanks,

Sounds like a great project. Would like to dig deeper into it.

Stack uninit bug
Name "serial_read_mp_array_73"
in 
Name "serial_read_mp_array"
path-to-file
[UnName 4,UnName 71]
If you inspect the serial_read_mp_array() function, the buggy block path is %4 (the first block) to %71,where we use [%73].

Can you elaborate with more words, maybe C equivalent of the code to see the bug.

I am new to LLVM and *.ll (LLVM IR) output seems kind of cryptic. Where can I learn more about to understand it? LL LLVM syntax (LLVM IR) ? Showing with your example would be a great help.

I run it on sample project (freetype2) and got results with concroob check i.e

Potential OOB index of
Right 4294967295
4294967295
Name "sfnt_get_var_ps_name_490"
is
path possible
in file
/tmp/freetype-2.10.3/objs/sfnt.ll
in function
Name "sfnt_get_var_ps_name"
on path
[UnName 1,UnName 135,UnName 288,UnName 289,UnName 306,UnName 319,UnName 457,UnName 458,UnName 459,UnName 466]

How to interpret it?

Below is the sfnt.ll for reference.

https://github.com/marcinguy/public/blob/master/sfnt.ll

I run the sys with the uninit check:

stack exec sys -- -c uninit -e prod -d ./compile_out/

However, after a long while, it failed with the timed out error:

Timed out
CallStack (from HasCallStack):
  error, called at src/Symex/Symex/Boolector.hs:242:18 in adverse-0.0.0.1-8OpQWnI8CptBIFknhXSwPz:Symex.Symex.Boolector
Timed out
CallStack (from HasCallStack):
  error, called at src/Symex/Symex/Boolector.hs:242:18 in adverse-0.0.0.1-8OpQWnI8CptBIFknhXSwPz:Symex.Symex.Boolector
Timed out
CallStack (from HasCallStack):
  error, called at src/Symex/Symex/Boolector.hs:242:18 in adverse-0.0.0.1-8OpQWnI8CptBIFknhXSwPz:Symex.Symex.Boolector

I wonder whether there is an option or modification of code to change the default time for solver to solve the constraint, in order to avoid the timed out case.

There was a problem with the installation that I couldn't solve

ubuntu:~/sys-M/sys-master$ stack build
WARNING: Ignoring adverse's bounds on llvm-hs (>=9.0.1); using llvm-hs-9.0.0.
Reason: allow-newer enabled.
Building all executables for `adverse' once. After a successful build of all of them, only specified executables will be rebuilt.
adverse> configure (lib + exe)
Configuring adverse-0.0.0.1...
adverse> build (lib + exe)
Preprocessing library for adverse-0.0.0.1..
Building library for adverse-0.0.0.1..
[ 1 of 49] Compiling Control.Log [flags changed]
[ 2 of 49] Compiling LLVMAST.ASTInterface [flags changed]
[ 3 of 49] Compiling LLVMAST.ConstantInterface [flags changed]
[ 4 of 49] Compiling LLVMAST.OperandInterface [flags changed]
[ 5 of 49] Compiling LLVMAST.OrdInstances [flags changed]
[ 6 of 49] Compiling LLVMAST.RenameVariables [flags changed]
[ 7 of 49] Compiling InternalIR.ModuleInfo [flags changed]
[ 8 of 49] Compiling LLVMAST.TypeInterface [flags changed]
[ 9 of 49] Compiling LLVMAST.Interface [flags changed]
[10 of 49] Compiling InternalIR.SimplePath [flags changed]
[11 of 49] Compiling InternalIR.SSA [flags changed]
[12 of 49] Compiling InternalIR.PathExpand [flags changed]
[13 of 49] Compiling InternalIR.PathExpand.Refinements.EnterCall [flags changed]
[14 of 49] Compiling InternalIR.PathInfo [flags changed]
[15 of 49] Compiling Paths_adverse [flags changed]
[16 of 49] Compiling Static.CheckerState [flags changed]
[17 of 49] Compiling Static.CheckerConfigDef [flags changed]
[18 of 49] Compiling Static.Check [flags changed]
[19 of 49] Compiling Checkers.Utils.StaticUtils [flags changed]
[20 of 49] Compiling Checkers.UserInputStatic [flags changed]
[21 of 49] Compiling Checkers.UninitStatic [flags changed]
[22 of 49] Compiling Checkers.HeapOOBStatic [flags changed]
[23 of 49] Compiling Checkers.ConcreteOOBStatic [flags changed]
[24 of 49] Compiling Static.Kildall [flags changed]
[25 of 49] Compiling Symex.Symex.Boolector [flags changed]
[26 of 49] Compiling Symex.Symex.Utils [flags changed]
[27 of 49] Compiling Symex.Symex.SymexState [flags changed]
[28 of 49] Compiling Symex.Symex.Variable

/home/sys-M/sys-master/src/Symex/Symex/Variable.hs:240:44: error:
Variable not in scope:
getOffsetOfElement
:: GHC.Ptr.Ptr LLVM.Internal.FFI.DataLayout.DataLayout
-> t0 -> Integer -> IO Word64
|
240 | withFFIDataLayout dl (\layout -> getOffsetOfElement layout ety $ fromIntegral ind)
| ^^^^^^^^^^^^^^^^^^

-- While building package adverse-0.0.0.1 (scroll up to its section to see the error) using:
/home/.stack/setup-exe-cache/x86_64-linux/Cabal-simple_mPHDZzAJ_2.4.0.1_ghc-8.6.5 --builddir=.stack-work/dist/x86_64-linux/Cabal-2.4.0.1 build lib:adverse exe:sys --ghc-options " -fdiagnostics-color=always"
Process exited with code: ExitFailure 1
ubuntu:~/sys-M/sys-master$

Sys output

Stack uninit bug
Name "gmed_n_91"
in
Name "gmed_n"
[UnName 2,UnName 12,UnName 33,UnName 34,UnName 85]
"/tmp/test.ll"
on line
7

C Code:

user@2d2d788ad909:~/src/sys$ cat /tmp/test.c 
#define NMAX    9 
#include <stdio.h>
typedef short Word16;

Word16 gmed_n(            /* o : the median value    */
		Word16 ind[],   /* i : input values        */
		Word16 n        /* i : number of inputs    */
	     )
{
	Word16 i, j, ix = 0;
	Word16 max;
	Word16 medianIndex;
	Word16  tmp[NMAX];
	Word16  tmp2[NMAX];

	for (i = 0; i < n; i++)
	{
		*(tmp2 + i) = *(ind + i);
	}

	for (i = 0; i < n; i++)
	{
		max = -32767;
		for (j = 0; j < n; j++)
		{
			if (*(tmp2 + j) >= max)
			{
				max = *(tmp2 + j);
				ix = j;
			}
		}
		*(tmp2 + ix) = -32768;
		*(tmp + i) = ix;
	}


	medianIndex = *(tmp + (n >> 1));  /* account for complex addressing */

	return (*(ind + medianIndex)); <--- here should be uninit Bug per Sys
}

int main()
{
	short a[5]={1,32767,3,4,5};
	int i = 0;
	short res;
	res=gmed_n(a,5);
	printf("%i\n",res);
}

here is the bug:

return (*(ind + medianIndex)); <--- here should be uninit Bug per Sys

However tmp in the line above is referenced and assigned good values in for loop.

Any explanation why Sys flagged it? Using static and symbolic execution

Working on a real project and would like to understand Sys better.

Thanks in advance

LL for reference:

; ModuleID = 'test.c'
source_filename = "test.c"
target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128"
target triple = "x86_64-pc-linux-gnu"

@__const.main.a = private unnamed_addr constant [5 x i16] [i16 1, i16 32767, i16 3, i16 4, i16 5], align 2
@.str = private unnamed_addr constant [4 x i8] c"%i\0A\00", align 1

; Function Attrs: noinline nounwind optnone uwtable
define dso_local signext i16 @gmed_n(i16*, i16 signext) #0 {
  %3 = alloca i16*, align 8
  %4 = alloca i16, align 2
  %5 = alloca i16, align 2
  %6 = alloca i16, align 2
  %7 = alloca i16, align 2
  %8 = alloca i16, align 2
  %9 = alloca i16, align 2
  %10 = alloca [9 x i16], align 16
  %11 = alloca [9 x i16], align 16
  store i16* %0, i16** %3, align 8
  store i16 %1, i16* %4, align 2
  store i16 0, i16* %7, align 2
  store i16 0, i16* %5, align 2
  br label %12

12:                                               ; preds = %30, %2
  %13 = load i16, i16* %5, align 2
  %14 = sext i16 %13 to i32
  %15 = load i16, i16* %4, align 2
  %16 = sext i16 %15 to i32
  %17 = icmp slt i32 %14, %16
  br i1 %17, label %18, label %33

18:                                               ; preds = %12
  %19 = load i16*, i16** %3, align 8
  %20 = load i16, i16* %5, align 2
  %21 = sext i16 %20 to i32
  %22 = sext i32 %21 to i64
  %23 = getelementptr inbounds i16, i16* %19, i64 %22
  %24 = load i16, i16* %23, align 2
  %25 = getelementptr inbounds [9 x i16], [9 x i16]* %11, i64 0, i64 0
  %26 = load i16, i16* %5, align 2
  %27 = sext i16 %26 to i32
  %28 = sext i32 %27 to i64
  %29 = getelementptr inbounds i16, i16* %25, i64 %28
  store i16 %24, i16* %29, align 2
  br label %30

30:                                               ; preds = %18
  %31 = load i16, i16* %5, align 2
  %32 = add i16 %31, 1
  store i16 %32, i16* %5, align 2
  br label %12

33:                                               ; preds = %12
  store i16 0, i16* %5, align 2
  br label %34

34:                                               ; preds = %82, %33
  %35 = load i16, i16* %5, align 2
  %36 = sext i16 %35 to i32
  %37 = load i16, i16* %4, align 2
  %38 = sext i16 %37 to i32
  %39 = icmp slt i32 %36, %38
  br i1 %39, label %40, label %85

40:                                               ; preds = %34
  store i16 -32767, i16* %8, align 2
  store i16 0, i16* %6, align 2
  br label %41

41:                                               ; preds = %67, %40
  %42 = load i16, i16* %6, align 2
  %43 = sext i16 %42 to i32
  %44 = load i16, i16* %4, align 2
  %45 = sext i16 %44 to i32
  %46 = icmp slt i32 %43, %45
  br i1 %46, label %47, label %70

47:                                               ; preds = %41
  %48 = getelementptr inbounds [9 x i16], [9 x i16]* %11, i64 0, i64 0
  %49 = load i16, i16* %6, align 2
  %50 = sext i16 %49 to i32
  %51 = sext i32 %50 to i64
  %52 = getelementptr inbounds i16, i16* %48, i64 %51
  %53 = load i16, i16* %52, align 2
  %54 = sext i16 %53 to i32
  %55 = load i16, i16* %8, align 2
  %56 = sext i16 %55 to i32
  %57 = icmp sge i32 %54, %56
  br i1 %57, label %58, label %66

58:                                               ; preds = %47
  %59 = getelementptr inbounds [9 x i16], [9 x i16]* %11, i64 0, i64 0
  %60 = load i16, i16* %6, align 2
  %61 = sext i16 %60 to i32
  %62 = sext i32 %61 to i64
  %63 = getelementptr inbounds i16, i16* %59, i64 %62
  %64 = load i16, i16* %63, align 2
  store i16 %64, i16* %8, align 2
  %65 = load i16, i16* %6, align 2
  store i16 %65, i16* %7, align 2
  br label %66

66:                                               ; preds = %58, %47
  br label %67

67:                                               ; preds = %66
  %68 = load i16, i16* %6, align 2
  %69 = add i16 %68, 1
  store i16 %69, i16* %6, align 2
  br label %41

70:                                               ; preds = %41
  %71 = getelementptr inbounds [9 x i16], [9 x i16]* %11, i64 0, i64 0
  %72 = load i16, i16* %7, align 2
  %73 = sext i16 %72 to i32
  %74 = sext i32 %73 to i64
  %75 = getelementptr inbounds i16, i16* %71, i64 %74
  store i16 -32768, i16* %75, align 2
  %76 = load i16, i16* %7, align 2
  %77 = getelementptr inbounds [9 x i16], [9 x i16]* %10, i64 0, i64 0
  %78 = load i16, i16* %5, align 2
  %79 = sext i16 %78 to i32
  %80 = sext i32 %79 to i64
  %81 = getelementptr inbounds i16, i16* %77, i64 %80
  store i16 %76, i16* %81, align 2
  br label %82

82:                                               ; preds = %70
  %83 = load i16, i16* %5, align 2
  %84 = add i16 %83, 1
  store i16 %84, i16* %5, align 2
  br label %34

85:                                               ; preds = %34
  %86 = getelementptr inbounds [9 x i16], [9 x i16]* %10, i64 0, i64 0
  %87 = load i16, i16* %4, align 2
  %88 = sext i16 %87 to i32
  %89 = ashr i32 %88, 1
  %90 = sext i32 %89 to i64
  %91 = getelementptr inbounds i16, i16* %86, i64 %90
  %92 = load i16, i16* %91, align 2
  store i16 %92, i16* %9, align 2
  %93 = load i16*, i16** %3, align 8
  %94 = load i16, i16* %9, align 2
  %95 = sext i16 %94 to i32
  %96 = sext i32 %95 to i64
  %97 = getelementptr inbounds i16, i16* %93, i64 %96
  %98 = load i16, i16* %97, align 2
  ret i16 %98
}

; Function Attrs: noinline nounwind optnone uwtable
define dso_local i32 @main() #0 {
  %1 = alloca [5 x i16], align 2
  %2 = alloca i32, align 4
  %3 = alloca i16, align 2
  %4 = bitcast [5 x i16]* %1 to i8*
  call void @llvm.memcpy.p0i8.p0i8.i64(i8* align 2 %4, i8* align 2 bitcast ([5 x i16]* @__const.main.a to i8*), i64 10, i1 false)
  store i32 0, i32* %2, align 4
  %5 = getelementptr inbounds [5 x i16], [5 x i16]* %1, i64 0, i64 0
  %6 = call signext i16 @gmed_n(i16* %5, i16 signext 5)
  store i16 %6, i16* %3, align 2
  %7 = load i16, i16* %3, align 2
  %8 = sext i16 %7 to i32
  %9 = call i32 (i8*, ...) @printf(i8* getelementptr inbounds ([4 x i8], [4 x i8]* @.str, i64 0, i64 0), i32 %8)
  ret i32 0
}

; Function Attrs: argmemonly nounwind
declare void @llvm.memcpy.p0i8.p0i8.i64(i8* nocapture writeonly, i8* nocapture readonly, i64, i1 immarg) #1

declare dso_local i32 @printf(i8*, ...) #2

attributes #0 = { noinline nounwind optnone uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "min-legal-vector-width"="0" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }
attributes #1 = { argmemonly nounwind }
attributes #2 = { "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }

!llvm.module.flags = !{!0}
!llvm.ident = !{!1}

!0 = !{i32 1, !"wchar_size", i32 4}
!1 = !{!"clang version 9.0.1-16 "}

after install the dependencies ；
and run the command: git checkout cleanup
an error occur:

Hi,

More checkers explanations than in Whitepaper (https://cseweb.ucsd.edu/~dstefan/pubs/brown:2020:sys.pdf) & tutorial as well as doc on SysDSL, with examples, would be great.

Thanks,

What does the "Right" and value mean?

If path is possible does it mean the OOB is possible? Or it has to state "attack is possible"?

Tried to pinpoint the code, but wasn't able to... seems like this is a linked function. Don't know how to find it.

Can somebody explain the output of this check and help to diagnose the finding?

Or the bug is not "real", "effective"?

Potential OOB index of
Right 4294967295
4294967295
Name "_ZNSt3__113__vector_baseIdNS_9allocatorIdEEED2Ev_56"
is
path possible
in file
/local/frameworks/base/media/native/midi/libmidi/android_arm_armv7-a-neon_krait_core_shared/obj/frameworks/base/media/native/midi/.midi.o.ll
in function
Name "_ZNSt3__113__vector_baseIdNS_9allocatorIdEEED2Ev"
on path
[UnName 1,UnName 37,UnName 44,UnName 48]

Potential OOB index of
Right 4294967295
4294967295
Name "_ZNSt3__113__vector_baseIxNS_9allocatorIxEEED2Ev_56"
is
path possible
in file
/local/frameworks/base/media/native/midi/libmidi/android_arm_armv7-a-neon_krait_core_shared/obj/frameworks/base/media/native/midi/.midi.o.ll
in function
Name "_ZNSt3__113__vector_baseIxNS_9allocatorIxEEED2Ev"
on path
[UnName 1,UnName 37,UnName 44,UnName 48]

Potential OOB index of
Right 4294967295
4294967295
Name "_ZNSt3__113__vector_baseIiNS_9allocatorIiEEED2Ev_56"
is
path possible
in file
/local/frameworks/base/media/native/midi/libmidi/android_arm_armv7-a-neon_krait_core_shared/obj/frameworks/base/media/native/midi/.midi.o.ll
in function
Name "_ZNSt3__113__vector_baseIiNS_9allocatorIiEEED2Ev"
on path
[UnName 1,UnName 37,UnName 44,UnName 48]

C source - https://github.com/marcinguy/public/blob/master/midi.cpp
LL - https://github.com/marcinguy/public/blob/master/midi.o.ll (with debugs)

Help is appreciated.

Thanks,

It also makes sense to do a wllvm compilation of some pieces of the browser and enter all function calls (especially for the uninit memory checker). This will probably lead to a lot more bugs, because we won't have to be a conservative with fp suppression

Some bitcode files for firefox generate Write too large error.

How to reproduce:

stack exec -- sys -c uninit -e prod -d firefox_ll_files/vp9_segmentation.ll-O2_p

Bitcode is available here.

And the error is raised here:

Which seems like some kind of arbitrary limit that can be changed? Changing it to 20k fixed the error. I'm not sure if that would break something in Sys.

(Using clang-9 and bleeding edge firefox)

-Suyash

CC @epyeh

On longer block bounds, there are a number of reports related to unentered loops (that can never feasibly be unenetered).
Probably makes sense to just optionally ignore things that come from skipping loop headers (the LLVM has a %loop annotation we can use)

boolector> configure
boolector> Configuring boolector-0.0.0.11...
boolector> Cabal-simple_mPHDZzAJ_2.4.0.1_ghc-8.6.5: Missing dependency on a foreign
boolector> library:
boolector> * Missing (or bad) header file: boolector.h
boolector> * Missing (or bad) C library: boolector
boolector> This problem can usually be solved by installing the system package that
boolector> provides this library (you may need the "-dev" version). If the library is
boolector> already installed but in a non-standard location then you can use the flags
boolector> --extra-include-dirs= and --extra-lib-dirs= to specify where it is.If the
boolector> library file does exist, it may contain errors that are caught by the C
boolector> compiler at the preprocessing stage. In this case you can re-run configure
boolector> with the verbosity flag -v3 to see the error messages.
boolector> If the header file does exist, it may contain errors that are caught by the C
boolector> compiler at the preprocessing stage. In this case you can re-run configure
boolector> with the verbosity flag -v3 to see the error messages.
boolector>
Progress 1/2

-- While building package boolector-0.0.0.11 (scroll up to its section to see the error) using:
/root/.stack/setup-exe-cache/x86_64-linux-tinfo6/Cabal-simple_mPHDZzAJ_2.4.0.1_ghc-8.6.5 --builddir=.stack-work/dist/x86_64-linux-tinfo6/Cabal-2.4.0.1 configure --with-ghc=/root/.stack/programs/x86_64-linux/ghc-tinfo6-8.6.5/bin/ghc-8.6.5 --with-ghc-pkg=/root/.stack/programs/x86_64-linux/ghc-tinfo6-8.6.5/bin/ghc-pkg-8.6.5 --user --package-db=clear --package-db=global --package-db=/root/.stack/snapshots/x86_64-linux-tinfo6/0b693a77e93e365d112c81e2d9b2336adf17b99088fe2e0015d8b8497be8fd28/8.6.5/pkgdb --libdir=/root/.stack/snapshots/x86_64-linux-tinfo6/0b693a77e93e365d112c81e2d9b2336adf17b99088fe2e0015d8b8497be8fd28/8.6.5/lib --bindir=/root/.stack/snapshots/x86_64-linux-tinfo6/0b693a77e93e365d112c81e2d9b2336adf17b99088fe2e0015d8b8497be8fd28/8.6.5/bin --datadir=/root/.stack/snapshots/x86_64-linux-tinfo6/0b693a77e93e365d112c81e2d9b2336adf17b99088fe2e0015d8b8497be8fd28/8.6.5/share --libexecdir=/root/.stack/snapshots/x86_64-linux-tinfo6/0b693a77e93e365d112c81e2d9b2336adf17b99088fe2e0015d8b8497be8fd28/8.6.5/libexec --sysconfdir=/root/.stack/snapshots/x86_64-linux-tinfo6/0b693a77e93e365d112c81e2d9b2336adf17b99088fe2e0015d8b8497be8fd28/8.6.5/etc --docdir=/root/.stack/snapshots/x86_64-linux-tinfo6/0b693a77e93e365d112c81e2d9b2336adf17b99088fe2e0015d8b8497be8fd28/8.6.5/doc/boolector-0.0.0.11 --htmldir=/root/.stack/snapshots/x86_64-linux-tinfo6/0b693a77e93e365d112c81e2d9b2336adf17b99088fe2e0015d8b8497be8fd28/8.6.5/doc/boolector-0.0.0.11 --haddockdir=/root/.stack/snapshots/x86_64-linux-tinfo6/0b693a77e93e365d112c81e2d9b2336adf17b99088fe2e0015d8b8497be8fd28/8.6.5/doc/boolector-0.0.0.11 --dependency=base=base-4.12.0.0 --dependency=containers=containers-0.6.0.1 --dependency=directory=directory-1.3.3.0 --dependency=mtl=mtl-2.2.2 --dependency=temporary=temporary-1.3-D5m7D56K5ufHMiVDJGp2II --dependency=time=time-1.8.0.2 --extra-include-dirs=/usr/include/boolector --exact-configuration --ghc-option=-fhide-source-paths
Process exited with code: ExitFailure 1

hello, I use the follow code to test the ability of heapoob ,but it is not detected

int main()
{
int a;
char* ptr=malloc(1000);
ptr[2000]=0xa;
int b=a+10;
return b;
}