Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Running docker image outputs "Error running securify." on macOS #69

Open
mihairaulea opened this issue Dec 6, 2018 · 27 comments
Open
Labels
Bug Something isn't working Need Input Input needed to work on this issue

Comments

@mihairaulea
Copy link

mihairaulea commented Dec 6, 2018

Using a macOS Mojave. Docker is up to date.

➜ ~ docker version
Client: Docker Engine - Community
Version: 18.09.0
API version: 1.39
Go version: go1.10.4
Git commit: 4d60db4
Built: Wed Nov 7 00:47:43 2018
OS/Arch: darwin/amd64
Experimental: false

Server: Docker Engine - Community
Engine:
Version: 18.09.0
API version: 1.39 (minimum version 1.12)
Go version: go1.10.4
Git commit: 4d60db4
Built: Wed Nov 7 00:55:00 2018
OS/Arch: linux/amd64
Experimental: true

I have cloned the securify git repository, and ran docker build . -t securify successfully. I have checked that the Docker image was built, and is available.

When running docker run securify as per the project documentation, i get

Error running securify.

Running with a mounted volume yields the same output. I am confident the volume had only one contract in it, which was successfully analyzed with other engines.

Error running securify.

@mihairaulea mihairaulea changed the title docker iage outputs "Error running securify." docker image outputs "Error running securify." Dec 6, 2018
@mihairaulea mihairaulea changed the title docker image outputs "Error running securify." Running docker image outputs "Error running securify." Dec 6, 2018
@hiqua
Copy link
Contributor

hiqua commented Dec 6, 2018

Hi @mihairaulea , thanks for the report!

Unfortunately I cannot reproduce this with the latest commit on the master branch, are you using the commit b54522e as I am?

@hiqua hiqua added the Bug Something isn't working label Dec 6, 2018
@mihairaulea
Copy link
Author

Hi @hiqua , yes, i am. Cloned the repo yesterday.

While building the image yesterday, had some issues(downloading soufle and other binaries), had to issue the command 3 times before a successful run.
I have removed the image, and rebuilt it right now, with no luck.

@mihairaulea
Copy link
Author

Okay, run with verbose.

➜  examples docker run -v $(pwd):/tmp securify -p=/tmp -v
Compiling project
Running Securify
Error running securify.
Exception in thread "main" java.lang.OutOfMemoryError: Java heap space
	at java.util.HashMap.resize(HashMap.java:704)
	at java.util.HashMap.putVal(HashMap.java:629)
	at java.util.HashMap.put(HashMap.java:612)
	at java.util.HashSet.add(HashSet.java:220)
	at ch.securify.analysis.AbstractDataflow.readFixedpoint(AbstractDataflow.java:217)
	at ch.securify.analysis.AbstractDataflow.runQuery(AbstractDataflow.java:226)
	at ch.securify.analysis.MayImplicitDataflow.varMayDepOn(MayImplicitDataflow.java:49)
	at ch.securify.analysis.Dataflow.varMayDepOn(Dataflow.java:57)
	at ch.securify.patterns.MissingInputValidation.isCompliant(MissingInputValidation.java:96)
	at ch.securify.patterns.AbstractInstructionPattern.checkPattern(AbstractInstructionPattern.java:35)
	at ch.securify.Main.checkInstructions(Main.java:419)
	at ch.securify.Main.checkPatterns(Main.java:384)
	at ch.securify.Main.processHexFile(Main.java:178)
	at ch.securify.Main.processCompilationOutput(Main.java:120)
	at ch.securify.Main.mainFromCompilationOutput(Main.java:99)
	at ch.securify.Main.main(Main.java:229)

@hiqua
Copy link
Contributor

hiqua commented Dec 6, 2018

How much memory do you have on your computer? OutOfMemoryError would indicate that you don't have enough.

@hiqua
Copy link
Contributor

hiqua commented Dec 6, 2018

Also, docker build . does not require Soufflé.

@mihairaulea
Copy link
Author

mihairaulea commented Dec 6, 2018

It seems the docker build requires Souffle. This is from the Dockerfile.

RUN mkdir /souffle
RUN wget -P /souffle/ https://github.com/souffle-lang/souffle/releases/download/1.4.0/souffle_1.4.0-1_amd64.deb &&\
        gdebi --n /souffle/souffle_1.4.0-1_amd64.deb

I have 16GB, should be enough :) Also, ran with docker run --memory=2g securify

@hiqua
Copy link
Contributor

hiqua commented Dec 6, 2018

Yes, I meant that it is included in the Dockerfile so you shouldn't have to do anything in particular.

Did you also try without --memory=2g?

@mihairaulea
Copy link
Author

Yes, tried without, as well.

@hiqua
Copy link
Contributor

hiqua commented Dec 6, 2018

What is the RAM consumption at its peak?

@hiqua
Copy link
Contributor

hiqua commented Dec 7, 2018

Maybe you can tell me more about the issues you had while building? Was it a network problem? Everything is downloaded from github, which is obviously not 100% resilient but you would have been quite unlucky to encounter issues right at that moment. What is the full docker build output?

@hiqua hiqua added the Need Input Input needed to work on this issue label Dec 7, 2018
@mihairaulea
Copy link
Author

Yep, network problem when building the image, but it never happened again. Here is the output of running the docker image, with -v.

Processing contract: /project/example.sol:MarketPlace
  Attempt to decompile the contract with methods...
  Success. Inlining methods...
[MINL] found 3 methods
[MINL] processing method: method_abi_BC5A6C20
[MINL] processing method: method_abi_3155194C
[MINL] processing method: method_abi_C7961F2A
  Propagating constants...

Decompiled contract:
00:  	a{Push}{0x80} = 0x80
02:  	b{Push}{0x40} = 0x40
04:  	mstore(memoffset: b{Push}{0x40}, value: a{Push}{0x80})
05:  	c{Push}{0x04} = 0x04
07:  	d{CallDataSize}{?} = calldatasize()
08:  	e{CallDataSize|Push}{?} = (d{CallDataSize}{?} < c{Push}{0x04})
0C:  	if e{CallDataSize|Push}{?}: goto tag_1 [merge @57]
0D:  	h{Push}{0x00} = 0x00
0F:  	i{Push|CallDataLoad}{?} = calldataload(h{Push}{0x00})
10:  	j{Push}{0x0100000000000000000000000000000000000000000000000000000000} = 0x0100000000000000000000000000000000000000000000000000000000
2F:  	k{Div|Push|CallDataLoad}{?} = i{Push|CallDataLoad}{?} / j{Push}{0x0100000000000000000000000000000000000000000000000000000000}
30:  	l{Push}{0xFFFFFFFF} = 0xFFFFFFFF
35:  	m{Div|Push|CallDataLoad}{?} = l{Push}{0xFFFFFFFF} & k{Div|Push|CallDataLoad}{?}
37:  	n{Push}{0x3155194C} = 0x3155194C
3C:  	o{Div|Push|CallDataLoad}{?} = (n{Push}{0x3155194C} == m{Div|Push|CallDataLoad}{?})
40:  	if o{Div|Push|CallDataLoad}{?}: goto tag_2 [merge @5C]
42:  	bl{Push}{0xBC5A6C20} = 0xBC5A6C20
47:  	bm{Div|Push|CallDataLoad}{?} = (bl{Push}{0xBC5A6C20} == m{Div|Push|CallDataLoad}{?})
4B:  	if bm{Div|Push|CallDataLoad}{?}: goto tag_5
4D:  	cm{Push}{0xC7961F2A} = 0xC7961F2A
52:  	cn{Div|Push|CallDataLoad}{?} = (cm{Push}{0xC7961F2A} == m{Div|Push|CallDataLoad}{?})
56:  	if cn{Div|Push|CallDataLoad}{?}: goto tag_8
57:  	tag_1: [from @0C]
58:  	g{Push}{0x00} = 0x00
5B:  	revert(memoffset: g{Push}{0x00}, length: g{Push}{0x00})
5C:  	tag_2: [from @40]
5D:  	q{CallValue}{?} = callvalue()
5F:  	r{CallValue}{?} = !q{CallValue}{?}
63:  	if r{CallValue}{?}: goto tag_3 [merge @68]
64:  	bk{Push}{0x00} = 0x00
67:  	revert(memoffset: bk{Push}{0x00}, length: bk{Push}{0x00})
68:  	tag_3: [from @63]
70:  	() = method_abi_3155194C()
72:  	stop()
73:  	tag_5: [from @4B]
74:  	bo{CallValue}{?} = callvalue()
76:  	bp{CallValue}{?} = !bo{CallValue}{?}
7A:  	if bp{CallValue}{?}: goto tag_6 [merge @7F]
7B:  	cl{Push}{0x00} = 0x00
7E:  	revert(memoffset: cl{Push}{0x00}, length: cl{Push}{0x00})
7F:  	tag_6: [from @7A]
87:  	() = method_abi_BC5A6C20()
89:  	stop()
8A:  	tag_8: [from @56]
8B:  	cp{CallValue}{?} = callvalue()
8D:  	cq{CallValue}{?} = !cp{CallValue}{?}
91:  	if cq{CallValue}{?}: goto tag_9 [merge @96]
92:  	dl{Push}{0x00} = 0x00
95:  	revert(memoffset: dl{Push}{0x00}, length: dl{Push}{0x00})
96:  	tag_9: [from @91]
9E:  	() = method_abi_C7961F2A()
A0:  	stop()

DF:  	method_abi_BC5A6C20()
E2:  	bu{Address}{?} = address()
E3:  	bv{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
F8:  	bw{Address|Push}{?} = bv{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & bu{Address}{?}
F9:  	bx{Address|Balance|Push}{?} = balance(address: bw{Address|Push}{?})
FC:  	by{Caller|_AddressType}{?} = caller()
FD:  	bz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
112:  	ca{Caller|_AddressType|Push}{?} = bz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & by{Caller|_AddressType}{?}
113:  	cb{Push}{0x08FC} = 0x08FC
119:  	cc{Address|Balance|Push}{?} = !bx{Address|Balance|Push}{?}
11A:  	cd{Address|Balance|Push}{?} = cc{Address|Balance|Push}{?} * cb{Push}{0x08FC}
11C:  	ce{Push}{0x40} = 0x40
11E:  	cf{Push}{0x80} = mload(memoffset: ce{Push}{0x40})
11F:  	cg{Push}{0x00} = 0x00
121:  	ch{Push}{0x40} = 0x40
123:  	ci{Push}{0x80} = mload(memoffset: ch{Push}{0x40})
126:  	cj{Push}{0x00} = cf{Push}{0x80} - ci{Push}{0x80}
12B:  	ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
133:  	return ()

A1:  	method_abi_3155194C()
A4:  	w{CallValue}{?} = callvalue()
A7:  	x{Caller|_AddressType}{?} = caller()
A8:  	y{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
BD:  	z{Caller|_AddressType|Push}{?} = y{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & x{Caller|_AddressType}{?}
BE:  	ba{Push}{0x08FC} = 0x08FC
C4:  	bb{CallValue}{?} = !w{CallValue}{?}
C5:  	bc{CallValue|Push}{?} = bb{CallValue}{?} * ba{Push}{0x08FC}
C7:  	bd{Push}{0x40} = 0x40
C9:  	be{Push}{0x80} = mload(memoffset: bd{Push}{0x40})
CA:  	bf{Push}{0x00} = 0x00
CC:  	bg{Push}{0x40} = 0x40
CE:  	bh{Push}{0x80} = mload(memoffset: bg{Push}{0x40})
D1:  	bi{Push}{0x00} = be{Push}{0x80} - bh{Push}{0x80}
D6:  	bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
DE:  	return ()

134:  	method_abi_C7961F2A()
138:  	cv{Push}{0x64} = 0x64
13C:  	cw{Push}{0x64} = 0x64
13F:  	cx{Push}{0x2710} = cv{Push}{0x64} * cw{Push}{0x64}
142:  	cy{Caller|_AddressType}{?} = caller()
143:  	cz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
158:  	da{Caller|_AddressType|Push}{?} = cz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & cy{Caller|_AddressType}{?}
159:  	db{Push}{0x08FC} = 0x08FC
15F:  	dc{Push}{0x00} = !cx{Push}{0x2710}
160:  	dd{Push}{0x00} = dc{Push}{0x00} * db{Push}{0x08FC}
162:  	de{Push}{0x40} = 0x40
164:  	df{Push}{0x80} = mload(memoffset: de{Push}{0x40})
165:  	dg{Push}{0x00} = 0x00
167:  	dh{Push}{0x40} = 0x40
169:  	di{Push}{0x80} = mload(memoffset: dh{Push}{0x40})
16C:  	dj{Push}{0x00} = df{Push}{0x80} - di{Push}{0x80}
171:  	dk{Caller|Call|_AddressType|Push}{?} = call(gas: dd{Push}{0x00}, to_addr: da{Caller|_AddressType|Push}{?}, value: cx{Push}{0x2710}, in_offset: di{Push}{0x80}, in_size: dj{Push}{0x00}, out_offset: di{Push}{0x80}, out_size: dg{Push}{0x00})
17A:  	return ()
  Verifying patterns...
Analyzing method with 19 instructions:

DF:  	method_abi_BC5A6C20()
E2:  	bu{Address}{?} = address()
E3:  	bv{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
F8:  	bw{Address|Push}{?} = bv{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & bu{Address}{?}
F9:  	bx{Address|Balance|Push}{?} = balance(address: bw{Address|Push}{?})
FC:  	by{Caller|_AddressType}{?} = caller()
FD:  	bz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
112:  	ca{Caller|_AddressType|Push}{?} = bz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & by{Caller|_AddressType}{?}
113:  	cb{Push}{0x08FC} = 0x08FC
119:  	cc{Address|Balance|Push}{?} = !bx{Address|Balance|Push}{?}
11A:  	cd{Address|Balance|Push}{?} = cc{Address|Balance|Push}{?} * cb{Push}{0x08FC}
11C:  	ce{Push}{0x40} = 0x40
11E:  	cf{Push}{0x80} = mload(memoffset: ce{Push}{0x40})
11F:  	cg{Push}{0x00} = 0x00
121:  	ch{Push}{0x40} = 0x40
123:  	ci{Push}{0x80} = mload(memoffset: ch{Push}{0x40})
126:  	cj{Push}{0x00} = cf{Push}{0x80} - ci{Push}{0x80}
12B:  	ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
133:  	return ()
Computing dataflow fixpoint over the method body...

Checking pattern DAO: 
	Violations:
	Warnings: 
	Safe: 
	Conflicts: 


Checking pattern DAOConstantGas: 
	Violations:
	Warnings: 
	Safe: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
	Conflicts: 


Checking pattern MissingInputValidation: 
	Violations:
	Warnings: 
	Safe: method_abi_BC5A6C20()
	Conflicts: 


Checking pattern TODAmount: 
	Violations:ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
	Warnings: 
	Safe: 
	Conflicts: 


Checking pattern TODReceiver: 
	Violations:
	Warnings: 
	Safe: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
	Conflicts: 


Checking pattern UnhandledException: 
	Violations:ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
	Warnings: 
	Safe: 
	Conflicts: 


Checking pattern UnrestrictedEtherFlow: 
	Violations:
	Warnings: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
	Safe: 
	Conflicts: 


Checking pattern UnrestrictedWrite: 
	Violations:
	Warnings: 
	Safe: 
	Conflicts: 

Analyzing method with 16 instructions:

A1:  	method_abi_3155194C()
A4:  	w{CallValue}{?} = callvalue()
A7:  	x{Caller|_AddressType}{?} = caller()
A8:  	y{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
BD:  	z{Caller|_AddressType|Push}{?} = y{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & x{Caller|_AddressType}{?}
BE:  	ba{Push}{0x08FC} = 0x08FC
C4:  	bb{CallValue}{?} = !w{CallValue}{?}
C5:  	bc{CallValue|Push}{?} = bb{CallValue}{?} * ba{Push}{0x08FC}
C7:  	bd{Push}{0x40} = 0x40
C9:  	be{Push}{0x80} = mload(memoffset: bd{Push}{0x40})
CA:  	bf{Push}{0x00} = 0x00
CC:  	bg{Push}{0x40} = 0x40
CE:  	bh{Push}{0x80} = mload(memoffset: bg{Push}{0x40})
D1:  	bi{Push}{0x00} = be{Push}{0x80} - bh{Push}{0x80}
D6:  	bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
DE:  	return ()
Computing dataflow fixpoint over the method body...

Checking pattern DAO: 
	Violations:
	Warnings: 
	Safe: 
	Conflicts: 


Checking pattern DAOConstantGas: 
	Violations:
	Warnings: 
	Safe: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
		bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
	Conflicts: 


Checking pattern MissingInputValidation: 
	Violations:
	Warnings: 
	Safe: method_abi_BC5A6C20()
		method_abi_3155194C()
	Conflicts: 


Checking pattern TODAmount: 
	Violations:ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
	Warnings: bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
	Safe: 
	Conflicts: 


Checking pattern TODReceiver: 
	Violations:
	Warnings: 
	Safe: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
		bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
	Conflicts: 


Checking pattern UnhandledException: 
	Violations:ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
		bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
	Warnings: 
	Safe: 
	Conflicts: 


Checking pattern UnrestrictedEtherFlow: 
	Violations:
	Warnings: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
		bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
	Safe: 
	Conflicts: 


Checking pattern UnrestrictedWrite: 
	Violations:
	Warnings: 
	Safe: 
	Conflicts: 

Analyzing method with 18 instructions:

134:  	method_abi_C7961F2A()
138:  	cv{Push}{0x64} = 0x64
13C:  	cw{Push}{0x64} = 0x64
13F:  	cx{Push}{0x2710} = cv{Push}{0x64} * cw{Push}{0x64}
142:  	cy{Caller|_AddressType}{?} = caller()
143:  	cz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
158:  	da{Caller|_AddressType|Push}{?} = cz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & cy{Caller|_AddressType}{?}
159:  	db{Push}{0x08FC} = 0x08FC
15F:  	dc{Push}{0x00} = !cx{Push}{0x2710}
160:  	dd{Push}{0x00} = dc{Push}{0x00} * db{Push}{0x08FC}
162:  	de{Push}{0x40} = 0x40
164:  	df{Push}{0x80} = mload(memoffset: de{Push}{0x40})
165:  	dg{Push}{0x00} = 0x00
167:  	dh{Push}{0x40} = 0x40
169:  	di{Push}{0x80} = mload(memoffset: dh{Push}{0x40})
16C:  	dj{Push}{0x00} = df{Push}{0x80} - di{Push}{0x80}
171:  	dk{Caller|Call|_AddressType|Push}{?} = call(gas: dd{Push}{0x00}, to_addr: da{Caller|_AddressType|Push}{?}, value: cx{Push}{0x2710}, in_offset: di{Push}{0x80}, in_size: dj{Push}{0x00}, out_offset: di{Push}{0x80}, out_size: dg{Push}{0x00})
17A:  	return ()
Computing dataflow fixpoint over the method body...

Checking pattern DAO: 
	Violations:
	Warnings: 
	Safe: 
	Conflicts: 


Checking pattern DAOConstantGas: 
	Violations:
	Warnings: 
	Safe: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
		bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
		dk{Caller|Call|_AddressType|Push}{?} = call(gas: dd{Push}{0x00}, to_addr: da{Caller|_AddressType|Push}{?}, value: cx{Push}{0x2710}, in_offset: di{Push}{0x80}, in_size: dj{Push}{0x00}, out_offset: di{Push}{0x80}, out_size: dg{Push}{0x00})
	Conflicts: 


Checking pattern MissingInputValidation: 
	Violations:
	Warnings: 
	Safe: method_abi_BC5A6C20()
		method_abi_3155194C()
		method_abi_C7961F2A()
	Conflicts: 


Checking pattern TODAmount: 
	Violations:ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
	Warnings: bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
	Safe: dk{Caller|Call|_AddressType|Push}{?} = call(gas: dd{Push}{0x00}, to_addr: da{Caller|_AddressType|Push}{?}, value: cx{Push}{0x2710}, in_offset: di{Push}{0x80}, in_size: dj{Push}{0x00}, out_offset: di{Push}{0x80}, out_size: dg{Push}{0x00})
	Conflicts: 


Checking pattern TODReceiver: 
	Violations:
	Warnings: 
	Safe: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
		bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
		dk{Caller|Call|_AddressType|Push}{?} = call(gas: dd{Push}{0x00}, to_addr: da{Caller|_AddressType|Push}{?}, value: cx{Push}{0x2710}, in_offset: di{Push}{0x80}, in_size: dj{Push}{0x00}, out_offset: di{Push}{0x80}, out_size: dg{Push}{0x00})
	Conflicts: 


Checking pattern UnhandledException: 
	Violations:ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
		bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
		dk{Caller|Call|_AddressType|Push}{?} = call(gas: dd{Push}{0x00}, to_addr: da{Caller|_AddressType|Push}{?}, value: cx{Push}{0x2710}, in_offset: di{Push}{0x80}, in_size: dj{Push}{0x00}, out_offset: di{Push}{0x80}, out_size: dg{Push}{0x00})
	Warnings: 
	Safe: 
	Conflicts: 


Checking pattern UnrestrictedEtherFlow: 
	Violations:dk{Caller|Call|_AddressType|Push}{?} = call(gas: dd{Push}{0x00}, to_addr: da{Caller|_AddressType|Push}{?}, value: cx{Push}{0x2710}, in_offset: di{Push}{0x80}, in_size: dj{Push}{0x00}, out_offset: di{Push}{0x80}, out_size: dg{Push}{0x00})
	Warnings: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
		bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
	Safe: 
	Conflicts: 


Checking pattern UnrestrictedWrite: 
	Violations:
	Warnings: 
	Safe: 
	Conflicts: 

Computing global dataflow fixpoint over the entire contract...

Checking pattern LockedEther: 
Exception in thread "main" java.lang.OutOfMemoryError: Java heap space
	at java.util.HashMap.resize(HashMap.java:704)
	at java.util.HashMap.putVal(HashMap.java:629)
	at java.util.HashMap.put(HashMap.java:612)
	at java.util.HashSet.add(HashSet.java:220)
	at ch.securify.analysis.AbstractDataflow.readFixedpoint(AbstractDataflow.java:217)
	at ch.securify.analysis.AbstractDataflow.runQuery(AbstractDataflow.java:226)
	at ch.securify.analysis.MustExplicitDataflow.varMustDepOn(MustExplicitDataflow.java:54)
	at ch.securify.analysis.Dataflow.varMustDepOn(Dataflow.java:97)
	at ch.securify.patterns.LockedEther.isSafe(LockedEther.java:45)
	at ch.securify.patterns.AbstractContractPattern.checkPattern(AbstractContractPattern.java:34)
	at ch.securify.Main.checkInstructions(Main.java:423)
	at ch.securify.Main.checkPatterns(Main.java:404)
	at ch.securify.Main.processHexFile(Main.java:174)
	at ch.securify.Main.processCompilationOutput(Main.java:121)
	at ch.securify.Main.mainFromCompilationOutput(Main.java:101)
	at ch.securify.Main.main(Main.java:233)
Error running Securify

@mihairaulea
Copy link
Author

I bet you have a memory leak, investigating.

@mihairaulea
Copy link
Author

mihairaulea commented Dec 10, 2018

Modified project.py, allocated 4GB of heap memory(hardcoded).

Line 79 in project.py

cmd = ["java", f"-Xmx4G", "-jar", str(self.securify_jar),

Here is the output now:

Processing contract: /project/example.sol:MarketPlace
  Attempt to decompile the contract with methods...
  Success. Inlining methods...
[MINL] found 3 methods
[MINL] processing method: method_abi_BC5A6C20
[MINL] processing method: method_abi_3155194C
[MINL] processing method: method_abi_C7961F2A
  Propagating constants...

Decompiled contract:
00:  	a{Push}{0x80} = 0x80
02:  	b{Push}{0x40} = 0x40
04:  	mstore(memoffset: b{Push}{0x40}, value: a{Push}{0x80})
05:  	c{Push}{0x04} = 0x04
07:  	d{CallDataSize}{?} = calldatasize()
08:  	e{CallDataSize|Push}{?} = (d{CallDataSize}{?} < c{Push}{0x04})
0C:  	if e{CallDataSize|Push}{?}: goto tag_1 [merge @57]
0D:  	h{Push}{0x00} = 0x00
0F:  	i{Push|CallDataLoad}{?} = calldataload(h{Push}{0x00})
10:  	j{Push}{0x0100000000000000000000000000000000000000000000000000000000} = 0x0100000000000000000000000000000000000000000000000000000000
2F:  	k{Div|Push|CallDataLoad}{?} = i{Push|CallDataLoad}{?} / j{Push}{0x0100000000000000000000000000000000000000000000000000000000}
30:  	l{Push}{0xFFFFFFFF} = 0xFFFFFFFF
35:  	m{Div|Push|CallDataLoad}{?} = l{Push}{0xFFFFFFFF} & k{Div|Push|CallDataLoad}{?}
37:  	n{Push}{0x3155194C} = 0x3155194C
3C:  	o{Div|Push|CallDataLoad}{?} = (n{Push}{0x3155194C} == m{Div|Push|CallDataLoad}{?})
40:  	if o{Div|Push|CallDataLoad}{?}: goto tag_2 [merge @5C]
42:  	bl{Push}{0xBC5A6C20} = 0xBC5A6C20
47:  	bm{Div|Push|CallDataLoad}{?} = (bl{Push}{0xBC5A6C20} == m{Div|Push|CallDataLoad}{?})
4B:  	if bm{Div|Push|CallDataLoad}{?}: goto tag_5
4D:  	cm{Push}{0xC7961F2A} = 0xC7961F2A
52:  	cn{Div|Push|CallDataLoad}{?} = (cm{Push}{0xC7961F2A} == m{Div|Push|CallDataLoad}{?})
56:  	if cn{Div|Push|CallDataLoad}{?}: goto tag_8
57:  	tag_1: [from @0C]
58:  	g{Push}{0x00} = 0x00
5B:  	revert(memoffset: g{Push}{0x00}, length: g{Push}{0x00})
5C:  	tag_2: [from @40]
5D:  	q{CallValue}{?} = callvalue()
5F:  	r{CallValue}{?} = !q{CallValue}{?}
63:  	if r{CallValue}{?}: goto tag_3 [merge @68]
64:  	bk{Push}{0x00} = 0x00
67:  	revert(memoffset: bk{Push}{0x00}, length: bk{Push}{0x00})
68:  	tag_3: [from @63]
70:  	() = method_abi_3155194C()
72:  	stop()
73:  	tag_5: [from @4B]
74:  	bo{CallValue}{?} = callvalue()
76:  	bp{CallValue}{?} = !bo{CallValue}{?}
7A:  	if bp{CallValue}{?}: goto tag_6 [merge @7F]
7B:  	cl{Push}{0x00} = 0x00
7E:  	revert(memoffset: cl{Push}{0x00}, length: cl{Push}{0x00})
7F:  	tag_6: [from @7A]
87:  	() = method_abi_BC5A6C20()
89:  	stop()
8A:  	tag_8: [from @56]
8B:  	cp{CallValue}{?} = callvalue()
8D:  	cq{CallValue}{?} = !cp{CallValue}{?}
91:  	if cq{CallValue}{?}: goto tag_9 [merge @96]
92:  	dl{Push}{0x00} = 0x00
95:  	revert(memoffset: dl{Push}{0x00}, length: dl{Push}{0x00})
96:  	tag_9: [from @91]
9E:  	() = method_abi_C7961F2A()
A0:  	stop()

DF:  	method_abi_BC5A6C20()
E2:  	bu{Address}{?} = address()
E3:  	bv{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
F8:  	bw{Address|Push}{?} = bv{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & bu{Address}{?}
F9:  	bx{Address|Balance|Push}{?} = balance(address: bw{Address|Push}{?})
FC:  	by{Caller|_AddressType}{?} = caller()
FD:  	bz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
112:  	ca{Caller|_AddressType|Push}{?} = bz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & by{Caller|_AddressType}{?}
113:  	cb{Push}{0x08FC} = 0x08FC
119:  	cc{Address|Balance|Push}{?} = !bx{Address|Balance|Push}{?}
11A:  	cd{Address|Balance|Push}{?} = cc{Address|Balance|Push}{?} * cb{Push}{0x08FC}
11C:  	ce{Push}{0x40} = 0x40
11E:  	cf{Push}{0x80} = mload(memoffset: ce{Push}{0x40})
11F:  	cg{Push}{0x00} = 0x00
121:  	ch{Push}{0x40} = 0x40
123:  	ci{Push}{0x80} = mload(memoffset: ch{Push}{0x40})
126:  	cj{Push}{0x00} = cf{Push}{0x80} - ci{Push}{0x80}
12B:  	ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
133:  	return ()

A1:  	method_abi_3155194C()
A4:  	w{CallValue}{?} = callvalue()
A7:  	x{Caller|_AddressType}{?} = caller()
A8:  	y{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
BD:  	z{Caller|_AddressType|Push}{?} = y{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & x{Caller|_AddressType}{?}
BE:  	ba{Push}{0x08FC} = 0x08FC
C4:  	bb{CallValue}{?} = !w{CallValue}{?}
C5:  	bc{CallValue|Push}{?} = bb{CallValue}{?} * ba{Push}{0x08FC}
C7:  	bd{Push}{0x40} = 0x40
C9:  	be{Push}{0x80} = mload(memoffset: bd{Push}{0x40})
CA:  	bf{Push}{0x00} = 0x00
CC:  	bg{Push}{0x40} = 0x40
CE:  	bh{Push}{0x80} = mload(memoffset: bg{Push}{0x40})
D1:  	bi{Push}{0x00} = be{Push}{0x80} - bh{Push}{0x80}
D6:  	bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
DE:  	return ()

134:  	method_abi_C7961F2A()
138:  	cv{Push}{0x64} = 0x64
13C:  	cw{Push}{0x64} = 0x64
13F:  	cx{Push}{0x2710} = cv{Push}{0x64} * cw{Push}{0x64}
142:  	cy{Caller|_AddressType}{?} = caller()
143:  	cz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
158:  	da{Caller|_AddressType|Push}{?} = cz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & cy{Caller|_AddressType}{?}
159:  	db{Push}{0x08FC} = 0x08FC
15F:  	dc{Push}{0x00} = !cx{Push}{0x2710}
160:  	dd{Push}{0x00} = dc{Push}{0x00} * db{Push}{0x08FC}
162:  	de{Push}{0x40} = 0x40
164:  	df{Push}{0x80} = mload(memoffset: de{Push}{0x40})
165:  	dg{Push}{0x00} = 0x00
167:  	dh{Push}{0x40} = 0x40
169:  	di{Push}{0x80} = mload(memoffset: dh{Push}{0x40})
16C:  	dj{Push}{0x00} = df{Push}{0x80} - di{Push}{0x80}
171:  	dk{Caller|Call|_AddressType|Push}{?} = call(gas: dd{Push}{0x00}, to_addr: da{Caller|_AddressType|Push}{?}, value: cx{Push}{0x2710}, in_offset: di{Push}{0x80}, in_size: dj{Push}{0x00}, out_offset: di{Push}{0x80}, out_size: dg{Push}{0x00})
17A:  	return ()
  Verifying patterns...
Analyzing method with 19 instructions:

DF:  	method_abi_BC5A6C20()
E2:  	bu{Address}{?} = address()
E3:  	bv{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
F8:  	bw{Address|Push}{?} = bv{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & bu{Address}{?}
F9:  	bx{Address|Balance|Push}{?} = balance(address: bw{Address|Push}{?})
FC:  	by{Caller|_AddressType}{?} = caller()
FD:  	bz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
112:  	ca{Caller|_AddressType|Push}{?} = bz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & by{Caller|_AddressType}{?}
113:  	cb{Push}{0x08FC} = 0x08FC
119:  	cc{Address|Balance|Push}{?} = !bx{Address|Balance|Push}{?}
11A:  	cd{Address|Balance|Push}{?} = cc{Address|Balance|Push}{?} * cb{Push}{0x08FC}
11C:  	ce{Push}{0x40} = 0x40
11E:  	cf{Push}{0x80} = mload(memoffset: ce{Push}{0x40})
11F:  	cg{Push}{0x00} = 0x00
121:  	ch{Push}{0x40} = 0x40
123:  	ci{Push}{0x80} = mload(memoffset: ch{Push}{0x40})
126:  	cj{Push}{0x00} = cf{Push}{0x80} - ci{Push}{0x80}
12B:  	ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
133:  	return ()
Computing dataflow fixpoint over the method body...

Checking pattern DAO: 
	Violations:
	Warnings: 
	Safe: 
	Conflicts: 


Checking pattern DAOConstantGas: 
	Violations:
	Warnings: 
	Safe: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
	Conflicts: 


Checking pattern MissingInputValidation: 
	Violations:
	Warnings: 
	Safe: method_abi_BC5A6C20()
	Conflicts: 


Checking pattern TODAmount: 
	Violations:ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
	Warnings: 
	Safe: 
	Conflicts: 


Checking pattern TODReceiver: 
	Violations:
	Warnings: 
	Safe: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
	Conflicts: 


Checking pattern UnhandledException: 
	Violations:ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
	Warnings: 
	Safe: 
	Conflicts: 


Checking pattern UnrestrictedEtherFlow: 
	Violations:
	Warnings: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
	Safe: 
	Conflicts: 


Checking pattern UnrestrictedWrite: 
	Violations:
	Warnings: 
	Safe: 
	Conflicts: 

Analyzing method with 16 instructions:

A1:  	method_abi_3155194C()
A4:  	w{CallValue}{?} = callvalue()
A7:  	x{Caller|_AddressType}{?} = caller()
A8:  	y{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
BD:  	z{Caller|_AddressType|Push}{?} = y{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & x{Caller|_AddressType}{?}
BE:  	ba{Push}{0x08FC} = 0x08FC
C4:  	bb{CallValue}{?} = !w{CallValue}{?}
C5:  	bc{CallValue|Push}{?} = bb{CallValue}{?} * ba{Push}{0x08FC}
C7:  	bd{Push}{0x40} = 0x40
C9:  	be{Push}{0x80} = mload(memoffset: bd{Push}{0x40})
CA:  	bf{Push}{0x00} = 0x00
CC:  	bg{Push}{0x40} = 0x40
CE:  	bh{Push}{0x80} = mload(memoffset: bg{Push}{0x40})
D1:  	bi{Push}{0x00} = be{Push}{0x80} - bh{Push}{0x80}
D6:  	bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
DE:  	return ()
Computing dataflow fixpoint over the method body...

Checking pattern DAO: 
	Violations:
	Warnings: 
	Safe: 
	Conflicts: 


Checking pattern DAOConstantGas: 
	Violations:
	Warnings: 
	Safe: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
		bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
	Conflicts: 


Checking pattern MissingInputValidation: 
	Violations:
	Warnings: 
	Safe: method_abi_BC5A6C20()
		method_abi_3155194C()
	Conflicts: 


Checking pattern TODAmount: 
	Violations:ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
	Warnings: bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
	Safe: 
	Conflicts: 


Checking pattern TODReceiver: 
	Violations:
	Warnings: 
	Safe: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
		bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
	Conflicts: 


Checking pattern UnhandledException: 
	Violations:ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
		bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
	Warnings: 
	Safe: 
	Conflicts: 


Checking pattern UnrestrictedEtherFlow: 
	Violations:
	Warnings: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
		bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
	Safe: 
	Conflicts: 


Checking pattern UnrestrictedWrite: 
	Violations:
	Warnings: 
	Safe: 
	Conflicts: 

Analyzing method with 18 instructions:

134:  	method_abi_C7961F2A()
138:  	cv{Push}{0x64} = 0x64
13C:  	cw{Push}{0x64} = 0x64
13F:  	cx{Push}{0x2710} = cv{Push}{0x64} * cw{Push}{0x64}
142:  	cy{Caller|_AddressType}{?} = caller()
143:  	cz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
158:  	da{Caller|_AddressType|Push}{?} = cz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & cy{Caller|_AddressType}{?}
159:  	db{Push}{0x08FC} = 0x08FC
15F:  	dc{Push}{0x00} = !cx{Push}{0x2710}
160:  	dd{Push}{0x00} = dc{Push}{0x00} * db{Push}{0x08FC}
162:  	de{Push}{0x40} = 0x40
164:  	df{Push}{0x80} = mload(memoffset: de{Push}{0x40})
165:  	dg{Push}{0x00} = 0x00
167:  	dh{Push}{0x40} = 0x40
169:  	di{Push}{0x80} = mload(memoffset: dh{Push}{0x40})
16C:  	dj{Push}{0x00} = df{Push}{0x80} - di{Push}{0x80}
171:  	dk{Caller|Call|_AddressType|Push}{?} = call(gas: dd{Push}{0x00}, to_addr: da{Caller|_AddressType|Push}{?}, value: cx{Push}{0x2710}, in_offset: di{Push}{0x80}, in_size: dj{Push}{0x00}, out_offset: di{Push}{0x80}, out_size: dg{Push}{0x00})
17A:  	return ()
Computing dataflow fixpoint over the method body...

Checking pattern DAO: 
	Violations:
	Warnings: 
	Safe: 
	Conflicts: 


Checking pattern DAOConstantGas: 
	Violations:
	Warnings: 
	Safe: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
		bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
		dk{Caller|Call|_AddressType|Push}{?} = call(gas: dd{Push}{0x00}, to_addr: da{Caller|_AddressType|Push}{?}, value: cx{Push}{0x2710}, in_offset: di{Push}{0x80}, in_size: dj{Push}{0x00}, out_offset: di{Push}{0x80}, out_size: dg{Push}{0x00})
	Conflicts: 


Checking pattern MissingInputValidation: 
	Violations:
	Warnings: 
	Safe: method_abi_BC5A6C20()
		method_abi_3155194C()
		method_abi_C7961F2A()
	Conflicts: 


Checking pattern TODAmount: 
Error running Securify

@hiqua
Copy link
Contributor

hiqua commented Dec 10, 2018

It's very possible that there's a memory leak (actually I'd be surprised if there isn't any!), but I still don't understand why I cannot reproduce this. How big is your swap partition? I have 16GB of memory and my swap is 16GB.

@mihairaulea
Copy link
Author

Try with docker system prune -a . Re memory: exactly same config. Thanks for the time and patience so far.

@hiqua
Copy link
Contributor

hiqua commented Dec 10, 2018

I ran your command, but I still cannot reproduce your bug after building the image from scratch. It runs fine with 11GB available in memory, and an empty swap.

@charles-lei
Copy link

@mihairaulea I have met the same issue, do you have any new discoveries?

@0x3bfc
Copy link

0x3bfc commented Dec 21, 2018

I am experiencing the same issue:
Truffle version: v5.0.0
Solc version: 0.4.25
Docker version 18.09.0

ahmeds-mbp-2:securify ahmed$ docker run --memory=16g -v $(pwd):/project securify
Compiling project
Running Securify
Processing contract: /project/contracts/Migrations.sol:Migrations
  Attempt to decompile the contract with methods...
  Success. Inlining methods...
  Propagating constants...
  Verifying patterns...
Exception in thread "main" java.lang.OutOfMemoryError: Java heap space
	at java.util.HashMap.resize(HashMap.java:704)
	at java.util.HashMap.putVal(HashMap.java:629)
	at java.util.HashMap.put(HashMap.java:612)
	at java.util.HashSet.add(HashSet.java:220)
	at ch.securify.analysis.AbstractDataflow.readFixedpoint(AbstractDataflow.java:217)
	at ch.securify.analysis.AbstractDataflow.runQuery(AbstractDataflow.java:226)
	at ch.securify.analysis.MayImplicitDataflow.mayFollow(MayImplicitDataflow.java:44)
	at ch.securify.analysis.Dataflow.mayFollow(Dataflow.java:49)
	at ch.securify.patterns.MissingInputValidation.isViolation(MissingInputValidation.java:67)
	at ch.securify.patterns.AbstractInstructionPattern.checkPattern(AbstractInstructionPattern.java:38)
	at ch.securify.Main.checkInstructions(Main.java:443)
	at ch.securify.Main.checkPatterns(Main.java:408)
	at ch.securify.Main.processHexFile(Main.java:185)
	at ch.securify.Main.processCompilationOutput(Main.java:132)
	at ch.securify.Main.mainFromCompilationOutput(Main.java:108)
	at ch.securify.Main.main(Main.java:244)
Error running Securify

@hiqua
Copy link
Contributor

hiqua commented Dec 21, 2018

@aabdulwahed you're using macOS right? And @charles-lei as well?

I don't, so that could explain why I cannot reproduce it. I'm not sure what the root issue is for now though.

@charles-lei
Copy link

yes, I'm using macOS and docker toolbox
OS version: Mojave 10.14

@0x3bfc
Copy link

0x3bfc commented Dec 24, 2018

Thanks @hiqua for swift reply, yes I am using MacOS.. Does it work for Ubuntu 18.04 LTS ?

@hiqua
Copy link
Contributor

hiqua commented Jan 3, 2019

@aabdulwahed it works for me on Debian, I assume it will work on Ubuntu as well. It really seems to be related to macOS or at least to Docker on macOS.

@0x3bfc
Copy link

0x3bfc commented Jan 7, 2019

@hiqua thanks, I will move to Ubuntu

@mihairaulea
Copy link
Author

Seems to be related to MacOS, specifically Mojave. okay, will run in a vm.

@Ramarti
Copy link

Ramarti commented Jan 16, 2019

Same here.

Mac Os Mojave: 10.14
Docker Desktop Community Version 2.0.0.2 (30215)
Truffle version: 4.1.15 (changed in Dockerfile)

platform-contracts git:(earlyreturn) docker run --memory=16g -v $(pwd):/project securify --truffle
Compiling project
Running Securify
Processing contract: /project/contracts/user/EthicHubUser.sol:EthicHubUser
  Attempt to decompile the contract with methods...
  Failed to decompile methods. Attempt to decompile the contract without identifying methods...
  Propagating constants...
  Verifying patterns...
Exception in thread "main" java.lang.OutOfMemoryError: Java heap space
	at java.util.HashMap.resize(HashMap.java:704)
	at java.util.HashMap.putVal(HashMap.java:629)
	at java.util.HashMap.put(HashMap.java:612)
	at java.util.HashSet.add(HashSet.java:220)
	at ch.securify.analysis.AbstractDataflow.readFixedpoint(AbstractDataflow.java:217)
	at ch.securify.analysis.AbstractDataflow.runQuery(AbstractDataflow.java:226)
	at ch.securify.analysis.MustExplicitDataflow.mustPrecede(MustExplicitDataflow.java:44)
	at ch.securify.analysis.Dataflow.mustPrecede(Dataflow.java:89)
	at ch.securify.patterns.LockedEther.isSafe(LockedEther.java:54)
	at ch.securify.patterns.AbstractContractPattern.checkPattern(AbstractContractPattern.java:38)
	at ch.securify.Main.checkInstructions(Main.java:443)
	at ch.securify.Main.checkPatterns(Main.java:388)
	at ch.securify.Main.processHexFile(Main.java:185)
	at ch.securify.Main.processCompilationOutput(Main.java:132)
	at ch.securify.Main.mainFromCompilationOutput(Main.java:108)
	at ch.securify.Main.main(Main.java:244)
Error running Securify

@instabridge-thomas
Copy link

Ditto

Truffle: 5.0.1
Docker: Community 18.09.1
MacOSX: 10.14.2

ThomasTGWUTWAs-MacBook-Pro:smart-contracts thomasinstabridge$ docker run -v $(pwd) --memory=16g chainsecurity/securify
Compiling project
Running Securify
Processing contract: /project/example.sol:MarketPlace
  Attempt to decompile the contract with methods...
  Success. Inlining methods...
  Propagating constants...
  Verifying patterns...
Exception in thread "main" java.lang.OutOfMemoryError: Java heap space
	at java.util.HashMap.resize(HashMap.java:704)
	at java.util.HashMap.putVal(HashMap.java:629)
	at java.util.HashMap.put(HashMap.java:612)
	at java.util.HashSet.add(HashSet.java:220)
	at ch.securify.analysis.AbstractDataflow.readFixedpoint(AbstractDataflow.java:217)
	at ch.securify.analysis.AbstractDataflow.runQuery(AbstractDataflow.java:226)
	at ch.securify.analysis.MustExplicitDataflow.varMustDepOn(MustExplicitDataflow.java:54)
	at ch.securify.analysis.Dataflow.varMustDepOn(Dataflow.java:97)
	at ch.securify.patterns.TODAmount.isViolation(TODAmount.java:56)
	at ch.securify.patterns.AbstractInstructionPattern.checkPattern(AbstractInstructionPattern.java:38)
	at ch.securify.Main.checkInstructions(Main.java:443)
	at ch.securify.Main.checkPatterns(Main.java:408)
	at ch.securify.Main.processHexFile(Main.java:185)
	at ch.securify.Main.processCompilationOutput(Main.java:132)
	at ch.securify.Main.mainFromCompilationOutput(Main.java:108)
	at ch.securify.Main.main(Main.java:244)
Error running Securify

@hiqua
Copy link
Contributor

hiqua commented Jan 16, 2019

If those having problems with macOS can try with a VM on Ubuntu and see whether they have the same problems, that'd be great! So far I haven't seen anyone claiming that they could reproduce this issue on an OS different from macOS.

@hiqua hiqua changed the title Running docker image outputs "Error running securify." Running docker image outputs "Error running securify." on macOS Jan 17, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Bug Something isn't working Need Input Input needed to work on this issue
Projects
None yet
Development

No branches or pull requests

6 participants