Ο προγραμματισμός στη λογική μπορεί να σας βοηθήσει να παράγετε καλύτερα βελτιστοποιημένο, πιο ασφαλή κώδικα χωρίς σφάλματα… αν ξέρατε πώς να το κάνετε.
Μου πήρε περίπου δύο χρόνια για να γράψω το πρώτο μου πρόγραμμα στο Z3. Είχα κάνει μερικά μαθήματα, έγραψα κώδικα για να λύσω παζλ με παραδείγματα άλλων ανθρώπων, αλλά δεν μπορούσα πραγματικά να καταλάβω πώς να περάσω από τις πολύ αφηρημένες περιπτώσεις χρήσης «παιχνιδιών» σε εφαρμογές που είχαν πραγματική συνάφεια.
Το Z3 είναι ένας λύτης Satisfiability modulo theories (SMT), ένας ξάδερφος με τους λύτες ικανοποίησης (SAT) Έχω γράψει για το παρελθόν. Ενώ οι επιλύτες SAT απαιτούν την κωδικοποίηση των πάντων σε ένα σύνολο προτάσεων True/False, οι λύτες SMT επιτρέπουν μεγαλύτερη εκφραστικότητα. Σε απλό SAT μπορείτε να αναπαραστήσετε την πρόσθεση αντιπροσωπεύοντας αριθμούς σε δυαδικό και εκτελώντας λογικές πράξεις για να παράγετε το σωστό άθροισμα. Εξάλλου, αυτός είναι ο τρόπος με τον οποίο η CPU επεξεργάζεται τα πάντα. Εάν αυτή η έννοια είναι εντελώς ξένη σε εσάς, προτείνω να δείτε το NAND to Tetris ως έναν εξαιρετικό τρόπο για να εξερευνήσετε πώς οι λογικές πύλες ενσωματώνονται σε πολύπλοκους επεξεργαστές.
Στο SMT, ωστόσο, μπορείτε απλώς να γράψετε 2+2 ως 2+2, επειδή το SMT βασίζεται σε αυτές τις αφαιρέσεις (που ονομάζονται "θεωρίες") ... βασικά: όπως μια γλώσσα προγραμματισμού όπως η python θα σας επιτρέψει να γράψετε πράγματα με φράσεις που μοιάζουν στα αγγλικά, επειδή καταλαβαίνει πώς Για να μετατρέψουν αυτές τις φράσεις στον κώδικα μηχανής που έπρεπε να αντιμετωπίσουν οι προγραμματιστές της παλιάς σχολής, οι λύτες SMT επέτρεψαν στους ανθρώπους να γράφουν πιο καθαρά μοντέλα, επειδή κατανοούν πώς να μετατρέπουν το 2+2 σε λογική.
Υπάρχουν δύο κύριοι τρόποι με τους οποίους λειτουργούν οι θεωρίες στο SMT. Το πρώτο είναι ουσιαστικά απλώς η μεταγλώττιση στο ισοδύναμο SAT και η εκτέλεσή του ως ένα μεγάλο SAT. Η δεύτερη προσέγγιση ενσωματώνει αυτά τα μη-Boolean ειδικά τμήματα του μοντέλου σε ένα πρόβλημα SAT εντός του SAT που πρέπει να αντιμετωπιστεί ξεχωριστά. Το πλεονέκτημα της δεύτερης προσέγγισης είναι η μεγαλύτερη αποτελεσματικότητα σε ερωτήσεις όπως: x + y = y + x
Όλα αυτά είναι πολύ ωραία και εντελώς άχρηστα αν δεν μπορείτε να καταλάβετε πώς να αναπαραστήσετε το πρόβλημά σας με λογική + αριθμητική. Και πολλά από αυτά που κάνουν οι προγραμματιστές δεν μοιάζουν με λογική + αριθμητική… τουλάχιστον όχι με την πρώτη ματιά.
Σκέψου σαν μεταγλωττιστής
Μαθαίνω πολλά από την προσπάθεια να μάθω άλλα πράγματα και αυτή ήταν μια από αυτές τις καταστάσεις. Είχα σταματήσει να προσπαθώ να καταλάβω πώς να γράφω SMT και να χρησιμοποιώ το Z3. Ήταν απλά πάρα πολύ δύσκολο.
Μετά άρχισα να μαθαίνω πώς λειτουργούν οι μεταγλωττιστές.
Εάν θέλετε να πάρετε ένα κομμάτι κώδικα και να το αναπαραστήσετε στο Z3, πρέπει να ακολουθήσετε τα ίδια βήματα που θα έκανε ο μεταγλωττιστής. Αυτό συμβαίνει επειδή τόσο οι SMT/SAT όσο και οι CPU σκέφτονται με λογική boolean. Έτσι, για να εκτελεστεί ένα κομμάτι κώδικα πρέπει να μεταφραστεί σε λογική boolean. Αυτό σημαίνει τα ακόλουθα βήματα*:
- Ενσωμάτωση όλων των λειτουργιών. Οι λειτουργίες είναι επαναχρησιμοποιήσιμα και καλούμενα μπλοκ κώδικα είναι χρήσιμα για ανθρώπους για τους οποίους λιγότερος κώδικας σημαίνει καλύτερη αναγνωσιμότητα. Αλλά δεν είναι χρήσιμο για τον υπολογιστή που θα προτιμούσε μια ωραία ροή οδηγιών η μία μετά την άλλη, κινούμενη μόνο προς τα εμπρός και ποτέ προς τα πίσω. Έτσι, ένας μεταγλωττιστής παίρνει όλες τις προσεγμένες κλήσεις συναρτήσεων και τις αντικαθιστά με το σώμα της συνάρτησης έτσι ώστε ο κώδικας να είναι όσο το δυνατόν πιο επίπεδος.
- Εξέλιξη βρόχων/αναδρομής. Θέλουμε επίπεδο κώδικα, επομένως πρέπει να φύγουν και αυτοί οι βρόχοι. Αυτό λειτουργεί με τον ίδιο τρόπο όπως το in-lining, απλώς αντιγράφουμε και επικολλούμε το μπλοκ κώδικα στον βρόχο ίδιες φορές με τον βρόχο.
- Κάντε τις μεταβλητές αμετάβλητες. Διαφορετικά, γνωστό ως Single Static Assignment (SSA) το
a = a + bγίνεταιa1 = a + b, έτσι ώστε μόλις εκχωρηθεί μια τιμή σε μια μεταβλητή, δεν αλλάζει.
*τα geek του μεταγλωττιστή θα έρθουν εδώ με μερικά "καλά στην πραγματικότητα..." σχετικά με τις παραλλαγές και τις συζητήσεις στο σχεδιασμό του μεταγλωττιστή, κάτι που είναι ενδιαφέρον αλλά εκτός θέματος για αυτήν την ανάρτηση. Το θέμα είναι να ακολουθήσετε αυτά τα βήματα θα σας δώσει κώδικα που μοιάζει με μοντέλο Z3.
Εκ των υστέρων, αυτό φαίνεται πραγματικά προφανές: αφού ο επεξεργαστής σκέφτεται με λογική boolean, φυσικά μπορείτε να δημιουργήσετε μοντέλα στο Z3 ακολουθώντας την ίδια διαδικασία που χρησιμοποιεί ο μεταγλωττιστής για να παρουσιάσει αυτόν τον κώδικα σε λογική boolean. Γιατί δεν υπάρχουν περισσότερα εργαλεία για να μεταγλωττίσετε απευθείας σε μια φιλική μορφή SMT ή SAT για εσάς;
Καλά…. Αυτό συμβαίνει επειδή ένα μοντέλο SMT/SAT είναι κάτι περισσότερο από ένα σύνολο οδηγιών. Είναι ένα παζλ. Μπορείτε να μετατρέψετε τον κώδικα αυτόματα, αλλά αυτό δεν είναι πολύ χρήσιμο. Χωρίς ισχυρισμούς (ή κατηγορήματα όπως συνήθως ονομάζονται) δεν υπάρχει τίποτα που να λύσει ο λύτης. Η μετατροπή του κώδικα είναι ένα κρίσιμο κομμάτι, τότε πρέπει να πείτε στον Z3 ποιες καταστάσεις να λύσει.
Και εδώ έχετε δύο επιλογές: είτε πείτε στον λύτη ποιες καταστάσεις απαιτούνται και επιστρέφει τις διάφορες συνθήκες στις οποίες συμβαίνουν αυτές οι καταστάσεις είτε πείτε στον λύτη ποιες καταστάσεις είναι αδύνατες και ελέγξτε για να βεβαιωθείτε ότι είστε σωστές. Αυτά τα δύο μονοπάτια ανοίγουν έναν κόσμο πιθανών εφαρμογών. Εάν ζητήσετε από το μοντέλο να δημιουργήσει έγκυρες καταστάσεις, μπορείτε να δημιουργήσετε βελτιστοποιητές (να βρείτε μια λύση που είναι πιο γρήγορη ή χρησιμοποιεί λιγότερο κώδικα από μια γνωστή λύση), μπορείτε να γράψετε ένα fuzzer, μπορείτε να συνθέσετε κώδικα και αντίστροφη μηχανική (αν και αυτό μάλλον δεν είναι πρακτικό για μεγάλα προγράμματα)
Εάν ζητήσετε από το μοντέλο να βρει μη έγκυρες καταστάσεις, μπορείτε να ελέγξετε για σφάλματα (ειδικά ζητήματα ταυτόχρονης χρήσης), μπορείτε να επαληθεύσετε ότι δύο κομμάτια κώδικα κάνουν το ίδιο πράγμα (χρήσιμο αν θέλετε να απλοποιήσετε), μπορείτε να ελέγξετε για ζητήματα ασφαλείας… . και πάνω και πάνω και επάνω.
Bytecode σε Z3
Ακριβώς επειδή δεν μπορούμε να δημιουργήσουμε αυτόματα κώδικα φιλικό προς το SMT/SAT, δεν σημαίνει ότι πρέπει να κάνουμε όλη τη δουλειά του μεταγλωττιστή στα κεφάλια μας. Πολλοί μεταγλωττιστές θα σας επιτρέψουν να επιθεωρήσετε κάποιο μέρος αυτού που δημιουργούν στη διαδικασία. Στην python, για παράδειγμα, η ενότητα dis θα εξάγει τον bytecode του προγράμματος. Χρησιμοποιώντας έναν απλό κώδικα γραμμένο σε python, μπορώ να δείξω πώς μπορείτε να αιτιολογήσετε τον πρακτικό κώδικα που γράφετε καθημερινά στο SMT.
Πάρτε για παράδειγμα αυτήν τη μικρή συνάρτηση που ελέγχει εάν ένα έτος είναι δίσεκτο:
def leap(year):
if year % 4 == 0 and year % 100 != 0:
return true
else:
return false
Μπορείτε πραγματικά να γράψετε μοντέλα Z3 σε python, κάτι που είναι χρήσιμο εδώ επειδή η SMT-LIB2 (η προτιμώμενη γλώσσα του Z3) χρησιμοποιεί στιλβωτική σημείωση… και αν δεν είστε εξοικειωμένοι με αυτό, αυτά τα παραδείγματα θα είναι πιο δύσκολο να κατανοήσετε.
Αλλά διαφορετικά αυτό είναι πολύ εύκολο να μετατραπεί σε Z3. Δεν χρειάζεται καν να συμβουλευόμαστε τον bytecode για ιδέες:
from z3 import *
year = Int('year')
s = Solver()
s.add(year % 4 == 0)
s.add(year % 100 != 0)
s.check()
Όταν εκτελούμε αυτό το μοντέλο, το Z3 θα καθορίσει εάν υπάρχει μια τιμή για τη μεταβλητή year που ικανοποιεί τους δύο κανόνες που της έχουμε δώσει. Εάν η απάντηση είναι ναι, μπορούμε να προσθέσουμε τη γραμμή s.model() για να εξάγουμε μία πιθανή λύση. Κάνοντας αυτό μπορεί να επιστρέψει μια εκπληκτική τιμή (για παράδειγμα -96!) που δεν είναι έγκυρο έτος και θα μπορούσε να είναι ένα πιθανό σφάλμα στο πρόγραμμά μας.
Αλλά αντί να τρέχουμε το μοντέλο ξανά και ξανά και ξανά, αναζητώντας ακραίες θήκες μπορούμε να είμαστε λίγο πιο πραγματιστές. Αν ξέρουμε ποιες καταστάσεις θα έπρεπε να είναι αδύνατες. Για παράδειγμα, γνωρίζουμε ότι τα έτη χιλιετίας είναι δίσεκτα και ότι τα έτη που τελειώνουν με περιττό αριθμό δεν μπορεί να είναι δίσεκτα. Προσθέτοντας αυτά τα χαρακτηριστικά ως ισχυρισμούς στο μοντέλο μας, μπορούμε να ελέγξουμε εάν ο αλγόριθμός μας είναι ακριβής ή όχι:
from z3 import *
year = Int('year')
s = Solver()
s.add(year % 4 == 0)
s.add(year % 100 != 0)
s.push()
s.add(year == 2000)
if s.check() == unsat:
print("2000 failed")
s.pop()
s.push() # Reload the original two rules
s.add(year != 1953, year != 1800, year != 1969)
if s.check() == unsat:
print("Non-leap year not detected")
s.check()
Ωχ! Ξεχάσαμε την εξαίρεση της χιλιετίας στον κανόνα του δίσεκτου έτους! Με ένα απλό πρόγραμμα πιθανότατα δεν χρειαζόμασταν έναν SMT επίλυσης για να εντοπίσουμε αυτό το πρόβλημα, αλλά με πιο περίπλοκα προγράμματα τέτοια σφάλματα μπορούν να παραμείνουν κρυφά για χρόνια.
Σημείωση s.push() και s.pop() μας επιτρέπουν να προσθέτουμε και να αφαιρούμε ισχυρισμούς. Μεταξύ άλλων, αυτό θα μας επιτρέψει να ελέγξουμε σταδιακά ένα μοντέλο.
Τι γίνεται όμως με ένα πιο περίπλοκο πρόγραμμα;
def calc(x, y):
if(x < y):
x = x + y
for i in range(0,3):
y = x + next(y)
return x + y
def next(y):
return y + 1
Αν και είναι μόνο μερικές γραμμές κώδικα, αντιπροσωπεύει πολλές κατασκευές που πρέπει να μεταφράσουμε για να μοντελοποιήσουμε σωστά στο SMT. Υπάρχει αλλαγή μεταβλητής, υπάρχουν κλήσεις συναρτήσεων, υπάρχουν βρόχοι…. Αυτό το πρόγραμμα είναι αρκετά απλό ώστε να μπορείτε να μεταφράσετε μόνοι σας σε μορφή SMT, αλλά ας χρησιμοποιήσουμε τον bytecode για αυτό ως οδηγό
>>> dis.dis(calc)
2 0 LOAD_FAST 0 (x)
2 LOAD_FAST 1 (y)
4 COMPARE_OP 0 (<)
6 POP_JUMP_IF_FALSE 16
3 8 LOAD_FAST 0 (x)
10 LOAD_FAST 1 (y)
12 BINARY_ADD
14 STORE_FAST 0 (x)
5 >> 16 SETUP_LOOP 30 (to 48)
18 LOAD_GLOBAL 0 (range)
20 LOAD_CONST 1 (0)
22 LOAD_CONST 2 (3)
24 CALL_FUNCTION 2
26 GET_ITER
>> 28 FOR_ITER 16 (to 46)
30 STORE_FAST 2 (i)
6 32 LOAD_FAST 0 (x)
34 LOAD_GLOBAL 1 (next)
36 LOAD_FAST 1 (y)
38 CALL_FUNCTION 1
40 BINARY_ADD
42 STORE_FAST 1 (y)
44 JUMP_ABSOLUTE 28
>> 46 POP_BLOCK
7 >> 48 LOAD_FAST 0 (x)
50 LOAD_FAST 1 (y)
52 BINARY_ADD
54 RETURN_VALUE
Η τεκμηρίωση για το dis περιέχει περιγραφές κάθε εντολής, αλλά ουσιαστικά αυτό που συμβαίνει εδώ είναι:
# if(x < y): - Put the value of x on the stack - Put the value of y on the stack - Pop x and y off the stack and put the result of x < y on the stack - If top of stack (TOS) is False, pop it off and jump forward to 16 # x = x + y - Put the value of x on the stack - Put the value of y on the stack - Pop x and y off the stack and put the result of x + y on the stack - Pop the TOS and assign it to variable x # for i in range(0,3): - Repeat instructions 30 to 48 - Put beginning of range on TOS - Put end of range on TOS - Pop beginning and end off stack and put range call result on TOS - Convert list to iterable and put on TOS - Call next on the iterable, put on TOS - Pop the TOS and assign it to variable i # y = x + next(y) - Put the value of x on the stack - Put instructions for function next on the stack - Put the value of y on the stack - Pop next function and y off the stack and call function next(y) - Pop results of next(y) and value of x off the stack and add - Pop result off the stack and assign to variable y
Προφανώς υπάρχουν περισσότερα, αλλά καταλαβαίνεις το νόημα. Με αυτό τον τρόπο, είναι πιο εύκολο να δείτε πώς να αναπαραστήσετε αυτήν τη λειτουργία στο Z3. Ευτυχώς ο βρόχος μας έχει μόνο τρεις επαναλήψεις, αν είχε περισσότερες ή ήταν while True:, θα έπρεπε να αποφασίσουμε πώς θα το χειριστούμε επειδή τα μοντέλα Z3 είναι οριοθετημένα, που σημαίνει ότι οι βρόχοι πρέπει να έχουν συγκεκριμένα τελικά σημεία. Επίσης, επειδή το SMT/SAT είναι NP-complete, ένα μοντέλο μπορεί να πάρει πολύ χρόνο για να επιστρέψει μια απάντηση ή ποτέ να μην επιστρέψει καθόλου…. Επομένως, είναι γενικά καλή ιδέα να διατηρήσετε τον αριθμό των επαναλήψεων χαμηλό.
Τέλος πάντων, στο Z3 η συνάρτηση υπολογισμού θα μοιάζει με αυτό:
x, x1 = Ints('x x1')
y, y1, y2, y3 = Ints('y y1 y2 y3')
nextv, nextv1, nextv2 = Ints('nextv nextv1 nextv2')
result = Int('result')
s = Solver()
s.add(If(x<y, x1 == x + y, x1 == x))
s.add(nextv == y + 1)
s.add(y1 == x1 + nextv)
s.add(nextv1 == y1 + 1)
s.add(y2 == x1 + nextv1)
s.add(nextv2 == y2 + 1)
s.add(y3 == x1 + nextv2)
s.add(result == x1 + y3)
s.check()
s.model()
Εφόσον χρησιμοποιούμε τις συνδέσεις python για το Z3, μπορούμε να ελέγξουμε ότι λειτουργεί εκτελώντας την αρχική συνάρτηση και, στη συνέχεια, προσθέτοντας πρόσθετες συνθήκες στον λύτη μας, ορίζοντας την τιμή του αποτελέσματος και ζητώντας του να λύσει για x, y Αν και πιθανότατα θα ανακαλύψουμε επίσης ότι υπάρχουν άλλοι πιθανοί x, y συνδυασμοί που θα έχουν το ίδιο αποτέλεσμα!
Μάθετε περισσότερα…
Ας ελπίσουμε ότι σας βοήθησα να κατανοήσετε πώς να αναπαραστήσετε τον κώδικα που εργάζεστε τώρα στο SMT. Εάν είστε έτοιμοι να αρχίσετε να πηγαίνετε βαθύτερα στον κόσμο του Z3, ακολουθούν μερικοί πόροι που θα συνιστούσα:
- Formal Methods for Informal Engineers, Z3 Tutorial Αυτό είναι το βιβλίο εργασίας από ένα διαδικτυακό συνέδριο που έγινε φέτος, αλλά ο εκπαιδευτής (Philip Zucker) συμπεριέλαβε βοηθητικά τη διάλεξή του ως γραπτές σημειώσεις δίπλα στις ασκήσεις.
- Εφαρμογές επιλυτών SMT στην επαλήθευση προγράμματος Αυτό είναι ένα υπέροχο χαρτί που εξηγεί τους τύπους δοκιμών που μπορεί να θέλετε να κάνετε με το Z3 σε διαφορετικούς τύπους προγραμμάτων, με πολλά παραδείγματα για τον τρόπο κατασκευής τους.
