Section 1 -- IntroductionSection 1 - IntroductionUNISEX, a UNIx-based Symbolic EXecutor for Pascal, provides an environment for testing andverification of programs. This document is a guide to using UNISEX. Section 2 presents an overview ofthe capabilities and usage of the symbolic executor itself. Section 3 describes UNISEX Pascal, a Pascalsubset with an integrated assertion language. A more detailed description can be found in The UNISEXPascal Language Reference Manual. Section 4 is a detailed listing of the symbolic executor commands.The symbolic executor has been developed to run on the VAX 11/780, running under the Unix operatingsystem. It also requires the use of the Franz Lisp interpreter environment. UNISEX consists of a crosscompiler and a set of Lisp utility routines. The cross compiler was developed using the Lex lexicalanalyzer generator and the YACC compiler generator, and takes as source code the Pascal program to besymbolically executed. The output of the compiler is a valid Franz Lisp source program. This Lisp pro-gram, when run under the Franz Lisp interpreter (along with the utility routines) is an interactive symbolicexecutor of the original Pascal program.- 2 -Section 2 -- UNISEX System FeaturesSection 2 - UNISEX System FeaturesThe UNISEX system provides a symbolic execution approach for testing or verification. Its key featuresare:It supports a large subset of Pascal, described in the UNISEX Pascal Language Reference Manual.It runs on UNIX, and is thus easier to use than similar systems on less friendly operating systems.It allows the user to choose test or verify mode. In test mode, it gives the user the option of executingwith numeric or symbolic values. In verify mode, it gives the user the option of automatic or manual exe-cution.Overview of Operation Overview of Operation The UNISEX system is currently invoked with a shellscript in unisex (/usr/local/unisex on the UCSB Computer Science Instructional Vax). A Pascal program inthe file program.p would be executed with the command: unisex program.p This causes the Pas-cal program to be compiled and loaded, after which the user is prompted to choose test or verify mode andinitialize the UNISEX debug functions. In test mode UNISEX will prompt the user to initialize globalvariables. The user may then enter a sequence of assignments of the form variable = value, separated bycommas. If all of the values are numeric UNISEX will act like a symbolic debugger. UNISEX can beused for generating path predicates or for more general testing by giving variables symbolic values.1 2Symbolic values entered by the user must have the same syntax as Pascal identifiers. UNISEX-generatedsymbolic values will generally begin with a special symbol: for scalar values, and for pointer values. Inthis mode the user has available all of the UNISEX commands presented in Section 4 except verify and au-toverify. In verify mode all variables are assigned symbolic values by the system, and the full commandset is available. In this mode UNISEX keeps track of verified paths, as well as paths that have beentraversed but were not verifiable.3 4Since the UNISEX simplifier is not very powerful, the user is asked toevaluate most verification conditions and branch conditions. UNISEX actually has two simplifiers; one forprograms with variables of type real and the other for programs without variables of type real. Internallythe difference is that the real simplifier does not use all of the rewrite rules used by the integer simplifier.From the user’s point of view the difference is that two identical expressions may not look the same aftersimplification if one occurs in a program with real numbers and the other in a program without realnumbers. These can be reviewed with the paths command.Trace options Trace options UNISEX allows the user to choose the amount of information displayed asexecution progresses. Turning the branch option on causes all decisions to be displayed. Turning verb ondoes that, and also displays statements just before they get executed, and the results of assignments. Thedefault for both is off. In addition, the simplifier may be turned off so that the results of all operations willbe stored and displayed in unsimplified symbolic form.Breakpoints Breakpoints UNISEX allows the user to set and remove breakpoints at any statement in aprogram at any time (except in autoverify mode, when breakpoints are ignored). In addition the user mayset step on, which is equivalent to having a breakpoint at every statement.- 3 -States States The of a UNISEX symbolic execution consists of a path condition (pc), a program counterand the current value of each variable. The pc is a predicate that represents all of the known constraints onsymbolic values occurring in the program. It is always initialized to before starting an execution, whichsays that nothing is known about any symbolic values. Whenever a decision is unresolvable (i.e., pc is notstrong enough to imply the test or its negation), both branches must be traversed to completely cover theexecution tree [2]. To do this, it must be possible to postpone one of the branches while continuing the oth-er. In UNISEX, the user is given almost unlimited freedom in moving around in the execution tree,through the use of the save and restore commands. The state can be saved at any time, and any saved statecan be restored at any time, without affecting the other saved states. This allows the user to, for example,choose a branch, pursue it for a while, saving more states, and then decide that it would be better to do theother branch first instead. This other branch could be restarted with the restore command without affect-ing the subsequently saved states.Miscellaneous Displays Miscellaneous Displays At any time UNISEX is displaying the prompt the usermay look at: fragments of the program, the path condition, a list of the saved states, the values of variables,and a few more things detailed in Section 4.Test Mode Test Mode Any valid UNISEX Pascal program may be executed in test mode. Assertionlanguage statements may be included, but are not necessary. Details of what each assertion statement typedoes can be found in Section 13 of the Language Reference Manual. In this mode the path condition canbe modified in four ways: by encountering an entry or assume statement, by the user explicitly modifyingit with the addpred command, or by executing an unresolvable decision statement. As noted in the over-view,