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

Docker image to wrap z3 behind http #2963

Open
chriseth opened this Issue Sep 26, 2017 · 12 comments

Comments

Projects
None yet
3 participants
@chriseth
Contributor

chriseth commented Sep 26, 2017

For remix, it would be helpful to have a docker image that exposes z3 / smtlib via HTTP so that it can be used from within the browser.

The idea would be to run the image either locally or on a server and connect remix to it via ajax requests.

The image should have an open port with an http server behind it, which forwards the request payload to the standard input of a z3 instance run using something like z3 -smt2 -in and responds with the contents of standard output of the command.

Example smtlib2 inputs look like:

(declare-const a Int)
(declare-fun f (Int Bool) Int)
(assert (> a 10))
(assert (< (f a true) 100))
(check-sat)
(get-model)

The output of z3 on this would be:

sat
(model 
  (define-fun a () Int
    11)
  (define-fun f ((x!1 Int) (x!2 Bool)) Int
    (ite (and (= x!1 11) (= x!2 true)) 0
      0))
)

During a single compilation run, multiple of these requests would be sent to the z3 "server".

@chriseth chriseth changed the title from Docker image to wrap z3 behind REST to Docker image to wrap z3 behind http Sep 26, 2017

@axic

This comment has been minimized.

Show comment
Hide comment
@axic

axic Sep 26, 2017

Member

For privacy reasons I think the function names should be hashed. This would be the first instance Remix sending contract data out as part of the compilation process.

Member

axic commented Sep 26, 2017

For privacy reasons I think the function names should be hashed. This would be the first instance Remix sending contract data out as part of the compilation process.

@eelkevdbos

This comment has been minimized.

Show comment
Hide comment
@eelkevdbos

eelkevdbos Oct 9, 2017

I would like to pick this one up. Should I reference the created repo / docker image in this thread or create a pull request somewhere?

eelkevdbos commented Oct 9, 2017

I would like to pick this one up. Should I reference the created repo / docker image in this thread or create a pull request somewhere?

@chriseth

This comment has been minimized.

Show comment
Hide comment
@chriseth

chriseth Oct 9, 2017

Contributor

Thanks, @eelkevdbos ! You can put the dockerfile into the scripts directory (under a different name).

Contributor

chriseth commented Oct 9, 2017

Thanks, @eelkevdbos ! You can put the dockerfile into the scripts directory (under a different name).

eelkevdbos added a commit to eelkevdbos/solidity that referenced this issue Oct 9, 2017

@eelkevdbos

This comment has been minimized.

Show comment
Hide comment
@eelkevdbos

eelkevdbos Oct 9, 2017

@chriseth I could inline the docker file but providing a 'script' seems more suitable and keeps the development of the wrapper less bound to the solidity project. We could also opt for a 'wget' approach of the go binary inside a vanilla golang docker image.

eelkevdbos commented Oct 9, 2017

@chriseth I could inline the docker file but providing a 'script' seems more suitable and keeps the development of the wrapper less bound to the solidity project. We could also opt for a 'wget' approach of the go binary inside a vanilla golang docker image.

@chriseth

This comment has been minimized.

Show comment
Hide comment
@chriseth

chriseth Oct 9, 2017

Contributor

@eelkevdbos wonderful, that's exactly the functionality that we need :-)

Would it be possible to make the image a "little" smaller than 700 MB? Also I'm not a big fan of using files external to the Dockerfile, at least for such tiny things - I guess that's a philosophical question...

Contributor

chriseth commented Oct 9, 2017

@eelkevdbos wonderful, that's exactly the functionality that we need :-)

Would it be possible to make the image a "little" smaller than 700 MB? Also I'm not a big fan of using files external to the Dockerfile, at least for such tiny things - I guess that's a philosophical question...

@eelkevdbos

This comment has been minimized.

Show comment
Hide comment
@eelkevdbos

eelkevdbos Oct 9, 2017

I managed to compile z3 (4.5.0) for alpine linux. This creates a smaller image (200 MB), but the output differs:

alpine

sat
(model 
  (define-fun a () Int
    11)
  (define-fun f ((x!0 Int) (x!1 Bool)) Int
    (ite (and (= x!0 11) (= x!1 true)) 0
      0))
)

debian stretch

sat
(model 
  (define-fun a () Int
    11)
  (define-fun f ((x!1 Int) (x!2 Bool)) Int
    (ite (and (= x!1 11) (= x!2 true)) 0
      0))
)

I can't really judge if this is a deal-breaker (it seems the index of starts at 0 instead of 1). Can you perhaps shine some light on the differences?

eelkevdbos commented Oct 9, 2017

I managed to compile z3 (4.5.0) for alpine linux. This creates a smaller image (200 MB), but the output differs:

alpine

sat
(model 
  (define-fun a () Int
    11)
  (define-fun f ((x!0 Int) (x!1 Bool)) Int
    (ite (and (= x!0 11) (= x!1 true)) 0
      0))
)

debian stretch

sat
(model 
  (define-fun a () Int
    11)
  (define-fun f ((x!1 Int) (x!2 Bool)) Int
    (ite (and (= x!1 11) (= x!2 true)) 0
      0))
)

I can't really judge if this is a deal-breaker (it seems the index of starts at 0 instead of 1). Can you perhaps shine some light on the differences?

@chriseth

This comment has been minimized.

Show comment
Hide comment
@chriseth

chriseth Oct 10, 2017

Contributor

Ah, that's great! The difference in the output is weird but does not change the behaviour (the x!1 are just names of local variables).

Another thing that I forgot to mention: The http server should respond to CORS requests and approve all of them.

Contributor

chriseth commented Oct 10, 2017

Ah, that's great! The difference in the output is weird but does not change the behaviour (the x!1 are just names of local variables).

Another thing that I forgot to mention: The http server should respond to CORS requests and approve all of them.

@eelkevdbos

This comment has been minimized.

Show comment
Hide comment
@eelkevdbos

eelkevdbos Oct 10, 2017

Allright! I modified the request handler to approve all CORS requests. A simple docker pull evdb/z3-http would suffice to pull in the new image.

eelkevdbos commented Oct 10, 2017

Allright! I modified the request handler to approve all CORS requests. A simple docker pull evdb/z3-http would suffice to pull in the new image.

@axic axic added help wanted and removed help wanted labels Dec 2, 2017

@axic axic removed the up-for-grabs label Dec 18, 2017

@eelkevdbos

This comment has been minimized.

Show comment
Hide comment
@eelkevdbos

eelkevdbos Jan 15, 2018

Updated to python, should be fine now, sorry for the wait.

eelkevdbos commented Jan 15, 2018

Updated to python, should be fine now, sorry for the wait.

@eelkevdbos

This comment has been minimized.

Show comment
Hide comment
@eelkevdbos

eelkevdbos Jun 30, 2018

Hi @chriseth is there anything I can do to help resolve this issue? I've updated the pull request to reflect the feedback given #3056

eelkevdbos commented Jun 30, 2018

Hi @chriseth is there anything I can do to help resolve this issue? I've updated the pull request to reflect the feedback given #3056

@chriseth

This comment has been minimized.

Show comment
Hide comment
@chriseth

chriseth Jul 10, 2018

Contributor

I'm sorry, we are just not sure whether this is the way to go because it is still a little cumbersome. If we decide to do it like this, we will pick up your docker image again. Thanks for your help and sorry for the bad planning on our side.

Contributor

chriseth commented Jul 10, 2018

I'm sorry, we are just not sure whether this is the way to go because it is still a little cumbersome. If we decide to do it like this, we will pick up your docker image again. Thanks for your help and sorry for the bad planning on our side.

@eelkevdbos

This comment has been minimized.

Show comment
Hide comment
@eelkevdbos

eelkevdbos Jul 10, 2018

No problem, I will look for some other low hanging fruit issue if available.

eelkevdbos commented Jul 10, 2018

No problem, I will look for some other low hanging fruit issue if available.

@axic axic removed the hacktoberfest label Jul 28, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment