Ανάλυση προγραμμάτων μέσω συμβολικής εκτέλεσής τους

Abstract

Most program analysis methods have been applied to optimising compilers. It is our belief that there is enough theory that could support the application of program analysis methods to software construction. Embedded and safety-critical systems but also large and complex software demand sophisticated tools for design, development, testing and maintenance of software. Symbolic execution is a method used to reconstruct logic and computations along a program path by executing the path with symbolic, rather than actual values of data. The results obtained by symbolic execution are the symbolic formulae, representing the values of the program variables, and the path condition for each path examined. Symbolic execution is a component of a tool which implements a kind of program analysis called symbolic analysis. Symbolic analysis comprises the transformation of a source program to an intermediate representation, the symbolic execution of the program using the intermediate representation, the determination of the feasibility of execution paths, the static error checking and other kinds of processing. All stages of symbolic analysis have been based on formal techniques. Regular expressions have been used in lexical analysis, BNF-rules in syntax analysis, attribute-collection in static-semantic analysis, algebra's homomorphism for the creation of the abstract syntax and semantics-directed symbolic execution.

Στο πεδίο ανάλυσης προγραμμάτων, οι περισσότερες μέθοδοι εφαρμόζονται στη βελτιστοποίηση των μεταγλωττιστών. Πιστεύουμε ότι υπάρχει αρκετή θεωρία, η οποία θα μπορούσε να υποστηρίξει την εφαρμογή των μεθόδων ανάλυσης προγραμμάτων στην ανάπτυξη λογισμικού. Ένθετα και ασφάλειας-κρίσιμα συστήματα, όπως, επίσης, και η ανάπτυξη πολύ μεγάλων και πολύπλοκων εφαρμογών, απαιτούν πιο περίτεχνα εργαλεία για τη σχεδίαση, ανάπτυξη, έλεγχο και συντήρηση λογισμικού. Η συμβολική εκτέλεση είναι μια μέθοδος, η οποία χρησιμοποιείται για την ανασυγκρότηση της λογικής και των υπολογισμών κατά μήκος μιας διαδρομής προγράμματος, εκτελώντας τη διαδρομή με συμβολικές τιμές παρά με πραγματικές τιμές για τις μεταβλητές εισόδου. Τα αποτελέσματα, από την εφαρμογή της μεθόδου, είναι οι συμβολικές παραστάσεις των μεταβλητών του προγράμματος, ως προς τις συμβολικές τιμές των μεταβλητών εισόδου και η συνθήκη-διαδρομής για κάθε διαδρομή που εξετάζεται. Η συμβολική εκτέλεση είναι μια εκ των συνιστωσών ενός εργαλείου, το οποίο υλοποιεί ένα είδος ανάλυσης προγραμμάτων που ονομάζεται συμβολική ανάλυση. Η συμβολική ανάλυση περιλαμβάνει τη μετατροπή ενός πηγαίου προγράμματος σε ενδιάμεση αναπαράσταση, στη συμβολική εκτέλεση του προγράμματος χρησιμοποιώντας την ενδιάμεση αναπαράσταση, στον προσδιορισμό της εφικτότητας εκτέλεσης των διαδρομών, στο στατικό έλεγχο σφαλμάτων και σε άλλου είδους επεξεργασία. Όλες οι φάσεις της συμβολικής ανάλυσης βασίστηκαν σε αυστηρές μαθηματικές τεχνικές. Κανονικές εκφράσεις στη λεξική ανάλυση, BNF-κανόνες στη συντακτική ανάλυση, συλλογή-ιδιοτήτων στη στατική-σημασιολογική ανάλυση, δημιουργία της αφαιρετικής σύνταξης με ομομορφισμό αλγεβρών και συμβολική εκτέλεση κατευθυνόμενη από τη δηλωτική σημασιολογία.