search

kenmcmil / ivy

IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Other
77 stars 24 forks source link

ivy_to_cpp: Add a newline after printing the model to the modelfile #33

Closed dijkstracula closed 1 month ago

dijkstracula commented 2 years ago

Currently, when ivy_to_cpp-generated code prints out the current model, it doesn't emit a trailing newline. This makes the output slightly tricky to read: consider the following example:

  99 (define-fun tcp.endpoint.port ((x!0 tcp.endpoint)) (_ BitVec 16)
 100   (ite (= x!0 tcp.endpoint!val!1) #xbfe5
 101   (ite (= x!0 tcp.endpoint!val!2) #xbfe6
 102     #xbfe4)))pred: (= |__prm:V0| 1)
 103 alit: |alit:0|
 104 pred: (= |__fml:val| #x4d)
 105 alit: |alit:1|
 106 begin check:
 107 (declare-fun max () Int)
…

Notice that the pred directive on line 102 is not actually part of the model but follows from a subsequent call to gen::add_alit(). With this patch, that output line now appears on its own line:

  99 (define-fun tcp.endpoint.port ((x!0 tcp.endpoint)) (_ BitVec 16)
 100   (ite (= x!0 tcp.endpoint!val!1) #xbfe5
 101   (ite (= x!0 tcp.endpoint!val!2) #xbfe6
 102     #xbfe4)))
 103 pred: (= |__prm:V0| 1)
 104 alit: |alit:0|
 105 pred: (= |__fml:val| #x4d)
 106 alit: |alit:1|
 107 begin check:
…

(As a result, this means that model files will also have a trailing newline at the end of the file, which is a tacet expectation on Unix systems, so that's a nice benefit too.)

➜  homework git:(main) ✗ diff foo.old.smt foo.new.smt | tail -n 15
976c999,1000
<   true)pred: (= |__prm:V0| 1)
---
>   true)
> pred: (= |__prm:V0| 1)
1014c1038,1039
<   true)pred: (= |__prm:V0| 1)
---
>   true)
> pred: (= |__prm:V0| 1)
1052c1077
<   true)
\ No newline at end of file
---
>   true)