(* $Header: /users/lal/black/hol/Disser/RCS/semeqTactics.sml,v 1.9 1997/05/19 23:13:19 black Exp $ *) (* *created "Mon Mar 17 09:22:13 1997" *by "Paul E. Black" *) (* *modified "Mon May 19 16:47:40 1997" *by "Paul E. Black" *) (*---------------------------------------------------------------------------- Tactics about semantic equivalence of C statments and expressions. ----------------------------------------------------------------------------*) new_parent "semeq"; (* the "handle" allows cast2hol to (try to) be reloaded *) use "cast2hol.sml" handle _ => (); add_theorems_to_sml "semeq"; (* print a list of terms *) fun print_terml terml = (print "["; if terml <> [] then (print_term (hd terml); map (fn x=>(print "; "; print_term x)) (tl terml)) else [()]; print "]"); (*------ Generate unique, special names for intermediate results, etc. -----*) (* the special variable representing the result of C expressions *) val C_RESULT = "C_Result"; (* generate a new, unique variable name *) local val C_Result_count = ref 0 in fun new_C_Result () = (C_Result_count := (!C_Result_count)+1; C_RESULT ^ (Int.toString (!C_Result_count))) end; (*------------------ break out expressions ----------------------------------*) (* replace an occurrence of expr with a new lval in code *) fun break_out expr lval code = if ctype_of expr <> ctype_of lval then (print_term expr;print "\n"; print_term lval;print "\n"; raise Fail "expr and lval are different C types in break_out") else let fun bko ex lv cd = if cd = ex then (true, (--`Lval ^lv`--)) else if is_comb cd then let val {Rator=opr,Rand=oprand} = dest_comb cd val (replaced,newopr) = bko ex lv opr in if replaced then (true, mk_comb{Rator=newopr,Rand=oprand}) else let val (repinrand,newrand) = bko ex lv oprand in (repinrand, mk_comb{Rator=opr,Rand=newrand}) end end else (false, cd) in bko expr lval code end; (* tests test_result (#2 (break_out (--`Const (CCint 2) Int`--) (--`Vref (Var "b" 0 Int)`--) (--`Binary (Const (CCint 2) Int) Add (Lval (Vref(Var "c" 0 Int)))`--))) (--`Binary (Lval (Vref (Var "b" 0 Int))) Add (Lval (Vref (Var "c" 0 Int)))`--); test_result (#2 (break_out (--`Const (CCint 2) Int`--) (--`Vref (Var "b" 0 Int)`--) (--`Binary (Const (CCint 2) Int) Add (Const (CCint 2) Int)`--))) (--`Binary (Lval (Vref (Var "b" 0 Int))) Add (Const (CCint 2) Int)`--); test_result (#2 (break_out (--`Const (CCint 3) Int`--) (--`Vref (Var "b" 0 Int)`--) (--`Binary (Const (CCint 2) Int) Add (Lval (Vref(Var "c" 0 Int)))`--))) (--`Binary (Const (CCint 2) Int) Add (Lval (Vref (Var "c" 0 Int)))`--); (* fails because they are different types *) break_out (--`Const (CCstr "a") Char`--) (--`Vref (Var "b" 0 Int)`--) (--`Binary (Const (CCstr "a") Char) Gt (Const (CCstr "b") Char)`--); *) (*----------------------------------------------------------------------- Prove that an expression has no side effects. -----------------------------------------------------------------------*) fun prove_NoSE expr = prove((--`NoSE ^expr`--), REPEAT (MATCH_ACCEPT_TAC NoSE_Const ORELSE MATCH_ACCEPT_TAC NoSE_LVvar ORELSE MATCH_MP_TAC NoSE_LVarray ORELSE MATCH_MP_TAC NoSE_LVderef ORELSE MATCH_MP_TAC NoSE_LVfield ORELSE (MATCH_MP_TAC NoSE_Binary THEN CONJ_TAC) ORELSE MATCH_MP_TAC NoSE_LUadrOf ORELSE MATCH_MP_TAC NoSE_Unary)); (*----------------------------------------------------------------------- Prove that an expression has no postevaluation side effects. -----------------------------------------------------------------------*) fun prove_NoPostSE expr = prove((--`NoPostSE ^expr`--), REPEAT (MATCH_ACCEPT_TAC NoPostSE_Const ORELSE MATCH_ACCEPT_TAC NoPostSE_LVvar ORELSE MATCH_MP_TAC NoPostSE_LVarray ORELSE MATCH_MP_TAC NoPostSE_LVderef ORELSE MATCH_MP_TAC NoPostSE_LVfield ORELSE (MATCH_MP_TAC NoPostSE_Assign THEN CONJ_TAC) ORELSE (MATCH_MP_TAC NoPostSE_Binary THEN CONJ_TAC) ORELSE MATCH_MP_TAC NoPostSE_LUadrOf ORELSE MATCH_MP_TAC NoPostSE_LUPreInc ORELSE MATCH_MP_TAC NoPostSE_LUPreDec ORELSE MATCH_MP_TAC NoPostSE_Unary ORELSE MATCH_ACCEPT_TAC NoPostSE_CallNPL ORELSE (MATCH_MP_TAC NoPostSE_CallPL THEN CONJ_TAC))); (*--------------------------------------------------------------------------- Preevaluation side effects ---------------------------------------------------------------------------*) (* this is quite unsafe -- it doesn't do any checking of the "before" and "after" statements. This should only be called from functions which compute the proper relation. *) fun prove_PreEval peTrm = let val [lval,expr,_,stmt] = strip_op (--`PreEval`--) peTrm val npostseThm = prove_NoPostSE expr handle _ => (print_term expr;print "\n"; raise HOL_ERR {origin_structure = "semeqTactics", origin_function = "prove_PreEval", message = "cannot prove that expr doesn't have post-eval side effects"}) val nseThm = prove_NoSE (--`Lval ^lval`--) val stmtOpr = (#1 o strip_comb) stmt val preevalRule = if stmtOpr = (--`Simple`--) then PreEval_simple else if stmtOpr = (--`If`--) then PreEval_if else if stmtOpr = (--`IfElse`--) then PreEval_ifelse else if stmtOpr = (--`Ret`--) then PreEval_ret else (print_term stmt;print "\n"; raise HOL_ERR {origin_structure = "semeqTactics", origin_function = "sep_preeval_expr", message = "stmt must be (Simple e), (If e s), (IfElse e s1 s2), or (Ret e)"}) in MATCH_MP (PART_MATCH (#conseq o dest_imp) preevalRule peTrm) (CONJ npostseThm nseThm) end; local (* for sep_preeval_expr *) (* return a variable (lvalue) which holds the final result of expr, eg, ++b yields b a = 2 * 3 yields a Return NONE if there is no such variable, eg, in c + d. *) fun final_result_var expr = let val (opr,rands) = strip_comb expr in if opr = (--`Assign`--) orelse opr = (--`Lval`--) then SOME (hd rands) else if opr = (--`LUnary`--) then let val theop = hd rands in if theop = (--`PreInc`--) orelse theop = (--`PreDec`--) then SOME (el 2 rands) else NONE end else NONE end; (* tests test_result (case (final_result_var (--`LUnary PreInc (Vref (Var "B" 0 Int))`--)) of SOME a => a | NONE => (--`F`--)) (--`Vref (Var "B" 0 Int)`--); test_result (case (final_result_var (--`Assign (Vref (Var "A" 0 Int)) (Binary (Const (CCint 2) Int) Add (Lval (Vref (Var "B" 0 Int))))`--)) of SOME a => a | NONE => (--`F`--)) (--`Vref (Var "A" 0 Int)`--); test_result (case (final_result_var (--`Binary (Lval (Vref (Var "A" 0 Int))) Add (Lval (Vref (Var "B" 0 Int)))`--)) of SOME a => a | NONE => (--`F`--)) (--`F`--); *) in (* separate a preevaluation expression from a statement, replace the expression with an appropriate lvalue, and return a theorem of the preevaluation equivalence of the pieces and the original code. If a variable name is passed and we need a temporary name, use it. *) fun sep_preeval_expr expr stmt optnewname = if type_of expr <> (==`:CExpr`==) then (print_term expr;print "\n"; raise HOL_ERR {origin_structure = "semeqTactics", origin_function = "sep_preeval_expr", message = "expr must be a :CExpr"}) else if type_of stmt <> (==`:CStmt`==) then (print_term stmt;print "\n"; raise HOL_ERR {origin_structure = "semeqTactics", origin_function = "sep_preeval_expr", message = "stmt must be a :CStmt"}) else (* if we need a new variable to hold the expression result, get it *) let val reslval = case (final_result_var expr) of NONE => let val thename = case (optnewname) of NONE => new_C_Result() | SOME newname => newname in (--`Vref (Var ^(mk_str thename) 0 ^(ctype_of expr))`--) end | SOME finalvar => finalvar val (replaced, stmtWOexpr) = break_out expr reslval stmt in if not replaced then (print "expr is: "; print_term expr; print "\n\nstmt is: "; print_term stmt; print "\n"; raise Fail "expr not found in stmt in sep_preeval_expr") else prove_PreEval (--`PreEval ^reslval ^expr ^stmtWOexpr ^stmt`--) end; (* tests (* remove ++X from ++X; *) test_result (concl (sep_preeval_expr (--`LUnary PreInc (Vref (Var "X" 0 Int))`--) (--`Simple (LUnary PreInc (Vref (Var "X" 0 Int)))`--) NONE)) (--`PreEval (Vref (Var "X" 0 Int)) (LUnary PreInc (Vref (Var "X" 0 Int))) (Simple (Lval (Vref (Var "X" 0 Int)))) (Simple (LUnary PreInc (Vref (Var "X" 0 Int))))`--) handle e=>Raise e; (* remove ++X from ++X; *) test_result (concl (sep_preeval_expr (--`LUnary PreInc (Vref (Var "X" 0 Int))`--) (--`Simple (LUnary PreInc (Vref (Var "X" 0 Int)))`--) (SOME "newvar"))) (--`PreEval (Vref (Var "X" 0 Int)) (LUnary PreInc (Vref (Var "X" 0 Int))) (Simple (Lval (Vref (Var "X" 0 Int)))) (Simple (LUnary PreInc (Vref (Var "X" 0 Int))))`--); (* remove g() from a=g(); *) test_result (concl (sep_preeval_expr (--`Call (Var "g" 0 Int) PLnull`--) (--`Simple (Assign (Vref (Var "a" 0 Int)) (Call (Var "g" 0 Int) PLnull))`--) (SOME "newvar"))) (--`PreEval (Vref (Var "newvar" 0 Int)) (Call (Var "g" 0 Int) PLnull) (Simple (Assign (Vref (Var "a" 0 Int)) (Lval (Vref (Var "newvar" 0 Int))))) (Simple (Assign (Vref (Var "a" 0 Int)) (Call (Var "g" 0 Int) PLnull)))`--); (* remove X+Y from if(X+Y)/*nothing*/; *) test_result (concl (sep_preeval_expr (--`Binary (Lval (Vref (Var "X" 0 Int))) Add (Lval (Vref (Var "Y" 0 Int)))`--) (--`If (Binary (Lval (Vref (Var "X" 0 Int))) Add (Lval (Vref (Var "Y" 0 Int)))) Empty`--) (SOME "C_Resultnnn"))) (--`PreEval (Vref (Var "C_Resultnnn" 0 Int)) (Binary (Lval (Vref (Var "X" 0 Int))) Add (Lval (Vref (Var "Y" 0 Int)))) (If (Lval (Vref (Var "C_Resultnnn" 0 Int))) Empty) (If (Binary (Lval (Vref (Var "X" 0 Int))) Add (Lval (Vref (Var "Y" 0 Int)))) Empty)`--); (* remove X+Y from if(X+Y)/*nothing*/; *) (* this fails since the C_Result chosen won't match *) test_result (concl (sep_preeval_expr (--`Binary (Lval (Vref (Var "X" 0 Int))) Add (Lval (Vref (Var "Y" 0 Int)))`--) (--`If (Binary (Lval (Vref (Var "X" 0 Int))) Add (Lval (Vref (Var "Y" 0 Int)))) Empty`--) NONE)) (--`PreEval (Vref (Var "C_Resultnnn" 0 Int)) (Binary (Lval (Vref (Var "X" 0 Int))) Add (Lval (Vref (Var "Y" 0 Int)))) (If (Lval (Vref (Var "C_Resultnnn" 0 Int))) Empty) (If (Binary (Lval (Vref (Var "X" 0 Int))) Add (Lval (Vref (Var "Y" 0 Int)))) Empty)`--); *) end; (* extract pieces from the PreEval theorem *) fun pre_ext_new_stm pethm = (strip_op (--`PreEval`--) o snd o dest_thm) pethm; (*----------------------------------------------------------------------- Prove that an expression has no preevaluation side effects. -----------------------------------------------------------------------*) fun prove_NoPreSE expr = prove((--`NoPreSE ^expr`--), REPEAT (MATCH_ACCEPT_TAC NoPreSE_Const ORELSE MATCH_ACCEPT_TAC NoPreSE_LVvar ORELSE MATCH_MP_TAC NoPreSE_LVarray ORELSE MATCH_MP_TAC NoPreSE_LVderef ORELSE MATCH_MP_TAC NoPreSE_LVfield ORELSE (MATCH_MP_TAC NoPreSE_Binary THEN CONJ_TAC) ORELSE MATCH_MP_TAC NoPreSE_LUadrOf ORELSE MATCH_MP_TAC NoPreSE_LUPostInc ORELSE MATCH_MP_TAC NoPreSE_LUPostDec ORELSE MATCH_MP_TAC NoPreSE_Unary)); (*--------------------------------------------------------------------------- Postevaluation side effects ---------------------------------------------------------------------------*) (* this is quite unsafe -- it doesn't do any checking of the "before" and "after" statements. This should only be called from functions which compute the proper relation. *) fun prove_PostEval peTrm = let val [_,expr,_] = strip_op (--`PostEval`--) peTrm val npreseThm = prove_NoPreSE expr handle _ => (print_term expr;print "\n"; raise HOL_ERR {origin_structure = "semeqTactics", origin_function = "prove_PostEval", message = "cannot prove that expr doesn't have pre-eval side effects"}) val postevalRule = PostEval_simple in MATCH_MP (PART_MATCH (#conseq o dest_imp) postevalRule peTrm) npreseThm end; (* separate a postevaluation expression from a piece of code, replace the expression with just the lvalue, and return a theorem of the semantic equivalence of the pieces and the original code. *) fun sep_posteval_expr expr stmt = let val reslval = el 2 (strip_op (--`LUnary`--) expr) val (replaced, stmtWOexpr) = break_out expr reslval stmt in if not replaced then (print "expr is: "; print_term expr; print "\n\nstmt is: "; print_term stmt; print "\n"; raise Fail "expr not found in stmt in sep_posteval_expr") else prove_PostEval (--`PostEval ^stmtWOexpr ^expr ^stmt`--) end; (* extract pieces from the PostEval theorem *) fun post_ext_new_stm pethm = (strip_op (--`PostEval`--) o snd o dest_thm) pethm; (* end of $Source: /users/lal/black/hol/Disser/RCS/semeqTactics.sml,v $ *)