*created "Mon Oct 9 15:06:42 1995" *by "Paul E. Black" *modified "Mon Dec 8 10:11:54 1997" *by "Paul E. Black" Notes on running the parser. All these steps must be done in HOL90. Running the parser 1. load the builder and grammar functions. This loads other files such as the lexical analyser and parser. use "c2holBuild.sml"; 2. to turn on parse tracing (to debug the grammar, etc.), do traceParse := true; to see the furthest the parsing got, do print (upcoming (!remainingToks) ^ "\n"); turn parse tracing off with traceParse := false; 3a. parse C code with c2hol `C code`; 3b. parse C code in a file with c2holf "filename.c"; 4. Here are test cases to validate the parser: test_result (c2hol(`w(){*p=43;}`)) (--`Cffun (Func (Var "w" 0 Int) [] [] (SOMEBody (Block [] (Simple (Assign (Deref (Lval (Vref (Var "p" 0 UnknownType)))) (Const (CCint 43) Int)))))) EndOfCFile`--); test_result (c2hol( `w(){struct stat buf;while(buf.st_uid!=0)p=3;}` )) (--`Cffun (Func (Var "w" 0 Int) [] [] (SOMEBody (Block [Var "buf" 0 (Struct "stat")] (CWhile (Binary (Lval (Field (Vref (Var "buf" 0 (Struct "stat"))) (Var "st_uid" 0 Int))) NEq (Const (CCint 0) Int)) (Simple (Assign (Vref (Var "p" 0 UnknownType)) (Const (CCint 3) Int))))))) EndOfCFile`--); test_result (c2hol `x(){"Hello, World!";}`) (--`Cffun (Func (Var "x" 0 Int) [] [] (SOMEBody (Block [] (Simple (Const (CCstr "Hello, World!") (Ptr Char)))))) EndOfCFile`--); test_result (c2hol ` #define e "this is a char" char f; int d; struct time_t p[102595]; y(){ { int f; #define d 32 f=d;} p[37]=e;f=d;} `) (--`Cfdcl [Var "f" 0 Char; Var "d" 0 Int; Var "p" 1 (Array (Struct "time_t") (CCint 102595))] (Cffun (Func (Var "y" 0 Int) [] [] (SOMEBody (Block [] (Seq (Block [Var "f" 1 Int] (Simple (Assign (Vref (Var "f" 1 Int)) (Const (CCid "d") Int)))) (Seq (Simple (Assign (Aryref (Var "p" 1 (Array (Struct "time_t") (CCint 102595))) (Const (CCint 37) Int)) (Const (CCid "e") (Ptr Char)))) (Simple (Assign (Vref (Var "f" 0 Char)) (Const (CCid "d") Int)))))))) EndOfCFile)`--); test_result (c2hol `z(){char g; g='a';}`) (--`Cffun (Func (Var "z" 0 Int) [] [] (SOMEBody (Block [Var "g" 0 Char] (Simple (Assign (Vref (Var "g" 0 Char)) (Const (CCstr "a") Char)))))) EndOfCFile`--); test_result (c2hol `g(c,a,b,s)char b, *c[];int s[MAX];{7;}`) (--`Cffun (Func (Var "g" 0 Int) [(Var "c" 1 (Array (Ptr Char) (CCid "UNK"))); (Var "a" 0 Int); (Var "b" 1 Char); (Var "s" 1 (Array Int (CCid "MAX")))] [] (SOMEBody (Block [] (Simple (Const (CCint 7) Int))))) EndOfCFile`--); test_result (c2hol `x(){char p1,p2;g1(p1[2],&(p2));}`) (--`Cffun (Func (Var "x" 0 Int) [] [] (SOMEBody (Block [Var "p1" 0 Char; Var "p2" 0 Char] (Simple (Call (Var "g1" 0 UnknownType) (PL (Lval (Aryref (Var "p1" 0 Char) (Const (CCint 2) Int))) (PL (LUnary AdrOf (Vref(Var "p2" 0 Char)))PLnull))))))) EndOfCFile`--); test_result (c2hol `void g1,g2,h;int q;g0(p1){g0();g1(p1+1);g2(h(2),"hi");}`) (--`Cfdcl [Var "g1" 0 Void; Var "g2" 0 Void; Var "h" 0 Void; Var "q" 1 Int] (Cffun (Func (Var "g0" 0 Int) [Var "p1" 0 Int] [] (SOMEBody (Block [] (Seq (Simple (Call (Var "g0" 0 UnknownType) PLnull)) (Seq (Simple (Call (Var "g1" 0 Void) (PL(Binary(Lval(Vref(Var "p1" 0 Int)))Add(Const(CCint 1) Int)) PLnull))) (Simple (Call (Var "g2" 0 Void) (PL(Call (Var "h" 0 Void) (PL (Const (CCint 2) Int) PLnull)) (PL (Const (CCstr "hi") (Ptr Char)) PLnull))))))))) EndOfCFile)`--); test_result (c2hol ` void c,d,t,m,n;int cup; y(){char h,q;FILE *a;if(0!=h)q=*a;else *a=37; if(c>d){t=m++;m=cup("joe");n=59;}}`) (--`Cfdcl [Var "c" 0 Void; Var "d" 0 Void;Var "t" 0 Void; Var "m" 0 Void; Var "n" 0 Void; Var "cup" 1 Int] (Cffun (Func (Var "y" 0 Int) [] [] (SOMEBody (Block [Var "h" 0 Char; Var "q" 0 Char; Var "a" 0 (Ptr (Struct"FILE"))] (Seq (IfElse (Binary (Const (CCint 0) Int) NEq (Lval (Vref (Var "h" 0 Char)))) (Simple (Assign (Vref (Var "q" 0 Char)) (Lval (Deref(Lval(Vref (Var "a" 0(Ptr(Struct"FILE"))))))))) (Simple (Assign (Deref(Lval(Vref (Var "a" 0 (Ptr (Struct "FILE")))))) (Const (CCint 37) Int)))) (If (Binary (Lval(Vref(Var "c" 0 Void))) Gt (Lval(Vref(Var "d" 0 Void)))) (Block [] (Seq (Simple (Assign(Vref(Var "t" 0 Void)) (LUnary PostInc (Vref(Var "m" 0 Void))))) (Seq (Simple (Assign (Vref (Var "m" 0 Void)) (Call (Var "cup" 1 Int) (PL (Const (CCstr "joe") (Ptr Char)) PLnull)))) (Simple (Assign (Vref (Var "n" 0 Void)) (Const (CCint 59) Int))))))))))) EndOfCFile)`--); test_result (c2hol `x(){if((k>'\0')||j){int *l;l[7]='X'-1;}else{2<=5;}}`) (--`Cffun (Func (Var "x" 0 Int) [] [] (SOMEBody (Block [] (IfElse (Binary (Binary (Lval (Vref (Var "k" 0 UnknownType))) Gt (Const (CCstr EOS) Char)) Or (Lval (Vref (Var "j" 0 UnknownType)))) (Block [Var "l" 1 (Ptr Int)] (Simple (Assign (Aryref (Var "l" 1 (Ptr Int)) (Const (CCint 7) Int)) (Binary (Const (CCstr "X") Char) Sub (Const (CCint 1) Int))))) (Block [] (Simple (Binary (Const (CCint 2) Int) LEq (Const (CCint 5) Int)))))))) EndOfCFile`--); test_result (c2hol `n(){struct k t;int j;t.r='\n';return &t;}`) (--`Cffun (Func (Var "n" 0 Int) [] [] (SOMEBody (Block [Var "t" 0 (Struct "k"); Var "j" 0 Int] (Seq (Simple (Assign (Field (Vref (Var "t" 0 (Struct "k"))) (Var "r" 0 Int)) (Const (CCstr CR) Char))) (Ret (LUnary AdrOf (Vref (Var "t" 0 (Struct "k"))))))))) EndOfCFile`--); (* ERROR: parser gets precedence and assoc. of binary operators wrong: the expression below should parse as ((k==ip)&&x) && y, but instead it parses as k == (ip && (x&&y)). *) test_result (c2hol ` #define k 0 w(ip)int *ip;int x,y;{k==ip&&x&&y;} `) (--`Cffun (Func (Var "w" 0 Int) [Var "ip" 1 (Ptr Int)] [] (SOMEBody (Block [] (Simple (Binary (Const (CCid "k") Int) Eq (Binary (Lval (Vref (Var "ip" 1 (Ptr Int)))) And (Binary (Lval (Vref (Var "x" 0 Int))) And (Lval (Vref (Var "y" 0 Int)))))))))) EndOfCFile`--); print "Tests done. **\n"; % end of $Source: /users/lal/black/hol/Disser/RCS/c2holReadMe.sml,v $ %