Rosette: can it help me
37 views
Skip to first unread message
Bertrand Augereau
Nov 26, 2020, 4:12:47 PM11/26/20
to racket users
Hello everybody,
not sure if this is the good place to ask about this but I couldn't
find a good location so I'm asking for help here, after all it's
strongly connected to Racket :)
I'm trying to reverse-engineer some specific piece of hardware with
the help of Rosette, to discover if it can help or not. In the long
run I want it to help me find magic numbers for a specific routine to
match captures of the hardware output (can't say more about this
though).
After dumbing down (a lot) my first tries, I'm having issues with this
code running endlessly:
#lang rosette/safe
(define (zero-a x) 0)
(define (zero-b x)
(if (= x 0) 0 (zero-b (- x 1))))
(define-symbolic x integer?)
(assert (>= x 0))
(assert (<= x 10))
(verify (assert (= (zero-a x) (zero-b x))))
I don't have a strong theoretical understanding of what Rosette can
and cannot do, but I thought that by restraining the range with the
asserts, at least I'd get a brute force search of the solution space,
which should be fast.
Does it make sense ? Can somebody explain me where is my misunderstanding ?
Thank you folks,
Bertrand
not sure if this is the good place to ask about this but I couldn't
find a good location so I'm asking for help here, after all it's
strongly connected to Racket :)
I'm trying to reverse-engineer some specific piece of hardware with
the help of Rosette, to discover if it can help or not. In the long
run I want it to help me find magic numbers for a specific routine to
match captures of the hardware output (can't say more about this
though).
After dumbing down (a lot) my first tries, I'm having issues with this
code running endlessly:
#lang rosette/safe
(define (zero-a x) 0)
(define (zero-b x)
(if (= x 0) 0 (zero-b (- x 1))))
(define-symbolic x integer?)
(assert (>= x 0))
(assert (<= x 10))
(verify (assert (= (zero-a x) (zero-b x))))
I don't have a strong theoretical understanding of what Rosette can
and cannot do, but I thought that by restraining the range with the
asserts, at least I'd get a brute force search of the solution space,
which should be fast.
Does it make sense ? Can somebody explain me where is my misunderstanding ?
Thank you folks,
Bertrand
Sorawee Porncharoenwase
Nov 26, 2020, 4:24:11 PM11/26/20
to Bertrand Augereau, racket users
You are doing a recursion on a symbolic value, which is a common pitfall in Rosette.
See slide 81 and subsequent slides for more details. Slide 87 shows a solution to this problem.
--
You received this message because you are subscribed to the Google Groups "Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to racket-users...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAHV%3D05otPXjbrEaHWvJF-SeDSxz2-Mjq3p%3DSHR3HvuJRAJJ3-A%40mail.gmail.com.
Bertrand Augereau
Nov 26, 2020, 4:29:40 PM11/26/20
to Sorawee Porncharoenwase, racket users
Thank you very much for the fast and precise answer, I'll study this !
Le jeu. 26 nov. 2020 à 22:24, Sorawee Porncharoenwase
<sorawe...@gmail.com> a écrit :
Le jeu. 26 nov. 2020 à 22:24, Sorawee Porncharoenwase
<sorawe...@gmail.com> a écrit :
Reply all
Reply to author
Forward
0 new messages