diff --git a/thys/CakeML/Tools/cakeml_compiler.ML b/thys/CakeML/Tools/cakeml_compiler.ML --- a/thys/CakeML/Tools/cakeml_compiler.ML +++ b/thys/CakeML/Tools/cakeml_compiler.ML @@ -1,168 +1,168 @@ signature CAKEML_COMPILER = sig datatype mode = Literal (* concrete syntax *) | Prog (* sexp syntax *) val compiler: unit -> Path.T val compile_ml: mode -> string -> Path.T val compile_ml_file: mode -> Path.T -> Path.T val compile_c_file: Path.T -> Path.T val compile_ffi: unit -> Path.T val link: Path.T list -> Path.T val eval: mode -> string -> string val eval_source: mode -> Input.source -> string val string_of_prog: Proof.context -> term -> string val cakeml_cmd: Proof.context -> mode -> Input.source -> unit end structure CakeML_Compiler : CAKEML_COMPILER = struct datatype mode = Literal | Prog fun compiler () = let val platform = getenv_strict "ISABELLE_PLATFORM64" val paths = [getenv_strict "ISABELLE_CAKEML_HOME", "bin", platform, "cake"] val file = Path.appends (map Path.explode paths) in if File.exists file then file else error "CakeML: unsupported platform" end fun basis_ffi () = Path.append (Path.explode (getenv_strict "ISABELLE_CAKEML_HOME")) (Path.basic "basis_ffi.c") fun compile_ml_file mode source = let val id = serial_string () val output = File.tmp_path (Path.basic ("cakeml_out" ^ id ^ ".S")) val sexp = if mode = Literal then "false" else "true" val bash_cake = File.bash_path (compiler ()) val bash_source = File.bash_path source val res = Isabelle_System.bash_process (Bash.script (bash_cake ^ " --sexp=" ^ sexp ^ " < " ^ bash_source)) val err = Process_Result.err res val out = Process_Result.out res val _ = if err <> "" then warning err else () in if not (Process_Result.ok res) orelse err <> "" then error "CakeML: ML compilation failed" else (File.write output out; output) end fun compile_ml mode source = let val id = serial_string () val output = File.tmp_path (Path.basic ("cakeml_in" ^ id)) val _ = File.write output source in compile_ml_file mode output end fun compile_c_file source = let val id = serial_string () val output = File.tmp_path (Path.basic ("c_out" ^ id ^ ".o")) val bash_cc = File.bash_path (Path.explode (getenv_strict "ISABELLE_CC")) val bash_source = File.bash_path source val bash_output = File.bash_path output val res = Isabelle_System.bash_process (Bash.script (bash_cc ^ " -c -o " ^ bash_output ^ " " ^ bash_source)) val err = Process_Result.err res val out = Process_Result.out res val _ = if err <> "" then warning err else () val _ = writeln out in if not (Process_Result.ok res) orelse err <> "" then error "CakeML: C compilation failed" else output end val compile_ffi = compile_c_file o basis_ffi fun link sources = let val id = serial_string () val output = File.tmp_path (Path.basic ("bin" ^ id ^ ".out")) val bash_cc = File.bash_path (Path.explode (getenv_strict "ISABELLE_CC")) val bash_sources = Bash.strings (map File.standard_path sources) val bash_output = File.bash_path output val res = Isabelle_System.bash_process (Bash.script (bash_cc ^ " -o " ^ bash_output ^ " " ^ bash_sources)) val err = Process_Result.err res val out = Process_Result.out res val _ = if err <> "" then warning err else () val _ = writeln out in if not (Process_Result.ok res) orelse err <> "" then error "CakeML: linking failed" else output end fun eval mode source = let val cake = compile_ml mode source val ffi = compile_ffi () val bin = link [cake, ffi] val res = Isabelle_System.bash_process (Bash.script (File.bash_path bin)) val err = Process_Result.err res val out = Process_Result.out res val _ = if err <> "" then warning err else () in if not (Process_Result.ok res) orelse err <> "" then error "CakeML: evaluation failed" else out end fun eval_source mode = eval mode o #1 o Input.source_content fun string_of_prog ctxt t = let val (_, raw_prog) = Thm.cterm_of ctxt t |> Code_Simp.dynamic_conv ctxt |> Thm.prop_of |> Logic.dest_equals in CakeML_Sexp.print_prog raw_prog end val parse_mode = Args.parens (Parse.reserved "literal" >> K Literal || Parse.reserved "prog" >> K Prog) fun cakeml_cmd ctxt mode source = let val source = case mode of Literal => #1 (Input.source_content source) | Prog => Syntax.implode_input source |> Syntax.parse_term ctxt |> Type.constraint @{typ Ast.prog} |> Syntax.check_term ctxt |> string_of_prog ctxt val _ = tracing ("Evaluating: " ^ source) val output = eval mode source in writeln output end val _ = Outer_Syntax.command \<^command_keyword>\cakeml\ "evalute CakeML source" - (parse_mode -- Parse.input Parse.text >> (fn (mode, src) => + (parse_mode -- Parse.embedded_input >> (fn (mode, src) => Toplevel.keep (fn state => cakeml_cmd (Toplevel.context_of state) mode src))) end \ No newline at end of file diff --git a/thys/Isabelle_Meta_Model/isabelle_home/src/Tools/Code/Isabelle_code_target.thy b/thys/Isabelle_Meta_Model/isabelle_home/src/Tools/Code/Isabelle_code_target.thy --- a/thys/Isabelle_Meta_Model/isabelle_home/src/Tools/Code/Isabelle_code_target.thy +++ b/thys/Isabelle_Meta_Model/isabelle_home/src/Tools/Code/Isabelle_code_target.thy @@ -1,214 +1,214 @@ (****************************************************************************** * ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER. * * Copyright (c) 1986-2018 Contributors (in the changeset history) * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) chapter\Part ...\ theory Isabelle_code_target imports Main keywords "attach" and "lazy_code_printing" "apply_code_printing" "apply_code_printing_reflect" :: thy_decl begin subsection\beginning (lazy code printing)\ ML\ structure Isabelle_Code_Target = struct (* Title: Tools/Code/code_target.ML Author: Florian Haftmann, TU Muenchen Generic infrastructure for target language data. *) open Basic_Code_Symbol; open Basic_Code_Thingol; (** checking and parsing of symbols **) val parse_classrel_ident = Parse.class --| @{keyword "<"} -- Parse.class; val parse_inst_ident = Parse.name --| @{keyword "::"} -- Parse.class; (** serializations and serializer **) (* serialization: abstract nonsense to cover different destinies for generated code *) (* serializers: functions producing serializations *) (** theory data **) (** serializer usage **) (* montage *) (* code generation *) fun prep_destination s = ({physical = true}, (Path.explode s, Position.none)); fun export_code_cmd all_public raw_cs seris thy = let val ctxt = Proof_Context.init_global thy; val cs = Code_Thingol.read_const_exprs ctxt raw_cs; in thy |> Named_Target.theory_map (Code_Target.export_code all_public cs ((map o apfst o apsnd o Option.map) prep_destination seris)) end; (** serializer configuration **) (* reserved symbol names *) (* checking of syntax *) (* custom symbol names *) (* custom printings *) (* concrete syntax *) (** Isar setup **) fun parse_single_symbol_pragma parse_keyword parse_isa parse_target = parse_keyword |-- Parse.!!! (parse_isa --| (@{keyword "\"} || @{keyword "=>"}) -- Parse.and_list1 (@{keyword "("} |-- (Parse.name --| @{keyword ")"} -- Scan.option parse_target))); fun parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module = parse_single_symbol_pragma @{keyword "constant"} Parse.term parse_const >> Constant || parse_single_symbol_pragma @{keyword "type_constructor"} Parse.type_const parse_tyco >> Type_Constructor || parse_single_symbol_pragma @{keyword "type_class"} Parse.class parse_class >> Type_Class || parse_single_symbol_pragma @{keyword "class_relation"} parse_classrel_ident parse_classrel >> Class_Relation || parse_single_symbol_pragma @{keyword "class_instance"} parse_inst_ident parse_inst >> Class_Instance || parse_single_symbol_pragma @{keyword "code_module"} Parse.name parse_module >> Code_Symbol.Module; fun parse_symbol_pragmas parse_const parse_tyco parse_class parse_classrel parse_inst parse_module = Parse.enum1 "|" (Parse.group (fn () => "code symbol pragma") (parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module)); end \ ML\ structure Code_printing = struct datatype code_printing = Code_printing of (string * (bstring * Code_Printer.raw_const_syntax option) list, string * (bstring * Code_Printer.tyco_syntax option) list, string * (bstring * string option) list, (string * string) * (bstring * unit option) list, (xstring * string) * (bstring * unit option) list, bstring * (bstring * (string * Code_Symbol.T list) option) list) Code_Symbol.attr list structure Data_code = Theory_Data ( type T = code_printing list Symtab.table val empty = Symtab.empty val merge = Symtab.merge (K true) ) val code_empty = "" val () = Outer_Syntax.command @{command_keyword lazy_code_printing} "declare dedicated printing for code symbols" (Isabelle_Code_Target.parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax) Parse.string (Parse.minus >> K ()) (Parse.minus >> K ()) - (Parse.text -- Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term >> map Code_Symbol.Constant) []) + (Parse.embedded -- Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term >> map Code_Symbol.Constant) []) >> (fn code => Toplevel.theory (Data_code.map (Symtab.map_default (code_empty, []) (fn l => Code_printing code :: l))))) fun apply_code_printing thy = (case Symtab.lookup (Data_code.get thy) code_empty of SOME l => rev l | _ => []) |> (fn l => fold (fn Code_printing l => fold Code_Target.set_printings l) l thy) val () = Outer_Syntax.command @{command_keyword apply_code_printing} "apply dedicated printing for code symbols" (Parse.$$$ "(" -- Parse.$$$ ")" >> K (Toplevel.theory apply_code_printing)) fun reflect_ml source thy = case ML_Context.exec (fn () => ML_Context.eval_source (ML_Compiler.verbose false ML_Compiler.flags) source) (Context.Theory thy) of Context.Theory thy => thy fun apply_code_printing_reflect thy = (case Symtab.lookup (Data_code.get thy) code_empty of SOME l => rev l | _ => []) |> (fn l => fold (fn Code_printing l => fold (fn Code_Symbol.Module (_, l) => fold (fn ("SML", SOME (txt, _)) => reflect_ml (Input.source false txt (Position.none, Position.none)) | _ => I) l | _ => I) l) l thy) val () = Outer_Syntax.command @{command_keyword apply_code_printing_reflect} "apply dedicated printing for code symbols" (Parse.ML_source >> (fn src => Toplevel.theory (apply_code_printing_reflect o reflect_ml src))) end \ end diff --git a/thys/Refine_Imperative_HOL/Lib/Named_Theorems_Rev.thy b/thys/Refine_Imperative_HOL/Lib/Named_Theorems_Rev.thy --- a/thys/Refine_Imperative_HOL/Lib/Named_Theorems_Rev.thy +++ b/thys/Refine_Imperative_HOL/Lib/Named_Theorems_Rev.thy @@ -1,108 +1,108 @@ theory Named_Theorems_Rev imports Main keywords "named_theorems_rev" :: thy_decl begin ML \ signature NAMED_THEOREMS_REV = sig val member: Proof.context -> string -> thm -> bool val get: Proof.context -> string -> thm list val add_thm: string -> thm -> Context.generic -> Context.generic val del_thm: string -> thm -> Context.generic -> Context.generic val add: string -> attribute val del: string -> attribute val check: Proof.context -> string * Position.T -> string val declare: binding -> string -> local_theory -> string * local_theory end; structure Named_Theorems_Rev: NAMED_THEOREMS_REV = struct (* context data *) structure Data = Generic_Data ( type T = thm Item_Net.T Symtab.table; val empty: T = Symtab.empty; val merge : T * T -> T = Symtab.join (K Item_Net.merge); ); fun new_entry name = Data.map (fn data => if Symtab.defined data name then error ("Duplicate declaration of named theorems: " ^ quote name) else Symtab.update (name, Thm.item_net) data); fun undeclared name = "Undeclared named theorems " ^ quote name; fun the_entry context name = (case Symtab.lookup (Data.get context) name of NONE => error (undeclared name) | SOME entry => entry); fun map_entry name f context = (the_entry context name; Data.map (Symtab.map_entry name f) context); (* maintain content *) fun member ctxt = Item_Net.member o the_entry (Context.Proof ctxt); fun content context = Item_Net.content o the_entry context; val get = content o Context.Proof; fun add_thm name = map_entry name o Item_Net.update; fun del_thm name = map_entry name o Item_Net.remove; val add = Thm.declaration_attribute o add_thm; val del = Thm.declaration_attribute o del_thm; (* check *) fun check ctxt (xname, pos) = let val context = Context.Proof ctxt; val fact_ref = Facts.Named ((xname, Position.none), NONE); fun err () = error (undeclared xname ^ Position.here pos); in (case try (Proof_Context.get_fact_generic context) fact_ref of SOME (SOME name, _) => if can (the_entry context) name then name else err () | _ => err ()) end; (* declaration *) fun declare binding descr lthy = let val name = Local_Theory.full_name lthy binding; val description = "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr); val lthy' = lthy |> Local_Theory.background_theory (Context.theory_map (new_entry name)) |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name))) |> Local_Theory.add_thms_dynamic (binding, fn context => content context name) |> Attrib.local_setup binding (Attrib.add_del (add name) (del name)) description in (name, lthy') end; val _ = Outer_Syntax.local_theory @{command_keyword named_theorems_rev} "declare named collection of theorems" - (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >> + (Parse.and_list1 (Parse.binding -- Scan.optional Parse.embedded "") >> fold (fn (b, descr) => snd o declare b descr)); (* ML antiquotation *) val _ = Theory.setup (ML_Antiquotation.inline @{binding named_theorems_rev} (Args.context -- Scan.lift Args.name_position >> (fn (ctxt, name) => ML_Syntax.print_string (check ctxt name)))); end; \ end diff --git a/thys/X86_Semantics/X86_Parse.ML b/thys/X86_Semantics/X86_Parse.ML --- a/thys/X86_Semantics/X86_Parse.ML +++ b/thys/X86_Semantics/X86_Parse.ML @@ -1,356 +1,356 @@ (* TODO: segment registers *) datatype Operand = (* size (in bytes) segment offset base index scale *) Mem of ( int * string option * int * string * string * int) | Reg of string | Imm of LargeInt.int datatype Instr = Instr of (LargeInt.int * LargeInt.int * string * Operand option * Operand option * Operand option) (* PRETTY PRINTING *) fun pp_option NONE = "" | pp_option (SOME s) = s fun pp_mem_size 1 = "BYTE PTR" | pp_mem_size 2 = "WORD PTR" | pp_mem_size 4 = "DWORD PTR" | pp_mem_size 8 = "QWORD PTR" | pp_mem_size 16 = "XMMWORD PTR" | pp_mem_size n = "SIZEDIR " ^ Int.toString (n*8) ^ " PTR" fun pp_operand (Mem (si,segment,offset,base, index, scale)) = pp_mem_size si ^ " " ^ pp_option segment ^ ":[" ^ Int.toString offset ^ " + " ^ base ^ " + " ^ index ^ " * " ^ Int.toString scale ^ "]" | pp_operand (Reg r) = r | pp_operand (Imm i) = Int.toString i fun pp_operands [] = "" | pp_operands (NONE::_) = "" | pp_operands [SOME op1] = pp_operand op1 | pp_operands [SOME op1,NONE] = pp_operand op1 | pp_operands (SOME op1::op2::ops) = pp_operand op1 ^ ", " ^ pp_operands (op2::ops) fun pp_instr (Instr (a,si,m,op1,op2,op3)) = LargeInt.toString a ^ ": " ^ m ^ " " ^ pp_operands [op1,op2,op3] ^ " (" ^ LargeInt.toString si ^ ")" val intFromHexString = StringCvt.scanString (LargeInt.scan StringCvt.HEX) o Substring.string fun intFromHexString_forced s = case intFromHexString s of SOME i => i | NONE => raise Fail ("Could not convert string '" ^ Substring.string s ^ "' to int.") fun is_whitespace c = (c = #" " orelse c = #"\t" orelse c = #"\n") fun trim str = let val (_,x) = Substring.splitl is_whitespace str val (y,_) = Substring.splitr is_whitespace x in y end; (* PARSING *) val registers = [ "rip", "rax", "eax", "ax", "ah", "al", "rbx", "ebx", "bx", "bh", "bl", "rcx", "ecx", "cx", "ch", "cl", "rdx", "edx", "dx", "dh", "dl", "rbp", "ebp", "bp", "bpl", "rsp", "esp", "sp", "spl", "rdi", "edi", "di", "dil", "rsi", "esi", "si", "sil", "r15", "r15d", "r15w", "r15b", "r14", "r14d", "r14w", "r14b", "r13", "r13d", "r13w", "r13b", "r12", "r12d", "r12w", "r12b", "r11", "r11d", "r11w", "r11b", "r10", "r10d", "r10w", "r10b", "r9", "r9d", "r9w", "r9b", "r8", "r8d", "r8w", "r8b", "xmm0","xmm1","xmm2","xmm3","xmm4","xmm5","xmm6","xmm7","xmm8", "xmm9","xmm10","xmm11","xmm12","xmm13","xmm14","xmm15" ] fun is_register str = List.find (fn (str') => String.compare (Substring.string str,str') = EQUAL) registers <> NONE fun overwrite_str "" s = s | overwrite_str s "" = s | overwrite_str _ s = s fun overwrite_str_option NONE s = s | overwrite_str_option s NONE = s | overwrite_str_option _ s = s fun max x y = if x >= y then x else y fun overwrite_Mem (Mem (si,seg,off,base,ind,sc)) (Mem (si',seg',off',base',ind',sc')) = Mem (max si si',overwrite_str_option seg seg',max off off',overwrite_str base base',overwrite_str ind ind',max sc sc') fun parse_operand_address_between_brackets_inner str = if is_register str then Mem (0,NONE,0,Substring.string str,"",0) (* base *) else let val tokens = map trim (Substring.tokens (fn c => c = #"*") str) in if length tokens = 1 then case intFromHexString str of SOME i => Mem (0,NONE,i,"","",0) (* offset *) | NONE => raise Fail ("Don't know how to parse operand part:" ^ Substring.string str) else if length tokens = 2 then if is_register (nth tokens 0) then Mem (0,NONE,0,"",Substring.string (nth tokens 0),intFromHexString_forced (nth tokens 1)) (* index * scale *) else if is_register (nth tokens 1) then Mem (0,NONE,0,"",Substring.string (nth tokens 1),intFromHexString_forced (nth tokens 0)) (* scale * index *) else raise Fail ("Don't know how to parse operand part:" ^ Substring.string str) else raise Fail ("Don't know how to parse operand part:" ^ Substring.string str) end fun parse_operand_address_between_brackets_sum si segment_reg str = let val tokens = map trim (Substring.tokens (fn c => c = #"+") str) in fold (overwrite_Mem o parse_operand_address_between_brackets_inner) tokens (Mem (si,segment_reg ,0,"","",0)) end; fun parse_operand_address_between_brackets_sub si segment_reg str = let val (lhs,num) = Substring.splitl (fn c => c <> #"-") str; val (Mem (x0,x1,_,x3,x4,x5)) = parse_operand_address_between_brackets_sum si segment_reg lhs in Mem (x0,x1,intFromHexString_forced num,x3,x4,x5) end fun parse_operand_address_between_brackets si segment_reg str = let val (_,num) = Substring.splitl (fn c => c <> #"-") str in if Substring.isEmpty num then parse_operand_address_between_brackets_sum si segment_reg str else parse_operand_address_between_brackets_sub si segment_reg str end fun skip_brackets str = let val (x,y) = Substring.splitAt (trim str,1) val (z,_) = Substring.splitl (fn c => c <> #"]") y in if Substring.compare (x,Substring.full "[") = EQUAL then z else raise Fail ("Expecting non-empty bracketed string preceded with colon or an immediate in hex-format, but got: " ^ Substring.string str) end; fun parse_operand_address_bracketed si segment_reg str = case intFromHexString str of SOME imm => Mem (si,segment_reg,imm,"", "",0) | NONE => parse_operand_address_between_brackets si segment_reg (skip_brackets str) fun tail str = case Substring.getc str of NONE => raise Fail ("Expecting non-empty string, but got: " ^ Substring.string str) | SOME (_,s) => s; fun parse_operand_address si str = case Substring.splitl (fn c => c <> #":") str of (before_colon, after_colon) => if Substring.isEmpty after_colon then parse_operand_address_bracketed si NONE before_colon else parse_operand_address_bracketed si (SOME (Substring.string (trim before_colon))) (tail after_colon); fun parse_operand str' = let val str = trim str' in if Substring.isPrefix "BYTE PTR" str then parse_operand_address 1 (snd (Substring.splitAt (str,8))) else if Substring.isPrefix "WORD PTR" str then parse_operand_address 2 (snd (Substring.splitAt (str,8))) else if Substring.isPrefix "DWORD PTR" str then parse_operand_address 4 (snd (Substring.splitAt (str,9))) else if Substring.isPrefix "QWORD PTR" str then parse_operand_address 8 (snd (Substring.splitAt (str,9))) else if Substring.isPrefix "XMMWORD PTR" str then parse_operand_address 16 (snd (Substring.splitAt (str,11))) else if Substring.isPrefix "[" str then (* happens in case of a LEA instruction *) parse_operand_address 0 str else if List.find (fn (str') => String.compare (Substring.string str,str') = EQUAL) registers <> NONE then Reg (Substring.string str) else case intFromHexString str of NONE => raise Fail ("Cannot read hex number in string: " ^ (Substring.string str)) | SOME imm => Imm imm end; fun parse_operands str = let val tokens = map trim (Substring.tokens (fn c => c = #",") (trim str)) val ops = map parse_operand tokens in case ops of [] => (NONE,NONE,NONE) | [op1] => (SOME op1,NONE,NONE) | [op1,op2] => (SOME op1,SOME op2,NONE) | [op1,op2,op3] => (SOME op1,SOME op2,SOME op3) | _ => raise Fail ("Unexpected number of operands in : " ^ Substring.string str) end; fun remove_comment str = let val (str0,str1) = Substring.splitl (fn c => c <> #"#" andalso c <> #"<") str in if Substring.isEmpty str1 then str0 else Substring.trimr 1 str0 end fun parse_external_func a si str = let val (m,func) = Substring.splitl (fn c => c <> #" ") str val func_name = Substring.string (trim func) in Instr (a, si, Substring.string m, SOME (Reg func_name), NONE, NONE) end fun parse_normal_instr a si str = let val (_,rem1) = Substring.splitl (fn c => c = #":" orelse c = #" ") str val (m,rem2) = Substring.splitl (fn c => c <> #" ") rem1 val (op1,op2,op3) = parse_operands rem2 in Instr (a, si, Substring.string m, op1,op2,op3) end; fun parse_instr si str = let val str' = remove_comment (Substring.full str) val (addr,rem0) = Substring.splitl (fn c => c <> #":") str' val a = intFromHexString_forced (Substring.full ("0x" ^ Substring.string (trim addr))) in if Substring.isPrefix "EXTERNAL_FUNCTION" (trim (tail (rem0))) then parse_external_func a si (trim (tail (rem0))) else parse_normal_instr a si rem0 end; fun read_instr_addr str = let val instr = parse_instr 0 str val (Instr (a,_,_,_,_,_)) = instr in a end (* EMBEDDING INTO HOL *) val mk_nat = HOLogic.mk_number @{typ nat} val mk_string = HOLogic.mk_string fun mk_word_typ_from_num s = Syntax.read_typ @{context} ("num \ " ^ Int.toString s ^ " word") fun mk_word_typ s = Syntax.read_typ @{context} (Int.toString s ^ " word") fun mk_word i b = if i=0 then Const ("Groups.zero_class.zero", mk_word_typ b) else if i=1 then Const ("Groups.one_class.one", mk_word_typ b) else if i < 0 then Syntax.read_term @{context} ("uminus :: " ^ Int.toString b ^ " word \ " ^ Int.toString b ^ " word") $ (Const ("Num.numeral_class.numeral", mk_word_typ_from_num b) $ HOLogic.mk_numeral (0 - i)) else Const ("Num.numeral_class.numeral", mk_word_typ_from_num b) $ HOLogic.mk_numeral i fun mk_operand (Mem (8,segment,offset,base,index,scale)) = @{term "qword_ptr"} $ HOLogic.mk_prod (mk_word offset 64, HOLogic.mk_prod (mk_string base, HOLogic.mk_prod (mk_string index, mk_nat scale))) | mk_operand (Mem (4,segment,offset,base,index,scale)) = @{term "dword_ptr"} $ HOLogic.mk_prod (mk_word offset 64, HOLogic.mk_prod (mk_string base, HOLogic.mk_prod (mk_string index, mk_nat scale))) | mk_operand (Mem (2,segment,offset,base,index,scale)) = @{term "word_ptr"} $ HOLogic.mk_prod (mk_word offset 64, HOLogic.mk_prod (mk_string base, HOLogic.mk_prod (mk_string index, mk_nat scale))) | mk_operand (Mem (1,segment,offset,base,index,scale)) = @{term "byte_ptr"} $ HOLogic.mk_prod (mk_word offset 64, HOLogic.mk_prod (mk_string base, HOLogic.mk_prod (mk_string index, mk_nat scale))) | mk_operand (Mem (si,segment,offset,base,index,scale)) = @{term Mem} $ mk_nat si $ mk_word offset 64 $ mk_string base $ mk_string index $ mk_nat scale | mk_operand (Reg reg) = @{term Reg} $ mk_string reg | mk_operand (Imm imm) = @{term Imm} $ mk_word imm 256 fun mk_operand_option NONE = @{term "None :: Operand option"} | mk_operand_option (SOME op1) = @{term "Some :: Operand \ Operand option"} $ mk_operand op1 fun mk_instr (Instr (_,_,"EXTERNAL_FUNCTION",SOME (Reg f),NONE,NONE)) lthy = let val def = Syntax.read_term (Local_Theory.target_of lthy) ("EXTERNAL_FUNCTION_" ^ f) in if fastype_of def = (@{typ state} --> @{typ state}) then @{term ExternalFunc} $ def else raise Fail ("Unknown external function: " ^ f ^ "; expecting a function named EXTERNAL_FUNCTION_" ^ f ^ " in locale unknowns of type state \ state") end | mk_instr (Instr (a,si,m,op1,op2,op3)) _ = @{term Instr} $ mk_string m $ mk_operand_option op1 $ mk_operand_option op2 $ mk_operand_option op3 $ mk_word (a+si) 64 (* Make a definition in HOL with name "name" and as body "value". Value can be any HOL term, e.g.,: HOLogic.mk_number @{typ nat} 42 Note that HOL terms can be produced using antiquotations, e.g., @{term "42::nat"} does the same as the above code. *) fun mk_definition name value lthy = let val binding = Binding.name name val (_, lthy) = Local_Theory.define ((binding, NoSyn), ((Thm.def_binding binding, []), value)) lthy val _ = tracing ("Added definition: " ^ (Local_Theory.full_name lthy binding)) in lthy end fun main localename assembly lthy = let (* Build a locale name *) val _ = not (Long_Name.is_qualified localename) orelse raise Fail ("Given localename looks like qualified Isabelle ID: " ^ localename) val _ = localename <> "" orelse raise Fail ("Given localename is illegal") (* The locale fixes a variable called "fetch" of type "64 word \ I" *) val fixes_fetch = Element.Fixes [( Binding.name "fetch" , SOME (@{typ "64 word => I"}), NoSyn)] (* the locale contains a list of assumptions, one for each instruction. They are given the [simp] attribute. *) val simp_attrib = Attrib.internal (fn (_) => Simplifier.simp_add) fun mk_assume thm_name term = ((Binding.name thm_name, [simp_attrib]), [term]); val mk_fetch = Free ("fetch", @{typ "64 word => I"}) fun mk_fetch_equality_assume si str = let val instr = parse_instr si str val (Instr (a,_,_,_,_,_)) = instr val asm_name = "fetch_" ^ LargeInt.toString a val eq_term = HOLogic.mk_eq (mk_fetch $ mk_word a 64, mk_instr instr lthy) in mk_assume asm_name (HOLogic.Trueprop $ eq_term, []) end fun mk_fetch_equality_assumes [] = [] | mk_fetch_equality_assumes [str] = [mk_fetch_equality_assume 1 str] | mk_fetch_equality_assumes (str0::str1::strs) = (mk_fetch_equality_assume (read_instr_addr str1 - read_instr_addr str0) str0) :: mk_fetch_equality_assumes (str1::strs) val assembly = String.tokens (fn c => c = #"\n") assembly |> List.filter (Substring.full #> remove_comment #> Substring.explode #> List.all Char.isSpace #> not) val loc_bindings = Binding.name localename val loc_elems = [fixes_fetch,Element.Assumes (mk_fetch_equality_assumes assembly)] val thy = Local_Theory.exit_global lthy val loc_expr : (string, term) Expression.expr = [(Locale.intern thy "unknowns",(("",false),(Expression.Named [], [])))] val (_,lthy) = Expression.add_locale loc_bindings loc_bindings [] (loc_expr,[]) loc_elems thy val _ = tracing ("Added locale: " ^ localename ^ " with a fetch function for " ^ Int.toString (length assembly) ^ " instructions. To get started, execute:\n\ncontext " ^ localename ^ "\nbegin\n find_theorems fetch\nend\n") in lthy end (* Add the command "x86_64_parser" to the Isabelle syntax. - Its argument is parsed by Parse.text, which simply returns - the text. The parsed text is given to the "main" function. + Its argument is parsed by Parse.embedded, which simply returns + the embedded source. The parsed text is given to the "main" function. *) val _ = Outer_Syntax.local_theory \<^command_keyword>\x86_64_parser\ "Generate a locale from a list of assembly instructions." - (Parse.text -- Parse.text >> (fn (localename, assembly) => main localename assembly)) + (Parse.embedded -- Parse.embedded >> (fn (localename, assembly) => main localename assembly))