diff --git a/Root.ML b/Root.ML index 5b3dcee2..a45c23e4 100644 --- a/Root.ML +++ b/Root.ML @@ -1,138 +1,139 @@ (* Copyright (c) 2009, 2010, 2015-16 David C. J. Matthews This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License version 2.1 as published by the Free Software Foundation. This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with this library; if not, write to the Free Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA *) (* Compiler root file. This gives the "use" instructions necessary to build the compiler and suitable for use with an IDE project file. It was constructed from the Poly/ML make files. *) PolyML.print_depth 1; PolyML.Compiler.reportUnreferencedIds := true; use "basis/RuntimeCalls.ML"; use "mlsource/MLCompiler/Address.ML"; use "mlsource/MLCompiler/Misc.ML"; use "mlsource/MLCompiler/HashTable.ML"; use "mlsource/MLCompiler/UniversalTable.ML"; +use "mlsource/MLCompiler/StronglyConnected.sml"; use "mlsource/MLCompiler/StretchArray.ML"; use "mlsource/MLCompiler/STRUCTVALSIG.sml"; use "mlsource/MLCompiler/PRETTYSIG.sml"; use "mlsource/MLCompiler/LEXSIG.sml"; use "mlsource/MLCompiler/SymbolsSig.sml"; use "mlsource/MLCompiler/COMPILERBODYSIG.sml"; use "mlsource/MLCompiler/DEBUGSIG.ML"; use "mlsource/MLCompiler/MAKESIG.sml"; use "mlsource/MLCompiler/MAKE_.ML"; use "mlsource/MLCompiler/FOREIGNCALLSIG.sml"; use "mlsource/MLCompiler/BUILTINS.sml"; use "mlsource/MLCompiler/CODETREESIG.ML"; use "mlsource/MLCompiler/STRUCT_VALS.ML"; use "mlsource/MLCompiler/CodeTree/BackendIntermediateCodeSig.sml"; use "mlsource/MLCompiler/CodeTree/BaseCodeTreeSig.sml"; use "mlsource/MLCompiler/CodeTree/CodetreeFunctionsSig.sml"; use "mlsource/MLCompiler/CodeTree/CodegenTreeSig.sml"; use "mlsource/MLCompiler/Codetree/GENCODESIG.sml"; use "mlsource/MLCompiler/CodeTree/CODETREE_FUNCTIONS.sml"; use "mlsource/MLCompiler/CodeTree/CODETREE_STATIC_LINK_AND_CASES.sml"; use "mlsource/MLCompiler/CodeTree/CODETREE_CODEGEN_CONSTANT_FUNCTIONS.sml"; use "mlsource/MLCompiler/CodeTree/CODETREE_LAMBDA_LIFT.sml"; use "mlsource/MLCompiler/CodeTree/CODETREE_REMOVE_REDUNDANT.sml"; use "mlsource/MLCompiler/CodeTree/CODETREE_SIMPLIFIER.sml"; use "mlsource/MLCompiler/CodeTree/CODETREE_OPTIMISER.sml"; use "mlsource/MLCompiler/CodeTree/CODETREE.ML"; use "mlsource/MLCompiler/Pretty.sml"; use "mlsource/MLCompiler/CodeTree/CODE_ARRAY.ML"; use "mlsource/MLCompiler/CodeTree/X86Code/X86CODESIG.sml"; use "mlsource/MLCompiler/CodeTree/X86Code/ICodeSig.ML"; use "mlsource/MLCompiler/CodeTree/X86Code/X86ICODETRANSFORMSIG.ML"; use "mlsource/MLCompiler/CodeTree/X86Code/X86IDENTIFYREFSSIG.ML"; use "mlsource/MLCompiler/CodeTree/X86Code/X86ICodeToX86Code.ML"; use "mlsource/MLCompiler/CodeTree/X86Code/X86ICodeTransform.ML"; use "mlsource/MLCompiler/CodeTree/X86Code/X86ICodeIdentifyReferences.ML"; use "mlsource/MLCompiler/CodeTree/X86Code/X86CodetreeToICode.ML"; use "mlsource/MLCompiler/CodeTree/X86Code/X86OUTPUTCODE.ML"; use "mlsource/MLCompiler/CodeTree/X86Code/X86OPTIMISE.ML"; use "mlsource/MLCompiler/Debug.ML"; use "mlsource/MLCompiler/CodeTree/X86Code/X86FOREIGNCALL.sml"; use "mlsource/MLCompiler/CodeTree/BackendIntermediateCode.sml"; use "mlsource/MLCompiler/CodeTree/BaseCodeTree.sml"; use "mlsource/MLCompiler/CodeTree/X86Code/ml_bind.ML"; use "mlsource/MLCompiler/CodeTree/GCode.i386.ML"; use "mlsource/MLCompiler/CodeTree/ml_bind.ML"; use "mlsource/MLCompiler/StructVals.ML"; use "mlsource/MLCompiler/LEX_.ML"; use "mlsource/MLCompiler/Symbols.ML"; use "mlsource/MLCompiler/Lex.ML"; use "mlsource/MLCompiler/SymsetSig.sml"; use "mlsource/MLCompiler/DATATYPEREPSIG.sml"; use "mlsource/MLCompiler/VALUEOPSSIG.sml"; use "mlsource/MLCompiler/EXPORTTREESIG.sml"; use "mlsource/MLCompiler/STRUCTURESSIG.sml"; use "mlsource/MLCompiler/COMPILER_BODY.ML"; use "mlsource/MLCompiler/SymSet.ML"; use "mlsource/MLCompiler/TYPETREESIG.sml"; use "mlsource/MLCompiler/COPIERSIG.sml"; use "mlsource/MLCompiler/TYPEIDCODESIG.sml"; use "mlsource/MLCompiler/DATATYPE_REP.ML"; use "mlsource/MLCompiler/PRINTTABLESIG.sml"; use "mlsource/MLCompiler/VALUE_OPS.ML"; use "mlsource/MLCompiler/TYPE_TREE.ML"; use "mlsource/MLCompiler/UTILITIES_.ML"; use "mlsource/MLCompiler/Utilities.ML"; use "mlsource/MLCompiler/PRINT_TABLE.ML"; use "mlsource/MLCompiler/PrintTable.ML"; use "mlsource/MLCompiler/ExportTree.sml"; use "mlsource/MLCompiler/ExportTreeStruct.sml"; use "mlsource/MLCompiler/TypeTree.ML"; use "mlsource/MLCompiler/COPIER.sml"; use "mlsource/MLCompiler/CopierStruct.sml"; use "mlsource/MLCompiler/TYPEIDCODE.sml"; use "mlsource/MLCompiler/TypeIDCodeStruct.sml"; use "mlsource/MLCompiler/DatatypeRep.ML"; use "mlsource/MLCompiler/ValueOps.ML"; use "mlsource/MLCompiler/PARSETREESIG.sml"; use "mlsource/MLCompiler/SIGNATURESSIG.sml"; use "mlsource/MLCompiler/DEBUGGERSIG.sml"; use "mlsource/MLCompiler/STRUCTURES_.ML"; use "mlsource/MLCompiler/DEBUGGER_.sml"; use "mlsource/MLCompiler/Debugger.sml"; use "mlsource/MLCompiler/ParseTree/BaseParseTreeSig.sml"; use "mlsource/MLCompiler/ParseTree/BASE_PARSE_TREE.sml"; use "mlsource/MLCompiler/ParseTree/PrintParsetreeSig.sml"; use "mlsource/MLCompiler/ParseTree/PRINT_PARSETREE.sml"; use "mlsource/MLCompiler/ParseTree/ExportParsetreeSig.sml"; use "mlsource/MLCompiler/ParseTree/EXPORT_PARSETREE.sml"; use "mlsource/MLCompiler/ParseTree/TypeCheckParsetreeSig.sml"; use "mlsource/MLCompiler/ParseTree/TYPECHECK_PARSETREE.sml"; use "mlsource/MLCompiler/ParseTree/MatchCompilerSig.sml"; use "mlsource/MLCompiler/ParseTree/MATCH_COMPILER.sml"; use "mlsource/MLCompiler/ParseTree/CodegenParsetreeSig.sml"; use "mlsource/MLCompiler/ParseTree/CODEGEN_PARSETREE.sml"; use "mlsource/MLCompiler/ParseTree/PARSE_TREE.ML"; use "mlsource/MLCompiler/ParseTree/ml_bind.ML"; use "mlsource/MLCompiler/SIGNATURES.sml"; use "mlsource/MLCompiler/SignaturesStruct.sml"; use "mlsource/MLCompiler/Structures.ML"; use "mlsource/MLCompiler/PARSE_DEC.ML"; use "mlsource/MLCompiler/SKIPS_.ML"; use "mlsource/MLCompiler/Skips.ML"; use "mlsource/MLCompiler/PARSE_TYPE.ML"; use "mlsource/MLCompiler/ParseType.ML"; use "mlsource/MLCompiler/ParseDec.ML"; use "mlsource/MLCompiler/CompilerBody.ML"; use "mlsource/MLCompiler/CompilerVersion.sml"; use "mlsource/MLCompiler/Make.ML"; use "mlsource/MLCompiler/INITIALISE_.ML"; use "mlsource/MLCompiler/Initialise.ML"; use "mlsource/MLCompiler/ml_bind.ML"; diff --git a/mlsource/MLCompiler/CodeTree/CODETREE_FUNCTIONS.sml b/mlsource/MLCompiler/CodeTree/CODETREE_FUNCTIONS.sml index f48a4554..9f2880b2 100644 --- a/mlsource/MLCompiler/CodeTree/CODETREE_FUNCTIONS.sml +++ b/mlsource/MLCompiler/CodeTree/CODETREE_FUNCTIONS.sml @@ -1,538 +1,470 @@ (* Copyright (c) 2012,13,16 David C.J. Matthews This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License version 2.1 as published by the Free Software Foundation. This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with this library; if not, write to the Free Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA *) (* Miscellaneous construction and operation functions on the code-tree. *) functor CODETREE_FUNCTIONS( structure BASECODETREE: BaseCodeTreeSig + structure STRONGLY: sig type node val stronglyConnectedComponents: node list -> node list list end + where type node = { addr: int, lambda: BASECODETREE.lambdaForm, use: BASECODETREE.codeUse list } ) : CodetreeFunctionsSig = struct open BASECODETREE + open STRONGLY open Address exception InternalError = Misc.InternalError fun mkEnv([], exp) = exp | mkEnv(decs, exp) = Newenv(decs, exp) val word0 = toMachineWord 0 and word1 = toMachineWord 1 val False = word0 and True = word1 val F_mutable_words : Word8.word = Word8.orb (F_words, F_mutable) val CodeFalse = Constnt(False, []) and CodeTrue = Constnt(True, []) and CodeZero = Constnt(word0, []) (* Properties of code. This indicates the extent to which the code has side-effects (i.e. where even if the result is unused the code still needs to be produced) or is applicative (i.e. where its value depends only arguments and can safely be reordered). *) (* The RTS has a table of properties for RTS functions. The 103 call returns these Or-ed into the register mask. *) val PROPWORD_NORAISE = 0wx40000000 and PROPWORD_NOUPDATE = 0wx20000000 and PROPWORD_NODEREF = 0wx10000000 (* Since RTS calls are being eliminated leave residual versions of these. *) fun earlyRtsCall _ = false and sideEffectFreeRTSCall _ = false local infix orb andb val op orb = Word.orb and op andb = Word.andb val noSideEffect = PROPWORD_NORAISE orb PROPWORD_NOUPDATE val applicative = noSideEffect orb PROPWORD_NODEREF in fun codeProps (Lambda _) = applicative | codeProps (Constnt _) = applicative | codeProps (Extract _) = applicative | codeProps (TagTest{ test, ... }) = codeProps test | codeProps (Cond(i, t, e)) = codeProps i andb codeProps t andb codeProps e | codeProps (Newenv(decs, exp)) = List.foldl (fn (d, r) => bindingProps d andb r) (codeProps exp) decs | codeProps (Handle { exp, handler, ... }) = (* A handler processes all the exceptions in the body *) (codeProps exp orb PROPWORD_NORAISE) andb codeProps handler | codeProps (Tuple { fields, ...}) = testList fields | codeProps (Indirect{base, ...}) = codeProps base (* A built-in function may be side-effect free. This can occur if we have, for example, "if exp1 orelse exp2" where exp2 can be reduced to "true", typically because it's inside an inline function and some of the arguments to the function are constants. This then gets converted to (exp1; true) and we can eliminate exp1 if it is simply a comparison. *) | codeProps GetThreadId = Word.orb(PROPWORD_NOUPDATE, PROPWORD_NORAISE) | codeProps (Unary{oper, arg1}) = let open BuiltIns val operProps = case oper of NotBoolean => applicative | IsTaggedValue => applicative | MemoryCellLength => applicative (* MemoryCellFlags could return a different result if a mutable cell was locked. *) | MemoryCellFlags => applicative | ClearMutableFlag => Word.orb(PROPWORD_NODEREF, PROPWORD_NORAISE) | StringLengthWord => applicative | AtomicIncrement => PROPWORD_NORAISE | AtomicDecrement => PROPWORD_NORAISE | AtomicReset => Word.orb(PROPWORD_NODEREF, PROPWORD_NORAISE) | LongWordToTagged => applicative | SignedToLongWord => applicative | UnsignedToLongWord => applicative | RealAbs => applicative (* Does not depend on rounding setting. *) | RealNeg => applicative (* Does not depend on rounding setting. *) (* If we float a 64-bit int to a 64-bit floating point value we may lose precision so this depends on the current rounding mode. *) | FloatFixedInt => Word.orb(PROPWORD_NOUPDATE, PROPWORD_NORAISE) in operProps andb codeProps arg1 end | codeProps (Binary{oper, arg1, arg2}) = let open BuiltIns val mayRaise = PROPWORD_NOUPDATE orb PROPWORD_NODEREF val operProps = case oper of WordComparison _ => applicative | FixedPrecisionArith _ => mayRaise | WordArith _ => applicative (* Quot and Rem don't raise exceptions - zero checking is done before. *) | SetStringLengthWord => Word.orb(PROPWORD_NODEREF, PROPWORD_NORAISE) | WordLogical _ => applicative | WordShift _ => applicative | AllocateByteMemory => Word.orb(PROPWORD_NOUPDATE, PROPWORD_NORAISE) (* Allocation returns a different value on each call. *) | LargeWordComparison _ => applicative | LargeWordArith _ => applicative (* Quot and Rem don't raise exceptions - zero checking is done before. *) | LargeWordLogical _ => applicative | LargeWordShift _ => applicative | RealComparison _ => applicative (* Real arithmetic operations depend on the current rounding setting. *) | RealArith _ => Word.orb(PROPWORD_NOUPDATE, PROPWORD_NORAISE) in operProps andb codeProps arg1 andb codeProps arg2 end | codeProps (AllocateWordMemory {numWords, flags, initial}) = let val operProps = Word.orb(PROPWORD_NOUPDATE, PROPWORD_NORAISE) in operProps andb codeProps numWords andb codeProps flags andb codeProps initial end | codeProps (Eval _) = 0w0 | codeProps(Raise exp) = codeProps exp andb (Word.notb PROPWORD_NORAISE) (* Treat these as unsafe at least for the moment. *) | codeProps(BeginLoop _) = 0w0 | codeProps(Loop _) = 0w0 | codeProps (SetContainer _) = 0w0 | codeProps (LoadOperation {address, kind}) = let val operProps = case kind of LoadStoreMLWord {isImmutable=true} => applicative | LoadStoreMLByte {isImmutable=true} => applicative | _ => Word.orb(PROPWORD_NOUPDATE, PROPWORD_NORAISE) in operProps andb addressProps address end | codeProps (StoreOperation {address, value, ...}) = Word.orb(PROPWORD_NODEREF, PROPWORD_NORAISE) andb addressProps address andb codeProps value | codeProps (BlockOperation {kind, sourceLeft, destRight, length}) = let val operProps = case kind of BlockOpMove _ => PROPWORD_NORAISE | BlockOpEqualByte => applicative | BlockOpCompareByte => applicative in operProps andb addressProps sourceLeft andb addressProps destRight andb codeProps length end and testList t = List.foldl(fn (c, r) => codeProps c andb r) applicative t and bindingProps(Declar{value, ...}) = codeProps value | bindingProps(RecDecs _) = applicative (* These should all be lambdas *) | bindingProps(NullBinding c) = codeProps c | bindingProps(Container{setter, ...}) = codeProps setter and addressProps{base, index=NONE, ...} = codeProps base | addressProps{base, index=SOME index, ...} = codeProps base andb codeProps index (* sideEffectFree - does not raise an exception or make an assignment. *) fun sideEffectFree c = (codeProps c andb noSideEffect) = noSideEffect (* reorderable - does not raise an exception or access a reference. *) and reorderable c = codeProps c = applicative end (* Return the inline property if it is set. *) fun findInline [] = EnvSpecNone | findInline (h::t) = if Universal.tagIs CodeTags.inlineCodeTag h then Universal.tagProject CodeTags.inlineCodeTag h else findInline t (* Makes a constant value from an expression which is known to be constant but may involve inline functions, tuples etc. *) fun makeConstVal (cVal:codetree) = let fun makeVal (c as Constnt _) = c (* should just be a tuple *) (* Get a vector, copy the entries into it and return it as a constant. *) | makeVal (Tuple {fields= [], ...}) = CodeZero (* should have been optimised already! *) | makeVal (Tuple {fields, ...}) = let val tupleSize = List.length fields val vec : address = allocWordData(Word.fromInt tupleSize, F_mutable_words, word0) val fieldCode = map makeVal fields fun copyToVec ([], _) = [] | copyToVec (Constnt(w, prop) :: t, locn) = ( assignWord (vec, locn, w); prop :: copyToVec (t, locn + 0w1) ) | copyToVec _ = raise InternalError "not constant" val props = copyToVec(fieldCode, 0w0) (* If any of the constants have properties create a tuple property for the result. *) val tupleProps = if List.all null props then [] else let (* We also need to construct an EnvSpecTuple property because findInline does not look at tuple properties. *) val inlineProps = map findInline props val inlineProp = if List.all (fn EnvSpecNone => true | _ => false) inlineProps then [] else let fun tupleEntry n = (EnvGenConst(loadWord(vec, Word.fromInt n), List.nth(props, n)), List.nth(inlineProps, n)) in [Universal.tagInject CodeTags.inlineCodeTag (EnvSpecTuple(tupleSize, tupleEntry))] end in Universal.tagInject CodeTags.tupleTag props :: inlineProp end in lock vec; Constnt(toMachineWord vec, tupleProps) end | makeVal _ = raise InternalError "makeVal - not constant or tuple" in makeVal cVal end local fun allConsts [] = true | allConsts (Constnt _ :: t) = allConsts t | allConsts _ = false fun mkRecord isVar xp = let val tuple = Tuple{fields = xp, isVariant = isVar } in if allConsts xp then (* Make it now. *) makeConstVal tuple else tuple end; in val mkTuple = mkRecord false and mkDatatype = mkRecord true end (* Set the inline property. If the property is already present it is replaced. If the property we are setting is EnvSpecNone no property is set. *) fun setInline p (h::t) = if Universal.tagIs CodeTags.inlineCodeTag h then setInline p t else h :: setInline p t | setInline EnvSpecNone [] = [] | setInline p [] = [Universal.tagInject CodeTags.inlineCodeTag p] (* These are very frequently used and it might be worth making special bindings for values such as 0, 1, 2, 3 etc to reduce garbage. *) fun checkNonZero n = if n < 0 then raise InternalError "mkLoadxx: argument negative" else n val mkLoadLocal = Extract o LoadLocal o checkNonZero and mkLoadArgument = Extract o LoadArgument o checkNonZero and mkLoadClosure = Extract o LoadClosure o checkNonZero (* Set the container to the fields of the record. Try to push this down as far as possible. *) fun mkSetContainer(container, Cond(ifpt, thenpt, elsept), filter) = Cond(ifpt, mkSetContainer(container, thenpt, filter), mkSetContainer(container, elsept, filter)) | mkSetContainer(container, Newenv(decs, exp), filter) = Newenv(decs, mkSetContainer(container, exp, filter)) | mkSetContainer(_, r as Raise _, _) = r (* We may well have the situation where one branch of an "if" raises an exception. We can simply raise the exception on that branch. *) | mkSetContainer(container, Handle {exp, handler, exPacketAddr}, filter) = Handle{exp=mkSetContainer(container, exp, filter), handler=mkSetContainer(container, handler, filter), exPacketAddr = exPacketAddr} | mkSetContainer(container, tuple, filter) = SetContainer{container = container, tuple = tuple, filter = filter } local val except: exn = InternalError "Invalid load encountered in compiler" (* Exception value to use for invalid cases. We put this in the code but it should never actually be executed. *) val raiseError = Raise (Constnt (toMachineWord except, [])) in (* Look for an entry in a tuple. Used in both the optimiser and in mkInd. *) fun findEntryInBlock (Tuple { fields, isVariant, ...}, offset, isVar) = ( isVariant = isVar orelse raise InternalError "findEntryInBlock: tuple/datatype mismatch"; if offset < List.length fields then List.nth(fields, offset) (* This can arise if we're processing a branch of a case discriminating on a datatype which won't actually match at run-time. e.g. Tests/Succeed/Test030. *) else if isVar then raiseError else raise InternalError "findEntryInBlock: invalid address" ) | findEntryInBlock (Constnt (b, props), offset, isVar) = let (* Find the tuple property if it is present and extract the field props. *) val fieldProps = case List.find(Universal.tagIs CodeTags.tupleTag) props of NONE => [] | SOME p => List.nth(Universal.tagProject CodeTags.tupleTag p, offset) in case findInline props of EnvSpecTuple(_, env) => (* Do the selection now. This is especially useful if we have a global structure *) (* At the moment at least we assume that we can get all the properties from the tuple selection. *) ( case env offset of (EnvGenConst(w, p), inl) => Constnt(w, setInline inl p) (* The general value from selecting a field from a constant tuple must be a constant. *) | _ => raise InternalError "findEntryInBlock: not constant" ) | _ => (* The ML compiler may generate loads from invalid addresses as a result of a val binding to a constant which has the wrong shape. e.g. val a :: b = nil It will always result in a Bind exception being generated before the invalid load, but we have to be careful that the optimiser does not fall over. *) if isShort b orelse not (Address.isWords (toAddress b)) orelse Address.length (toAddress b) <= Word.fromInt offset then if isVar then raiseError else raise InternalError "findEntryInBlock: invalid address" else Constnt (loadWord (toAddress b, Word.fromInt offset), fieldProps) end | findEntryInBlock(base, offset, isVar) = Indirect {base = base, offset = offset, isVariant = isVar} (* anything else *) end (* Exported indirect load operation i.e. load a field from a tuple. We can't use findEntryInBlock in every case since that discards unused entries in a tuple and at this point we haven't checked that the unused entries don't have side-effects/raise exceptions e.g. #1 (1, raise Fail "bad") *) local fun mkIndirect isVar (addr, base as Constnt _) = findEntryInBlock(base, addr, isVar) | mkIndirect isVar (addr, base) = Indirect {base = base, offset = addr, isVariant = isVar} in val mkInd = mkIndirect false and mkVarField = mkIndirect true end (* Create a tuple from a container. *) fun mkTupleFromContainer(addr, size) = Tuple{fields = List.tabulate(size, fn n => mkInd(n, mkLoadLocal addr)), isVariant = false} (* Get the value from the code. *) fun evalue (Constnt(c, _)) = SOME c | evalue _ = NONE (* This is really to simplify the change from mkEnv taking a codetree list to taking a codeBinding list * code. This extracts the last entry which must be a NullBinding and packages the declarations with it. *) fun decSequenceWithFinalExp decs = let fun splitLast _ [] = raise InternalError "decSequenceWithFinalExp: empty" | splitLast decs [NullBinding exp] = (List.rev decs, exp) | splitLast _ [_] = raise InternalError "decSequenceWithFinalExp: last is not a NullDec" | splitLast decs (hd::tl) = splitLast (hd:: decs) tl in mkEnv(splitLast [] decs) end - fun partitionMutableBindings(RecDecs rlist) = (* In general any mutually recursive declaration can refer to any other. It's better to partition the recursive declarations into strongly connected components i.e. those that actually refer to each other. *) - let - local - val anAddr = #addr (hd rlist) (* Must be at least one *) - in - val (startAddress, lastAddress) = - List.foldl (fn({addr, ...}, (mn, mx)) => (Int.min(addr, mn), Int.max(addr+1, mx))) (anAddr, anAddr) rlist - end - (* *) - val mapArray = Array.array(lastAddress - startAddress, NONE) - - fun updateMin(addr, try) = - let - val off = addr - startAddress - val { lowLink, index } = valOf(Array.sub(mapArray, off)) - in - Array.update(mapArray, off, SOME{ index = index, lowLink = Int.min(lowLink, try) }) - end - - fun addrInList a = List.exists(fn{addr, ...} => a = addr) - - fun strongcomponent(item as {addr, lambda = { closure, ...}, ...}, (thisIndex, stack, resList)) = + fun partitionMutableBindings(RecDecs rlist) = let - val newStack = item :: stack - val v = addr - startAddress - (* Mark this item as processed. *) - val () = Array.update(mapArray, v, SOME{index = thisIndex, lowLink = thisIndex}) - - (* Process links that refer to other items *) - fun processLink(LoadLocal a, args as (_, stack, _)) = - if addrInList a rlist - then (* It refers to another within this declaration *) - let - val w = a - startAddress - in - case Array.sub(mapArray, w) of - NONE => (* Not yet processed. *) - let - val result = strongcomponent(valOf(List.find(fn {addr, ...} => addr = a) rlist), args); - in - updateMin(addr, #lowLink(valOf(Array.sub(mapArray, w)))); - result - end - | SOME _ => - ( - (* Already processed - was it in this pass or a previous? *) - if addrInList a stack (* On the stack so in the current SCC *) - then updateMin(addr, #index(valOf(Array.sub(mapArray, w)))) - else (); (* Processed in previous pass *) - args - ) - end - else args - | processLink (_, args) = args - - val (nextIndex, stack', subRes) = List.foldl processLink (thisIndex+1, newStack, resList) closure + val processed = stronglyConnectedComponents rlist + (* Convert the result. Note that stronglyConnectedComponents returns the + dependencies in the reverse order i.e. if X depends on Y but not the other + way round then X will appear before Y in the list. We need to reverse + it so that X goes after Y. *) + fun rebuild ([], _) = raise InternalError "partitionMutableBindings" (* Should not happen *) + | rebuild ([{addr, lambda, use}], tl) = Declar{addr=addr, use=use, value=Lambda lambda} :: tl + | rebuild (multiple, tl) = RecDecs multiple :: tl in - (* Process references from this function. *) - if #lowLink(valOf(Array.sub(mapArray, v))) = thisIndex (* This is the minimum *) - then (* Create an SCC *) - let - fun popItems([], _) = raise InternalError "stack empty" - | popItems((item as {addr=a, ...}) :: r, l) = - if a = addr - then (r, item :: l) - else popItems(r, item :: l) - val (newStack, scc) = popItems(stack', []) - in - (nextIndex, newStack, RecDecs scc :: subRes) - end - else (nextIndex, stack', subRes) + List.foldl rebuild [] processed end - - (* Process items that have not yet been reached *) - fun processUnprocessed (item as {addr, ...}, args) = - case Array.sub(mapArray, addr-startAddress) of - NONE => strongcomponent(item, args) - | _ => args - - val (_, _, result) = List.foldl processUnprocessed (0, [], []) rlist; - val recBindings = List.rev result - in - recBindings - end (* This is only intended for RecDecs but it's simpler to handle all bindings. *) | partitionMutableBindings other = [other] (* Functions to help in building a closure. *) datatype createClosure = Closure of (loadForm * int) list ref fun makeClosure() = Closure(ref []) (* Function to build a closure. Items are added to the closure if they are not already there. *) fun addToClosure (Closure closureList) (ext: loadForm): loadForm = case (List.find (fn (l, _) => l = ext) (!closureList), ! closureList) of (SOME(_, n), _) => (* Already there *) LoadClosure n | (NONE, []) => (* Not there - first *) (closureList := [(ext, 0)]; LoadClosure 0) | (NONE, cl as (_, n) :: _) => (closureList := (ext, n+1) :: cl; LoadClosure(n+1)) fun extractClosure(Closure (ref closureList)) = List.foldl (fn ((ext, _), l) => ext :: l) [] closureList structure Sharing = struct type codetree = codetree and codeBinding = codeBinding and loadForm = loadForm and createClosure = createClosure and envSpecial = envSpecial end end; diff --git a/mlsource/MLCompiler/CodeTree/X86Code/ICodeSig.ML b/mlsource/MLCompiler/CodeTree/X86Code/ICodeSig.ML index 99a6f7bf..c07b5d42 100644 --- a/mlsource/MLCompiler/CodeTree/X86Code/ICodeSig.ML +++ b/mlsource/MLCompiler/CodeTree/X86Code/ICodeSig.ML @@ -1,306 +1,306 @@ (* Signature for the high-level X86 code Copyright David C. J. Matthews 2016 This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License version 2.1 as published by the Free Software Foundation. This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with this library; if not, write to the Free Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA *) signature ICodeSig = sig type machineWord = Address.machineWord type address = Address.address (* Registers. *) datatype genReg = GeneralReg of Word8.word * bool and fpReg = FloatingPtReg of Word8.word and xmmReg = SSE2Reg of Word8.word datatype reg = GenReg of genReg | FPReg of fpReg | XMMReg of xmmReg val regRepr: reg -> string val isX64: bool and is32bit: LargeInt.int -> bool (* Should we use SSE2 or X87 floating point? *) datatype fpMode = FPModeSSE2 | FPModeX87 val fpMode: fpMode val eax: genReg and ebx: genReg and ecx: genReg and edx: genReg and edi: genReg and esi: genReg and esp: genReg and ebp: genReg and r8: genReg and r9: genReg and r10: genReg and r11: genReg and r12: genReg and r13: genReg and r14: genReg and r15: genReg and fp0: fpReg and fp1: fpReg and fp2: fpReg and fp3: fpReg and fp4: fpReg and fp5: fpReg and fp6: fpReg and fp7: fpReg and xmm0:xmmReg and xmm1:xmmReg and xmm2:xmmReg and xmm3:xmmReg and xmm4:xmmReg and xmm5:xmmReg and xmm6:xmmReg datatype branchOps = JO | JNO | JE | JNE | JL | JGE | JLE | JG | JB | JNB | JNA | JA | JP | JNP and arithOp = ADD | OR (*|ADC | SBB*) | AND | SUB | XOR | CMP and shiftType = SHL | SHR | SAR datatype boxKind = BoxLargeWord | BoxFloat and fpOps = FADD | FMUL | FCOM | FCOMP | FSUB | FSUBR | FDIV | FDIVR and fpUnaryOps = FABS | FCHS | FLD1 | FLDZ and sse2Operations = SSE2Move | SSE2Comp | SSE2Add | SSE2Sub | SSE2Mul | SSE2Div | SSE2Xor | SSE2And | SSE2MoveSingle | SSE2DoubleToFloat val memRegThreadSelf: int (* Copied from X86CodeSig *) datatype callKinds = Recursive | ConstantCode of machineWord | FullCall | DirectReg of genReg datatype pregKind = PRegGeneral (* A general register. This can contain and address and be pushed to the stack. *) | PRegUntagged (* An untagged general register. Just used for short-term storage. Not valid on the stack. *) datatype abstract = PReg of int * pregKind (* A pseudo-register - an abstract register. *) datatype 'reg argument = RegisterArgument of 'reg | AddressConstant of machineWord (* A constant that is an address. *) | IntegerConstant of LargeInt.int (* A non-address constant. Will usually be shifted and tagged. *) | MemoryLocation of { base: 'reg, offset: int, index: 'reg memoryIndex } (* A memory location. *) (* Offset on the stack. The "adjustment" is a temporary hack. *) - | StackLocation of { offset: int, adjustment: int } + | StackLocation of { wordOffset: int, adjustment: int } and 'reg memoryIndex = NoMemIndex | MemIndex1 of 'reg | MemIndex2 of 'reg | MemIndex4 of 'reg | MemIndex8 of 'reg (* Kinds of moves. MoveWord - Move a whole word - 64-bits in 64-bit mode, 32-bits in 32-bit mode. MoveByte - When loading, load a byte and zero extend. Move16Bit - Used for C-memory loads and stores. Zero extends on load. Move32Bit - Used for C-memory loads and stores in 64-bit mode. MoveFloat - Load and store a single-precision value MoveDouble - Load and store a double-precision value. *) datatype moveKind = MoveWord | MoveByte | Move16Bit | Move32Bit | MoveFloat | MoveDouble datatype iLabel = ILabel of int (* The reference to a condition code. *) datatype ccRef = CcRef of int datatype 'reg x86ICode = (* Move a value into a register. *) LoadArgument of { source: 'reg argument, dest: 'reg, kind: moveKind } (* Store a value into memory. The source will usually be a register but could be a constant depending on the value. *) | StoreArgument of { source: 'reg argument, base: 'reg, offset: int, index: 'reg memoryIndex, kind: moveKind } (* Load an entry from the "memory registers". Used just for ThreadSelf. *) | LoadMemReg of { offset: int, dest: 'reg } (* Exchange two registers. *) | ExchangeRegisters of { regX: 'reg, regY: 'reg } (* Start of function. Set the register arguments. *) | BeginFunction of { regArgs: ('reg * reg) list } (* Call a function. If the code address is a constant it is passed here. Otherwise the address is obtained by indirecting through rdx which has been loaded as one of the argument registers. The result is stored in the destination register. *) | FunctionCall of { callKind: callKinds, regArgs: ('reg argument * reg) list, stackArgs: 'reg argument list, dest: 'reg} (* Jump to a tail-recursive function. This is similar to FunctionCall but complicated for stack arguments because the stack and the return address need to be overwritten. We could actually include the return address among the stackArgs but leave that for the moment. stackAdjust is the number of words to remove (positive) or add (negative) to the stack before the call. *) | TailRecursiveCall of { callKind: callKinds, regArgs: ('reg argument * reg) list, stackArgs: {src: 'reg argument, stack: int} list, returnAddr: {srcStack: int, stack: int}, stackAdjust: int } (* Allocate a fixed sized piece of memory. The size is the number of words required. This sets the length word including the flags bits. saveRegs is the list of registers that need to be saved if we need to do a garbage collection. *) | AllocateMemoryOperation of { size: int, flags: Word8.word, dest: 'reg, saveRegs: 'reg list } (* Allocate a piece of memory whose size is not known at compile-time. The size argument is the number of words. *) | AllocateMemoryVariable of { size: 'reg, dest: 'reg, saveRegs: 'reg list } (* Initialise a piece of memory. N.B. The size is an untagged value containing the number of words. This uses REP STOSL/Q so addr must be rdi, size must be rcx and init must be rax. *) | InitialiseMem of { size: 'reg, addr: 'reg, init: 'reg } (* Signal that a tuple has been fully initialised. Really a check in the low-level code-generator. *) | InitialisationComplete of { dest: 'reg} (* Begin a loop. A set of loop registers are initialised and the loop is entered. The loopLabel in all of these is for checking only, at least at the moment. *) | StartLoop of { arguments: {source: 'reg argument, loopReg: 'reg} list, loopLabel: iLabel } (* End a loop. Causes the loop stack to be popped. *) | EndLoop of { loopLabel: iLabel } (* Within a loop the loop registers are updated from the source registers and a jump is made back to the containing StartLoop *) | JumpLoop of { arguments: {source: 'reg argument, loopReg: 'reg} list, loopLabel: iLabel } (* Raise an exception. The packet is always loaded into rax. *) | RaiseExceptionPacket of { packet: 'reg } (* Reserve a contiguous area on the stack to receive a result tuple. *) | ReserveContainer of { size: int, address: 'reg } (* Indexed case. *) | IndexedCaseOperation of { testReg: 'reg, workReg: 'reg, cases: iLabel list, startValue: word } (* Lock a mutable cell by turning off the mutable bit. *) | LockMutable of { addr: 'reg argument } (* Forward branches. *) | ForwardJumpLabel of { label: iLabel, result: 'reg option } | UnconditionalForwardJump of { label: iLabel } (* Conditional branch. *) | ConditionalForwardJump of { ccRef: ccRef, condition: branchOps, label: iLabel } (* Compare two word values. *) | WordComparison of { arg1: 'reg argument, arg2: 'reg argument, ccRef: ccRef } (* Exception handling. - Set up an exception handler. handlerAddr is really just a work register but it's currently used by codeToICode to mark the entry on its value stack. *) | PushExceptionHandler of { handlerAddr: 'reg, handleStart: iLabel } (* End of a handled section. Restore the previous handler. handlerAddr is not actually used. It's currently used as a marker by codeToICode. *) | PopExceptionHandler of { handlerAddr: 'reg, resultReg: 'reg option, workReg: 'reg } (* Marks the start of a handler. This sets the stack pointer and restores the old handler. Sets the exception packet register. *) | BeginHandler of { handleStart: iLabel, packetReg: 'reg, workReg: 'reg } (* Return from the function. *) | ReturnResultFromFunction of { resultReg: 'reg, numStackArgs: int } (* Arithmetic or logical operation. These can set the condition codes. *) | ArithmeticFunction of { oper: arithOp, resultReg: 'reg, operand1: 'reg argument, operand2: 'reg argument, ccRef: ccRef } (* Test the tag bit of a word. Sets the Zero bit if the value is an address i.e. untagged. *) | TestTagBit of { arg: 'reg argument, ccRef: ccRef } (* Push a value to the stack. Added during translation phase. *) | PushValue of { arg: 'reg argument } (* Remove items from the stack. Added during translation phase. *) | ResetStackPtr of { numWords: int } (* Tag a value by shifting and setting the tag bit. *) | TagValue of { source: 'reg, dest: 'reg } (* Shift a value to remove the tag bit. *) | UntagValue of { source: 'reg argument, dest: 'reg, isSigned: bool } (* This provides the LEA instruction which can be used for various sorts of arithmetic. The base register is optional in this case. *) | LoadEffectiveAddress of { base: 'reg option, offset: int, index: 'reg memoryIndex, dest: 'reg } (* Shift a word by an amount that can either be a constant or a register. *) | ShiftOperation of { shift: shiftType, resultReg: 'reg, operand: 'reg argument, shiftAmount: 'reg argument, ccRef: ccRef } (* Multiplication. We can use signed multiplication for both fixed precision and word (unsigned) multiplication. There are various forms of the instruction including a three-operand version. *) | Multiplication of { resultReg: 'reg, operand1: 'reg argument, operand2: 'reg argument, ccRef: ccRef } (* Division. This takes a register pair, always RDX:RAX, divides it by the operand register and puts the quotient in RAX and remainder in RDX. At the abstract level we represent all of these by pRegs. The divisor can be either a register or a memory location. *) | Division of { isSigned: bool, dividend: 'reg, divisor: 'reg argument, quotient: 'reg, remainder: 'reg } (* Atomic exchange and addition. This is executed with a lock prefix and is used for atomic increment and decrement for mutexes. Before the operation the source contains an increment. After the operation the source contains the old value of the destination and the destination has been updated with its old value added to the increment. The destination is actually the word pointed at by "base". *) | AtomicExchangeAndAdd of { base: 'reg, source: 'reg } (* Create a "box" of a single-word "byte" cell and store the source into it. This can be implemented using AllocateMemoryOperation but the idea is to allow the transform layer to recognise when a value is being boxed and then unboxed and remove unnecessary allocation. *) | BoxValue of { boxKind: boxKind, source: 'reg, dest: 'reg, saveRegs: 'reg list } (* Compare two vectors of bytes and set the condition code on the result. In general vec1Addr and vec2Addr will be pointers inside memory cells so have to be untagged registers. *) | CompareByteVectors of { vec1Addr: 'reg, vec2Addr: 'reg, length: 'reg, ccRef: ccRef } (* Move a block of bytes (isByteMove true) or words (isByteMove false). The length is the number of items (bytes or words) to move. *) | BlockMove of { srcAddr: 'reg, destAddr: 'reg, length: 'reg, isByteMove: bool } (* Floating point comparison. *) | CompareFloatingPt of { arg1: 'reg argument, arg2: 'reg argument, ccRef: ccRef } (* The X87 FP unit does not generate condition codes directly. We have to load the cc into RAX and test it there. *) | X87FPGetCondition of { ccRef: ccRef, dest: 'reg } (* Binary floating point operations on the X87. *) | X87FPArith of { opc: fpOps, resultReg: 'reg, arg1: 'reg argument, arg2: 'reg argument } (* Floating point operations: negate and set sign positive. *) | X87FPUnaryOps of { fpOp: fpUnaryOps, dest: 'reg, source: 'reg argument } (* Load a fixed point value as a floating point value. *) | FloatFixedInt of { dest: 'reg, source: 'reg argument } (* Binary floating point operations using SSE2 instructions. *) | SSE2FPArith of { opc: sse2Operations, resultReg: 'reg, arg1: 'reg argument, arg2: 'reg argument } val codeAsX86Code: {icode: reg x86ICode list, maxLabels: int, stackRequired: int, inputRegisters: reg list, functionName: string, debugSwitches: Universal.universal list } -> address val printICodeConcrete: reg x86ICode * (string -> unit) -> unit and printICodeAbstract: abstract x86ICode * (string -> unit) -> unit structure Sharing: sig type genReg = genReg and 'reg argument = 'reg argument and iLabel = iLabel and 'reg x86ICode = 'reg x86ICode and branchOps = branchOps and reg = reg and abstract = abstract end end; diff --git a/mlsource/MLCompiler/CodeTree/X86Code/X86ICodeToX86Code.ML b/mlsource/MLCompiler/CodeTree/X86Code/X86ICodeToX86Code.ML index aba66eb8..4c4a2a2e 100644 --- a/mlsource/MLCompiler/CodeTree/X86Code/X86ICodeToX86Code.ML +++ b/mlsource/MLCompiler/CodeTree/X86Code/X86ICodeToX86Code.ML @@ -1,1296 +1,1303 @@ (* Copyright David C. J. Matthews 2016 This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License version 2.1 as published by the Free Software Foundation. This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with this library; if not, write to the Free Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA *) functor X86ICodeToX86Code( structure X86CODE: X86CODESIG structure X86OPTIMISE: sig type operation type code type operations = operation list val optimise: code * operations -> operations structure Sharing: sig type operation = operation type code = code end end structure DEBUG: DEBUGSIG sharing X86CODE.Sharing = X86OPTIMISE.Sharing ): ICodeSig = struct open X86CODE datatype fpMode = FPModeSSE2 | FPModeX87 (* For the moment use SSE2 only on X86/64. Not all 32-bit processors support SSE2. *) val fpMode: fpMode = if isX64 then FPModeSSE2 else FPModeX87 open Address datatype pregKind = PRegGeneral (* A general register. This can contain and address and be pushed to the stack. *) | PRegUntagged (* An untagged general register. Just used for short-term storage. Not valid on the stack. *) datatype abstract = PReg of int * pregKind (* A pseudo-register - an abstract register. *) datatype 'reg argument = RegisterArgument of 'reg | AddressConstant of machineWord (* A constant that is an address. *) | IntegerConstant of LargeInt.int (* A non-address constant. Will usually be shifted and tagged. *) | MemoryLocation of { base: 'reg, offset: int, index: 'reg memoryIndex } (* A memory location. Could be the stack. *) - | StackLocation of { offset: int, adjustment: int } + | StackLocation of { wordOffset: int, adjustment: int } and 'reg memoryIndex = NoMemIndex | MemIndex1 of 'reg | MemIndex2 of 'reg | MemIndex4 of 'reg | MemIndex8 of 'reg (* Kinds of moves. MoveWord - Move a whole word - 64-bits in 64-bit mode, 32-bits in 32-bit mode. MoveByte - When loading, load a byte and zero extend. Move16Bit - Used for C-memory loads and stores. Zero extends on load. Move32Bit - Used for C-memory loads and stores in 64-bit mode. MoveFloat - Load and store a single-precision value MoveDouble - Load and store a double-precision value. *) datatype moveKind = MoveWord | MoveByte | Move16Bit | Move32Bit | MoveFloat | MoveDouble datatype iLabel = ILabel of int (* The reference to a condition code. *) and ccRef = CcRef of int datatype boxKind = BoxLargeWord | BoxFloat datatype 'reg x86ICode = (* Move a value into a register. *) LoadArgument of { source: 'reg argument, dest: 'reg, kind: moveKind } (* Store a value into memory. The source will usually be a register but could be a constant depending on the value. *) | StoreArgument of { source: 'reg argument, base: 'reg, offset: int, index: 'reg memoryIndex, kind: moveKind } (* Load an entry from the "memory registers". Used just for ThreadSelf. *) | LoadMemReg of { offset: int, dest: 'reg } (* Exchange two registers. *) | ExchangeRegisters of { regX: 'reg, regY: 'reg } (* Start of function. Set the register arguments. *) | BeginFunction of { regArgs: ('reg * reg) list } (* Call a function. If the code address is a constant it is passed here. Otherwise the address is obtained by indirecting through rdx which has been loaded as one of the argument registers. The result is stored in the destination register. *) | FunctionCall of { callKind: callKinds, regArgs: ('reg argument * reg) list, stackArgs: 'reg argument list, dest: 'reg} (* Jump to a tail-recursive function. This is similar to FunctionCall but complicated for stack arguments because the stack and the return address need to be overwritten. We could actually include the return address among the stackArgs but leave that for the moment. stackAdjust is the number of words to remove (positive) or add (negative) to the stack before the call. *) | TailRecursiveCall of { callKind: callKinds, regArgs: ('reg argument * reg) list, stackArgs: {src: 'reg argument, stack: int} list, returnAddr: {srcStack: int, stack: int}, stackAdjust: int } (* Allocate a fixed sized piece of memory. The size is the number of words required. This sets the length word including the flags bits. saveRegs is the list of registers that need to be saved if we need to do a garbage collection. *) | AllocateMemoryOperation of { size: int, flags: Word8.word, dest: 'reg, saveRegs: 'reg list } (* Allocate a piece of memory whose size is not known at compile-time. The size argument is the number of words. *) | AllocateMemoryVariable of { size: 'reg, dest: 'reg, saveRegs: 'reg list } (* Initialise a piece of memory. N.B. The size is an untagged value containing the number of words. This uses REP STOSL/Q so addr must be rdi, size must be rcx and init must be rax. *) | InitialiseMem of { size: 'reg, addr: 'reg, init: 'reg } (* Signal that a tuple has been fully initialised. Really a check in the low-level code-generator. *) | InitialisationComplete of { dest: 'reg} (* Begin a loop. A set of loop registers are initialised and the loop is entered. The loopLabel in all of these is for checking only, at least at the moment. *) | StartLoop of { arguments: {source: 'reg argument, loopReg: 'reg} list, loopLabel: iLabel } (* End a loop. Causes the loop stack to be popped. *) | EndLoop of { loopLabel: iLabel } (* Within a loop the loop registers are updated from the source registers and a jump is made back to the containing StartLoop *) | JumpLoop of { arguments: {source: 'reg argument, loopReg: 'reg} list, loopLabel: iLabel } (* Raise an exception. The packet is always loaded into rax. *) | RaiseExceptionPacket of { packet: 'reg } (* Reserve a contiguous area on the stack to receive a result tuple. *) | ReserveContainer of { size: int, address: 'reg } (* Indexed case. *) | IndexedCaseOperation of { testReg: 'reg, workReg: 'reg, cases: iLabel list, startValue: word } (* Lock a mutable cell by turning off the mutable bit. *) | LockMutable of { addr: 'reg argument } (* Forward branches. *) | ForwardJumpLabel of { label: iLabel, result: 'reg option } | UnconditionalForwardJump of { label: iLabel } (* Conditional branch. *) | ConditionalForwardJump of { ccRef: ccRef, condition: branchOps, label: iLabel } (* Compare two word values. *) | WordComparison of { arg1: 'reg argument, arg2: 'reg argument, ccRef: ccRef } (* Exception handling. - Set up an exception handler. *) | PushExceptionHandler of { handlerAddr: 'reg, handleStart: iLabel } (* End of a handled section. Restore the previous handler. *) | PopExceptionHandler of { handlerAddr: 'reg, resultReg: 'reg option, workReg: 'reg } (* Marks the start of a handler. This sets the stack pointer and restores the old handler. Sets the exception packet register. *) | BeginHandler of { handleStart: iLabel, packetReg: 'reg, workReg: 'reg } (* Return from the function. *) | ReturnResultFromFunction of { resultReg: 'reg, numStackArgs: int } (* Arithmetic or logical operation. These can set the condition codes. *) | ArithmeticFunction of { oper: arithOp, resultReg: 'reg, operand1: 'reg argument, operand2: 'reg argument, ccRef: ccRef } (* Test the tag bit of a word. Sets the Zero bit if the value is an address i.e. untagged. *) | TestTagBit of { arg: 'reg argument, ccRef: ccRef } (* Push a value to the stack. Added during translation phase. *) | PushValue of { arg: 'reg argument } (* Remove items from the stack. Added during translation phase. *) | ResetStackPtr of { numWords: int } (* Tag a value by shifting and setting the tag bit. *) | TagValue of { source: 'reg, dest: 'reg } (* Shift a value to remove the tag bit. *) | UntagValue of { source: 'reg argument, dest: 'reg, isSigned: bool } (* This provides the LEA instruction which can be used for various sorts of arithmetic. The base register is optional in this case. *) | LoadEffectiveAddress of { base: 'reg option, offset: int, index: 'reg memoryIndex, dest: 'reg } (* Shift a word by an amount that can either be a constant or a register. *) | ShiftOperation of { shift: shiftType, resultReg: 'reg, operand: 'reg argument, shiftAmount: 'reg argument, ccRef: ccRef } (* Multiplication. We can use signed multiplication for both fixed precision and word (unsigned) multiplication. There are various forms of the instruction including a three-operand version. *) | Multiplication of { resultReg: 'reg, operand1: 'reg argument, operand2: 'reg argument, ccRef: ccRef } (* Division. This takes a register pair, always RDX:RAX, divides it by the operand register and puts the quotient in RAX and remainder in RDX. At the abstract level we represent all of these by pRegs. The divisor can be either a register or a memory location. *) | Division of { isSigned: bool, dividend: 'reg, divisor: 'reg argument, quotient: 'reg, remainder: 'reg } (* Atomic exchange and addition. This is executed with a lock prefix and is used for atomic increment and decrement for mutexes. Before the operation the source contains an increment. After the operation the source contains the old value of the destination and the destination has been updated with its old value added to the increment. The destination is actually the word pointed at by "base". *) | AtomicExchangeAndAdd of { base: 'reg, source: 'reg } (* Create a "box" of a single-word "byte" cell and store the source into it. This can be implemented using AllocateMemoryOperation but the idea is to allow the transform layer to recognise when a value is being boxed and then unboxed and remove unnecessary allocation. *) | BoxValue of { boxKind: boxKind, source: 'reg, dest: 'reg, saveRegs: 'reg list } (* Compare two vectors of bytes and set the condition code on the result. In general vec1Addr and vec2Addr will be pointers inside memory cells so have to be untagged registers. *) | CompareByteVectors of { vec1Addr: 'reg, vec2Addr: 'reg, length: 'reg, ccRef: ccRef } (* Move a block of bytes (isByteMove true) or words (isByteMove false). The length is the number of items (bytes or words) to move. *) | BlockMove of { srcAddr: 'reg, destAddr: 'reg, length: 'reg, isByteMove: bool } (* Floating point comparison. *) | CompareFloatingPt of { arg1: 'reg argument, arg2: 'reg argument, ccRef: ccRef } (* The X87 FP unit does not generate condition codes directly. We have to load the cc into RAX and test it there. *) | X87FPGetCondition of { ccRef: ccRef, dest: 'reg } (* Binary floating point operations on the X87. *) | X87FPArith of { opc: fpOps, resultReg: 'reg, arg1: 'reg argument, arg2: 'reg argument } (* Floating point operations: negate and set sign positive. *) | X87FPUnaryOps of { fpOp: fpUnaryOps, dest: 'reg, source: 'reg argument } (* Load a fixed point value as a floating point value. *) | FloatFixedInt of { dest: 'reg, source: 'reg argument } (* Binary floating point operations using SSE2 instructions. *) | SSE2FPArith of { opc: sse2Operations, resultReg: 'reg, arg1: 'reg argument, arg2: 'reg argument } local fun printLabel(ILabel i, stream) = stream("L"^Int.toString i) fun printIndex(NoMemIndex, _, _) = () | printIndex(MemIndex1 i, stream, printReg) = (stream "["; printReg(i, stream); stream "*1]") | printIndex(MemIndex2 i, stream, printReg) = (stream "["; printReg(i, stream); stream "*2]") | printIndex(MemIndex4 i, stream, printReg) = (stream "["; printReg(i, stream); stream "*4]") | printIndex(MemIndex8 i, stream, printReg) = (stream "["; printReg(i, stream); stream "*8]") fun printArg(RegisterArgument reg, stream, printReg) = printReg(reg, stream) | printArg(AddressConstant m, stream, _) = stream(stringOfWord m) | printArg(IntegerConstant i, stream, _) = stream(LargeInt.toString i) | printArg(MemoryLocation{base, offset, index}, stream, printReg) = ( stream(Int.toString offset ^ "("); printReg(base, stream); stream ")"; printIndex(index, stream, printReg) ) - | printArg(StackLocation{offset, adjustment}, stream, _) = - stream(Int.toString offset ^ "+" ^ Int.toString adjustment ^ "(stackptr)") + | printArg(StackLocation{wordOffset, adjustment}, stream, _) = + stream(Int.toString wordOffset ^ "+" ^ Int.toString adjustment ^ "(stackptr)") fun printSaves([], _, _) = () | printSaves([areg], printReg, stream) = printReg(areg, stream) | printSaves(areg::more, printReg, stream) = (printReg(areg, stream); stream ","; printSaves(more, printReg, stream)) fun printICode(LoadArgument{source, dest, kind}, stream, printReg) = ( case kind of MoveWord => stream "\tLoadWord\t" | MoveByte => stream "\tLoadByte\t" | Move16Bit => stream "\tLoad16Bit\t" | Move32Bit => stream "\tLoad32Bit\t" | MoveFloat => stream "\tLoadFloat\t" | MoveDouble => stream "\tLoadDouble\t"; printArg(source, stream, printReg); stream " => "; printReg(dest, stream) ) | printICode(StoreArgument{source, base, offset, index, kind}, stream, printReg) = ( case kind of MoveWord => stream "\tStoreWord\t" | MoveByte => stream "\tStoreByte\t" | Move16Bit => stream "\tStore16Bit\t" | Move32Bit => stream "\tStore32Bit\t" | MoveFloat => stream "\tStoreeFloat\t" | MoveDouble => stream "\tStoreDouble\t"; printArg(source, stream, printReg); stream " => "; stream(Int.toString offset ^ "("); printReg(base, stream); stream ")"; printIndex(index, stream, printReg) ) | printICode(LoadMemReg { offset, dest}, stream, printReg) = ( stream "\tLoadMemReg\t"; stream(Int.toString offset); stream " => "; printReg(dest, stream) ) | printICode(ExchangeRegisters { regX, regY}, stream, printReg) = ( stream "\tExchangeRegs\t"; printReg(regX, stream); stream " <=> "; printReg(regY, stream) ) | printICode(BeginFunction {regArgs}, stream, printReg) = ( stream "\tBeginFunction\t"; List.app(fn (arg, r) => (stream(regRepr r); stream "="; printReg(arg, stream); stream " ")) regArgs ) | printICode(FunctionCall{callKind, regArgs, stackArgs, dest}, stream, printReg) = ( stream "\tFunctionCall\t"; case callKind of Recursive => stream "recursive " | ConstantCode m => (stream(stringOfWord m); stream " ") | FullCall => () | DirectReg r => (stream(regRepr(GenReg r)); stream " "); List.app(fn (arg, r) => (stream(regRepr r); stream "="; printArg(arg, stream, printReg); stream " ")) regArgs; List.app(fn arg => (stream "p="; printArg(arg, stream, printReg); stream " ")) stackArgs; stream "=> "; printReg(dest, stream) ) | printICode(TailRecursiveCall{callKind, regArgs, stackArgs, returnAddr={srcStack, stack}, stackAdjust}, stream, printReg) = ( stream "\tTailCall\t"; case callKind of Recursive => stream "recursive " | ConstantCode m => (stream(stringOfWord m); stream " ") | FullCall => () | DirectReg r => (stream(regRepr(GenReg r)); stream " "); List.app(fn (arg, r) => (stream(regRepr r); stream "="; printArg(arg, stream, printReg); stream " ")) regArgs; List.app(fn {src, stack} => (stream (Int.toString stack); stream "<="; printArg(src, stream, printReg); stream " ")) stackArgs; stream "ret "; stream(Int.toString stack); stream "<="; stream(Int.toString srcStack); stream "adj="; stream(Int.toString stackAdjust) ) | printICode(AllocateMemoryOperation{size, flags, dest, saveRegs}, stream, printReg) = ( stream "\tAllocateMemory\t"; stream(concat["s=", Int.toString size, ",f=", Word8.toString flags, " => "]); printReg(dest, stream); stream " save="; printSaves(saveRegs, printReg, stream) ) | printICode(AllocateMemoryVariable{size, dest, saveRegs}, stream, printReg) = ( stream "\tAllocateMemory\t"; stream "s="; printReg(size, stream); stream " => "; printReg(dest, stream); stream " save="; printSaves(saveRegs, printReg, stream) ) | printICode(InitialiseMem{size, addr, init}, stream, printReg) = ( stream "\tInitialiseMem\t"; stream "s="; printReg(size, stream); stream ",i="; printReg(init, stream); stream ",a="; printReg(addr, stream) ) | printICode(InitialisationComplete{dest}, stream, printReg) = (stream "\tInitComplete\t"; printReg(dest, stream)) | printICode(StartLoop{arguments, loopLabel}, stream, printReg) = ( printLabel(loopLabel, stream); stream ":\tStartLoop\t"; List.app( fn {source, loopReg} => (printReg(loopReg, stream); stream "="; printArg(source, stream, printReg); stream " ") ) arguments ) | printICode(EndLoop{loopLabel}, stream, _) = (stream "\tEndLoop\t"; printLabel(loopLabel, stream)) | printICode(JumpLoop{arguments, loopLabel}, stream, printReg) = ( stream "\tJumpLoop\t"; List.app( fn {source, loopReg} => (printReg(loopReg, stream); stream "="; printArg(source, stream, printReg); stream " ") ) arguments; printLabel(loopLabel, stream) ) | printICode(RaiseExceptionPacket{packet}, stream, printReg) = (stream "\tRaise\t"; printReg(packet, stream)) | printICode(ReserveContainer{size, address}, stream, printReg) = (stream "\tReserveContainer\t"; stream(Int.toString size); stream "=>"; printReg(address, stream)) | printICode(IndexedCaseOperation{testReg, workReg, cases, startValue}, stream, printReg) = ( stream "\tIndexedCase\t"; stream "test="; printReg(testReg, stream); stream "work="; printReg(workReg, stream); stream "from="; stream(Word.toString startValue); List.app(fn l => (stream " "; printLabel(l, stream))) cases ) | printICode(LockMutable{addr}, stream, printReg) = (stream "\tLockMutable\t"; printArg(addr, stream, printReg)) | printICode(ForwardJumpLabel{label, ...}, stream, _) = (printLabel(label, stream); stream ":\t\t") | printICode(UnconditionalForwardJump{label}, stream, _) = (stream "\tJump\t"; printLabel(label, stream)) | printICode(ConditionalForwardJump{condition, label, ...}, stream, _) = ( case condition of JO => stream "\tJumpOverflow\t" | JNO => stream "\tJumpNoOverflow\t" | JE => stream "\tJumpEqual\t" | JNE => stream "\tJumpNotEqual\t" | JL => stream "\tJumpLessSigned\t" | JGE => stream "\tJumpGeqSigned\t" | JLE => stream "\tJumpLeqSigned\t" | JG => stream "\tJumpGrtSigned\t" | JB => stream "\tJumpLessUnsigned\t" | JNB => stream "\tJumpGeqUnsigned\t" | JNA => stream "\tJumpLeqUnsigned\t" | JA => stream "\tJumpGrtUnsigned\t" | JP => stream "\tJumpParitySet" | JNP => stream "\tJumpParityClear\t"; printLabel(label, stream) ) | printICode(WordComparison{arg1, arg2, ...}, stream, printReg) = (stream "\tWordComparison\t"; printArg(arg1, stream, printReg); stream ","; printArg(arg2, stream, printReg)) | printICode(PushExceptionHandler{handlerAddr, handleStart}, stream, printReg) = ( stream "\tPushExcHandler\t"; printLabel(handleStart, stream); stream " with "; printReg(handlerAddr, stream) ) | printICode(PopExceptionHandler{handlerAddr=_, resultReg=_, workReg}, stream, printReg) = ( stream "\tPopExceptionHandler\t"; stream "with "; printReg(workReg, stream) ) | printICode(BeginHandler{handleStart, packetReg, workReg}, stream, printReg) = ( printLabel(handleStart, stream); stream ":\tBeginHandler\t"; printReg(packetReg, stream); stream " with "; printReg(workReg, stream) ) | printICode(ReturnResultFromFunction{resultReg, numStackArgs}, stream, printReg) = (stream "\tReturnFromFunction\t"; printReg(resultReg, stream); stream("," ^ Int.toString numStackArgs)) | printICode(ArithmeticFunction{oper, resultReg, operand1, operand2, ...}, stream, printReg) = ( case oper of ADD => stream "\tAdd\t" | OR => stream "\tOrBits\t" | AND => stream "\tAndBits\t" | SUB => stream "\tSubtract\t" | XOR => stream "\tExclusiveOrBits\t" | CMP => stream "\tCompare\t"; printArg(operand1, stream, printReg); stream ","; printArg(operand2, stream, printReg); stream " => "; printReg(resultReg, stream) ) | printICode(TestTagBit{arg, ...}, stream, printReg) = (stream "\tTestTagBit\t"; printArg(arg, stream, printReg)) | printICode(PushValue{arg}, stream, printReg) = (stream "\tPushValue\t"; printArg(arg, stream, printReg)) | printICode(ResetStackPtr{numWords}, stream, _) = (stream "\tResetStackPtr\t"; stream(Int.toString numWords)) | printICode(TagValue{source, dest}, stream, printReg) = (stream "\tTagValue\t"; printReg(source, stream); stream " => "; printReg(dest, stream)) | printICode(UntagValue{source, dest, isSigned=true}, stream, printReg) = (stream "\tUntagSigned\t"; printArg(source, stream, printReg); stream " => "; printReg(dest, stream)) | printICode(UntagValue{source, dest, isSigned=false}, stream, printReg) = (stream "\tUntagSigned\t"; printArg(source, stream, printReg); stream " => "; printReg(dest, stream)) | printICode(LoadEffectiveAddress{base, offset, index, dest}, stream, printReg) = ( stream "\tLoadEffectiveAddr\t"; stream(Int.toString offset ^ "("); case base of NONE => stream "_" | SOME b => printReg(b, stream); stream ")"; printIndex(index, stream, printReg); stream " => "; printReg(dest, stream) ) | printICode(ShiftOperation{shift, resultReg, operand, shiftAmount, ...}, stream, printReg) = ( case shift of SHL => stream "\tShiftLeft\t" | SHR => stream "\tShiftRLogical\t" | SAR => stream "\tShiftRArith\t"; printArg(operand, stream, printReg); stream ","; printArg(shiftAmount, stream, printReg); stream " => "; printReg(resultReg, stream) ) | printICode(Multiplication{resultReg, operand1, operand2, ...}, stream, printReg) = ( stream "\tMultiplication\t"; printArg(operand1, stream, printReg); stream ","; printArg(operand2, stream, printReg); stream " => "; printReg(resultReg, stream) ) | printICode(Division{isSigned, dividend, divisor, quotient, remainder}, stream, printReg) = ( stream "\tDivision"; stream(if isSigned then "Signed\t" else "Unsigned\t"); printReg(dividend, stream); stream " by "; printArg(divisor, stream, printReg); stream " => "; printReg(quotient, stream); stream " rem "; printReg(remainder, stream) ) | printICode(AtomicExchangeAndAdd{base, source}, stream, printReg) = ( stream "\tAtomicExchangeAndAdd\t"; stream "addr=0("; printReg(base, stream); stream "),with="; printReg(source, stream) ) | printICode(BoxValue{boxKind, source, dest, saveRegs}, stream, printReg) = ( case boxKind of BoxLargeWord => stream "\tBoxLarge\t" | BoxFloat => stream "\tBoxFloat\t"; printReg(source, stream); stream " => "; printReg(dest, stream); stream " save="; printSaves(saveRegs, printReg, stream) ) | printICode(CompareByteVectors{vec1Addr, vec2Addr, length, ...}, stream, printReg) = ( stream "\tCompareByteVectors\t"; printReg(vec1Addr, stream); stream ","; printReg(vec2Addr, stream); stream ","; printReg(length, stream) ) | printICode(BlockMove{srcAddr, destAddr, length, isByteMove}, stream, printReg) = ( stream(if isByteMove then "\tBlockByteMove\t" else "\tBlockWordMove\t"); stream "src="; printReg(srcAddr, stream); stream ",dest="; printReg(destAddr, stream); stream ",len="; printReg(length, stream) ) | printICode(CompareFloatingPt{arg1, arg2, ...}, stream, printReg) = (stream "\tCompareFloatingPt\t"; printArg(arg1, stream, printReg); stream ","; printArg(arg2, stream, printReg)) | printICode(X87FPGetCondition{dest, ...}, stream, printReg) = (stream "\tX87FPGetCondition\t => "; printReg(dest, stream)) | printICode(X87FPArith{opc, resultReg, arg1, arg2}, stream, printReg) = ( case opc of FADD => stream "\tX87FPAdd\t" | FMUL => stream "\tX87FPMul" | FCOM => stream "\tX87FPCompare\t" | FCOMP => stream "\tX87FPComparePop\t" | FSUB => stream "\tX87FPSub\t" | FSUBR => stream "\tX87FPRevSub\t" | FDIV => stream "\tX87FPDiv\t" | FDIVR => stream "\tX87FPRevDiv\t"; printArg(arg1, stream, printReg); stream ","; printArg(arg2, stream, printReg); stream " => "; printReg(resultReg, stream) ) | printICode(X87FPUnaryOps{fpOp, dest, source}, stream, printReg) = ( case fpOp of FABS => stream "\tX87FPAbs\t" | FCHS => stream "\tX87FPNegate\t" | FLD1 => stream "\tX87FPLoad1\t" | FLDZ => stream "\tX87FPLoad0\t"; printArg(source, stream, printReg); stream " => "; printReg(dest, stream) ) | printICode(FloatFixedInt{dest, source}, stream, printReg) = (stream "\tFloatFixedInt\t"; printArg(source, stream, printReg); stream " => "; printReg(dest, stream)) | printICode(SSE2FPArith{opc, resultReg, arg1, arg2}, stream, printReg) = ( case opc of SSE2Move => stream "\tSSE2FPMove\t" | SSE2Comp => stream "\tSSE2FPComp\t" | SSE2Add => stream "\tSSE2FPAdd\t" | SSE2Sub => stream "\tSSE2FPSub\t" | SSE2Mul => stream "\tSSE2FPMul\t" | SSE2Div => stream "\tSSE2FPDiv\t" | SSE2Xor => stream "\tSSE2FPXor\t" | SSE2And => stream "\tSSE2FPAnd\t" | SSE2MoveSingle => stream "\tSSE2FPMoveSingle\t" | SSE2DoubleToFloat => stream "\tSSE2FPDoubleToFloat\t"; printArg(arg1, stream, printReg); stream ","; printArg(arg2, stream, printReg); stream " => "; printReg(resultReg, stream) ) fun printConcreteReg(reg, stream) = stream(regRepr reg) and printAbstractReg(PReg(i, PRegGeneral), stream) = stream("G" ^ Int.toString i) | printAbstractReg(PReg(i, PRegUntagged), stream) = stream("U" ^ Int.toString i) in fun printICodeConcrete(icode, stream) = printICode(icode, stream, printConcreteReg) and printICodeAbstract(icode, stream) = printICode(icode, stream, printAbstractReg) end exception InternalError = Misc.InternalError (* Generate code from the ICode. This assumes that all pseudo-registers have been replaced by real registers or locations. Only certain patterns of arguments are accepted. *) fun codeAsX86Code{icode, maxLabels, stackRequired, inputRegisters: reg list, functionName, debugSwitches} = let (* The profile object is a single mutable with the F_bytes bit set. *) local val v = RunCall.allocateByteMemory(0w1, Word.fromLargeWord(Word8.toLargeWord(Word8.orb(F_mutable, F_bytes)))) fun clear 0w0 = () | clear i = (assignByte(v, i-0w1, 0w0); clear (i-0w1)) val () = clear(Word.fromInt wordSize) in val profileObject = toMachineWord v end (* Switch to indicate if we want to trace where live data has been allocated. *) val addAllocatingFunction = DEBUG.getParameter DEBUG.profileAllocationTag debugSwitches = 1 fun asGenReg(GenReg r) = r | asGenReg _ = raise InternalError "asGenReg" fun argAsGenReg(RegisterArgument(GenReg r)) = r | argAsGenReg _ = raise InternalError "argAsGenReg" (* Labels. Create an array and fill in the entries. *) datatype labelKind = NormalLabel of label | HandlerLab of addrs ref | NoLabel val labelArray = Array.array(maxLabels, NoLabel) fun addLabels(ForwardJumpLabel{label=ILabel labno, ...}) = ( case Array.sub(labelArray, labno) of NoLabel => () | _ => raise InternalError "addLabels: redefined"; Array.update(labelArray, labno, NormalLabel(mkLabel())) ) | addLabels(StartLoop{loopLabel=ILabel labno, ...}) = ( case Array.sub(labelArray, labno) of NoLabel => () | _ => raise InternalError "addLabels: redefined"; Array.update(labelArray, labno, NormalLabel(mkLabel())) ) | addLabels(PushExceptionHandler{ handleStart=ILabel labno, ... }) = ( case Array.sub(labelArray, labno) of NoLabel => () | _ => raise InternalError "addLabels: redefined"; Array.update(labelArray, labno, HandlerLab(ref addrZero)) ) | addLabels _ = () val () = List.app addLabels icode (* Look up a normal label. *) fun findLabelDef(ILabel labno) = case Array.sub(labelArray, labno) of NormalLabel l => l | _ => raise InternalError "findLabel: label not defined" (* Look up a label and increment the reference count. *) fun findLabelRef lab = case findLabelDef lab of l as Labels{uses, ...} => (uses := !uses + 1; l) fun memoryAddressAsBaseOffset({offset, base=(GenReg baseReg), index}) = {base=baseReg, offset=offset, index=memoryIndexAsIndex index} | memoryAddressAsBaseOffset _ = raise InternalError "memoryAddressAsBaseOffset" and memoryIndexAsIndex NoMemIndex = NoIndex | memoryIndexAsIndex(MemIndex1((GenReg iReg))) = Index1 iReg | memoryIndexAsIndex(MemIndex2((GenReg iReg))) = Index2 iReg | memoryIndexAsIndex(MemIndex4((GenReg iReg))) = Index4 iReg | memoryIndexAsIndex(MemIndex8((GenReg iReg))) = Index8 iReg | memoryIndexAsIndex _ = raise InternalError "memoryIndexAsIndex" and sourceAsGenRegOrMem(RegisterArgument((GenReg r))) = RegisterArg r | sourceAsGenRegOrMem(MemoryLocation{offset, base=(GenReg baseReg), index}) = MemoryArg{base=baseReg, offset=offset, index=memoryIndexAsIndex index} | sourceAsGenRegOrMem(IntegerConstant v) = NonAddressConstArg v | sourceAsGenRegOrMem(AddressConstant v) = AddressConstArg v | sourceAsGenRegOrMem _ = raise InternalError "sourceAsGenRegOrMem" and sourceAsXMMRegOrMem(RegisterArgument((XMMReg r))) = RegisterArg r | sourceAsXMMRegOrMem(MemoryLocation{offset, base=(GenReg baseReg), index}) = MemoryArg{base=baseReg, offset=offset, index=memoryIndexAsIndex index} | sourceAsXMMRegOrMem(IntegerConstant v) = NonAddressConstArg v | sourceAsXMMRegOrMem(AddressConstant v) = AddressConstArg v | sourceAsXMMRegOrMem _ = raise InternalError "sourceAsGenRegOrMem" (* Turn the icode into machine code. This produces the code in reverse. *) fun codeGenICode([], code) = code | codeGenICode( (* Load to a general register or move to a general register. *) LoadArgument{ source, dest=GenReg destReg, kind=MoveWord} :: rest, code) = codeGenICode(rest, MoveToRegister { source=sourceAsGenRegOrMem source, output=destReg } :: code) | codeGenICode( (* Load from memory. *) LoadArgument{ source=MemoryLocation mLoc, dest=GenReg destReg, kind=MoveByte} :: rest, code) = codeGenICode(rest, LoadNonWord{size=Size8Bit, source=memoryAddressAsBaseOffset mLoc, output=destReg} :: code) | codeGenICode( (* Load from memory. *) LoadArgument{ source=MemoryLocation mLoc, dest=GenReg destReg, kind=Move16Bit} :: rest, code) = codeGenICode(rest, LoadNonWord{size=Size16Bit, source=memoryAddressAsBaseOffset mLoc, output=destReg} :: code) | codeGenICode( (* Load from memory. *) LoadArgument{ source=MemoryLocation mLoc, dest=GenReg destReg, kind=Move32Bit} :: rest, code) = codeGenICode(rest, LoadNonWord{size=Size32Bit, source=memoryAddressAsBaseOffset mLoc, output=destReg} :: code) (* Store to memory *) | codeGenICode( StoreArgument{ source=RegisterArgument(GenReg sourceReg), base, offset, index, kind=MoveWord} :: rest, code) = codeGenICode(rest, StoreRegToMemory{toStore=sourceReg, address=memoryAddressAsBaseOffset{base=base, offset=offset, index=index}} :: code) | codeGenICode( StoreArgument{ source=RegisterArgument(GenReg sourceReg), base, offset, index, kind=MoveByte} :: rest, code) = codeGenICode(rest, StoreNonWord{size=Size8Bit, toStore=sourceReg, address=memoryAddressAsBaseOffset {base=base, offset=offset, index=index}} :: code) | codeGenICode( StoreArgument{ source=RegisterArgument(GenReg sourceReg), base, offset, index, kind=Move16Bit} :: rest, code) = codeGenICode(rest, StoreNonWord{size=Size16Bit, toStore=sourceReg, address=memoryAddressAsBaseOffset {base=base, offset=offset, index=index}} :: code) | codeGenICode( StoreArgument{ source=RegisterArgument(GenReg sourceReg), base, offset, index, kind=Move32Bit} :: rest, code) = codeGenICode(rest, StoreNonWord{size=Size32Bit, toStore=sourceReg, address=memoryAddressAsBaseOffset {base=base, offset=offset, index=index}} :: code) (* Store a short constant to memory *) | codeGenICode( StoreArgument{ source=IntegerConstant srcValue, base, offset, index, kind=MoveWord} :: rest, code) = codeGenICode(rest, StoreConstToMemory{toStore=srcValue, address=memoryAddressAsBaseOffset {base=base, offset=offset, index=index}} :: code) | codeGenICode( StoreArgument{ source=IntegerConstant srcValue, base, offset, index, kind=MoveByte} :: rest, code) = codeGenICode(rest, StoreNonWordConst{size=Size8Bit, toStore=srcValue, address=memoryAddressAsBaseOffset {base=base, offset=offset, index=index}} :: code) (* Store a long constant to memory *) | codeGenICode( StoreArgument{ source=AddressConstant srcValue, base, offset, index, kind=MoveWord} :: rest, code) = codeGenICode(rest, StoreLongConstToMemory{toStore=srcValue, address=memoryAddressAsBaseOffset {base=base, offset=offset, index=index}} :: code) (* Load a floating point value. *) | codeGenICode(LoadArgument{source=MemoryLocation{offset, base=(GenReg baseReg), index}, dest=FPReg fpReg, kind=MoveDouble} :: rest, code) = let val _ = fpReg = fp0 orelse raise InternalError "codeGenICode: Load FPReg <> fp0" in codeGenICode(rest, FPLoadFromMemory{ address={base=baseReg, offset=offset, index=memoryIndexAsIndex index}, precision=DoublePrecision } :: code) end (* Load or move from an XMM reg. *) | codeGenICode(LoadArgument{source, dest=XMMReg xmmRegReg, kind=MoveDouble} :: rest, code) = codeGenICode(rest, XMMArith { opc= SSE2Move, source=sourceAsXMMRegOrMem source, output=xmmRegReg } :: code) (* Store a floating point value. *) | codeGenICode(StoreArgument{source=RegisterArgument(FPReg fpReg), offset, base=(GenReg baseReg), index, kind=MoveDouble} :: rest, code) = let val _ = fpReg = fp0 orelse raise InternalError "codeGenICode: Store FPReg <> fp0" in codeGenICode(rest, FPStoreToMemory{ address={ base=baseReg, offset=offset, index=memoryIndexAsIndex index}, precision=DoublePrecision, andPop=true } :: code) end | codeGenICode(StoreArgument{source=RegisterArgument(XMMReg xmmRegReg), offset, base=(GenReg baseReg), index, kind=MoveDouble} :: rest, code) = codeGenICode(rest, XMMStoreToMemory { toStore=xmmRegReg, address={base=baseReg, offset=offset, index=memoryIndexAsIndex index}, precision=DoublePrecision } :: code) (* Load a floating point value. *) | codeGenICode(LoadArgument{source=MemoryLocation{offset, base=(GenReg baseReg), index}, dest=FPReg fpReg, kind=MoveFloat} :: rest, code) = let val _ = fpReg = fp0 orelse raise InternalError "codeGenICode: Load FPReg <> fp0" in codeGenICode(rest, FPLoadFromMemory{ address={ base=baseReg, offset=offset, index=memoryIndexAsIndex index }, precision=SinglePrecision } :: code) end (* Load or move from an XMM reg. *) | codeGenICode(LoadArgument{source, dest=XMMReg xmmRegReg, kind=MoveFloat} :: rest, code) = codeGenICode(rest, XMMArith { opc= SSE2MoveSingle, source=sourceAsXMMRegOrMem source, output=xmmRegReg } :: code) (* Store a floating point value. *) | codeGenICode(StoreArgument{source=RegisterArgument(FPReg fpReg), offset, base=(GenReg baseReg), index, kind=MoveFloat} :: rest, code) = let val _ = fpReg = fp0 orelse raise InternalError "codeGenICode: Store FPReg <> fp0" in codeGenICode(rest, FPStoreToMemory{address={ base=baseReg, offset=offset, index=memoryIndexAsIndex index}, precision=SinglePrecision, andPop=true } :: code) end | codeGenICode(StoreArgument{source=RegisterArgument(XMMReg xmmRegReg), offset, base=(GenReg baseReg), index, kind=MoveFloat} :: rest, code) = codeGenICode(rest, XMMStoreToMemory { toStore=xmmRegReg, address={base=baseReg, offset=offset, index=memoryIndexAsIndex index}, precision=SinglePrecision } :: code) (* Any other combinations are not allowed. *) | codeGenICode(LoadArgument _ :: _, _) = raise InternalError "codeGenICode: LoadArgument" | codeGenICode(StoreArgument _ :: _, _) = raise InternalError "codeGenICode: StoreArgument" (* This should have been transformed into MoveArgument. *) | codeGenICode(LoadMemReg _ :: _, _) = raise InternalError "codeGenICode - LoadMemReg" (* Exchange two general registers. *) | codeGenICode(ExchangeRegisters{ regX, regY} :: rest, code) = codeGenICode(rest, XChngRegisters { regX=asGenReg regX, regY=asGenReg regY } :: code) | codeGenICode(BeginFunction _ :: rest, code) = codeGenICode(rest, code) (* Don't need to do anything. *) | codeGenICode(FunctionCall {callKind, ...} :: rest, code) = codeGenICode(rest, CallFunction callKind :: code) | codeGenICode(TailRecursiveCall {callKind, ...} :: rest, code) = codeGenICode(rest, JumpToFunction callKind :: code) | codeGenICode(AllocateMemoryOperation { size, flags, dest, saveRegs} :: rest, code) = let val toReg = asGenReg dest val preserve = map asGenReg saveRegs (* Allocate memory. N.B. Instructions are in reverse order. *) fun allocStore{size, flags, output, preserve} = if isX64 andalso flags <> 0w0 then [StoreNonWordConst{size=Size8Bit, toStore=Word8.toLargeInt flags, address={offset= ~1, base=output, index=NoIndex}}, StoreConstToMemory{toStore=LargeInt.fromInt size, address={offset= ~wordSize, base=output, index=NoIndex}}, AllocStore{size=size, output=output, saveRegs=preserve}] else let val lengthWord = IntInf.orb(IntInf.fromInt size, IntInf.<<(Word8.toLargeInt flags, 0w24)) in [StoreConstToMemory{toStore=lengthWord, address={offset= ~wordSize, base=output, index=NoIndex}}, AllocStore{size=size, output=output, saveRegs=preserve}] end val allocCode = (* If we need to add the profile object *) if addAllocatingFunction then allocStore {size=size+1, flags=Word8.orb(flags, Address.F_profile), output=toReg, preserve=preserve} @ [StoreLongConstToMemory{ toStore=profileObject, address={base=toReg, offset=size*wordSize, index=NoIndex}}] else allocStore {size=size, flags=flags, output=toReg, preserve=preserve} in codeGenICode(rest, allocCode @ code) end | codeGenICode(AllocateMemoryVariable{ size, dest, saveRegs} :: rest, code) = let val sReg = asGenReg size and dReg = asGenReg dest val _ = sReg <> dReg orelse raise InternalError "codeGenICode-AllocateMemoryVariable" val preserve = map asGenReg saveRegs val allocCode = [ (* Store it as the length field. *) StoreRegToMemory{toStore=sReg, address={base=dReg, offset= ~wordSize, index=NoIndex}}, (* Untag the length *) ShiftConstant{ shiftType=SHR, output=sReg, shift=0w1}, (* Allocate the memory *) AllocStoreVariable{ output=dReg, saveRegs=preserve}, (* Compute the number of bytes into dReg. The length in sReg is the number of words as a tagged value so we need to multiply it, add wordSize to include one word for the header then subtract the, multiplied, tag. *) if wordSize = 4 then LoadAddress{output=dReg, base=NONE, offset=wordSize-2, index=Index2 sReg } else LoadAddress{output=dReg, base=NONE, offset=wordSize-4, index=Index4 sReg } ] in codeGenICode(rest, allocCode @ code) end | codeGenICode(InitialiseMem{size, addr, init} :: rest, code) = let val sReg = asGenReg size and iReg = asGenReg init and aReg = asGenReg addr (* Initialise the memory. This requires that sReg = ecx, iReg = eax and aReg = edi. *) val _ = sReg = ecx orelse raise InternalError "codeGenICode: InitialiseMem" val _ = iReg = eax orelse raise InternalError "codeGenICode: InitialiseMem" val _ = aReg = edi orelse raise InternalError "codeGenICode: InitialiseMem" in codeGenICode(rest, RepeatOperation STOSL :: code) end | codeGenICode(InitialisationComplete _ :: rest, code) = codeGenICode(rest, StoreInitialised :: code) | codeGenICode(StartLoop {loopLabel, ...} :: rest, code) = (* Same as ForwardLabel. *) codeGenICode(rest, JumpLabel(findLabelDef loopLabel) :: code) | codeGenICode(EndLoop _ :: rest, code) = (* Nothing to do here. *) codeGenICode(rest, code) | codeGenICode(JumpLoop {loopLabel, ...} :: rest, code) = codeGenICode(rest, UncondBranch (findLabelRef loopLabel) :: code) | codeGenICode(RaiseExceptionPacket _ :: rest, code) = codeGenICode(rest, RaiseException :: code) | codeGenICode(IndexedCaseOperation { testReg, workReg, cases, startValue} :: rest, code) = let val rReg = asGenReg testReg and wReg = asGenReg workReg val caseLabels = map findLabelRef cases in codeGenICode(rest, IndexedCase{testReg=rReg, workReg=wReg, min=startValue, cases=caseLabels} :: code) end | codeGenICode(LockMutable { addr } :: rest, code) = codeGenICode(rest, LockMutableSegment (argAsGenReg addr) :: code) | codeGenICode(ForwardJumpLabel { label, ... } :: rest, code) = codeGenICode(rest, JumpLabel(findLabelDef label) :: code) | codeGenICode(UnconditionalForwardJump {label} :: rest, code) = codeGenICode(rest, UncondBranch(findLabelRef label) :: code) | codeGenICode(ConditionalForwardJump {condition, label, ...} :: rest, code) = codeGenICode(rest, ConditionalBranch{test=condition, predict=PredictNeutral, label=findLabelRef label} :: code) | codeGenICode(WordComparison {arg1=RegisterArgument(GenReg r), arg2, ...} :: rest, code) = codeGenICode(rest, ArithToGenReg {opc=CMP, output=r, source=sourceAsGenRegOrMem arg2} :: code) | codeGenICode(WordComparison _ :: _, _) = raise InternalError "codeGenICode: TODO WordComparison" | codeGenICode(PushExceptionHandler { handlerAddr, handleStart=ILabel hStart, ... } :: rest, code) = let (* Set up an exception handler. *) val handleReg = asGenReg handlerAddr val labelRef = case Array.sub(labelArray, hStart) of HandlerLab addr => addr | _ => raise InternalError "codeGenICode: PushExceptionHandler not handler" (* Set up the handler by pushing the old handler to the stack, pushing the entry point and setting the handler address to the current stack pointer. *) in codeGenICode(rest, StoreRegToMemory{ toStore=esp, address={offset=memRegHandlerRegister, base=ebp, index=NoIndex}} :: PushToStack(RegisterArg handleReg) :: LoadHandlerAddress{ handlerLab=labelRef, output=handleReg} :: PushToStack(MemoryArg{base=ebp, offset=memRegHandlerRegister, index=NoIndex}) :: code) end | codeGenICode(PopExceptionHandler { workReg, ... } :: rest, code) = let (* Remove an exception handler if no exception was raised. *) val wReg = asGenReg workReg in (* The stack pointer has been adjusted to just above the two words that were stored in PushExceptionHandler. *) codeGenICode(rest, StoreRegToMemory{ toStore=wReg, address={offset=memRegHandlerRegister, base=ebp, index=NoIndex}} :: PopR wReg :: ResetStack 1 :: code) end | codeGenICode(BeginHandler {handleStart=ILabel hStart, workReg, packetReg} :: rest, code) = let val _ = asGenReg packetReg = eax orelse raise InternalError "codeGenICode: BeginHandler" val wReg = asGenReg workReg val labelRef = case Array.sub(labelArray, hStart) of HandlerLab addr => addr | _ => raise InternalError "codeGenICode: BeginHandler not handler" in (* The code here is almost the same as PopExceptionHandler. The only real difference is that PopExceptionHandler needs to pass the result of executing the handled code which could be in any register. This code needs to transmit the exception packet and that is always in rax. *) codeGenICode(rest, StoreRegToMemory{ toStore=wReg, address={offset=memRegHandlerRegister, base=ebp, index=NoIndex}} :: PopR wReg :: ResetStack 1 :: MoveToRegister{ source=MemoryArg{base=ebp, offset=memRegHandlerRegister, index=NoIndex}, output=esp } :: StartHandler{handlerLab=labelRef} :: code) end | codeGenICode(ReturnResultFromFunction { numStackArgs, ... } :: rest, code) = codeGenICode(rest, ReturnFromFunction numStackArgs :: code) | codeGenICode( ArithmeticFunction{ oper, resultReg=(GenReg resReg), operand1=RegisterArgument(GenReg op1Reg), operand2, ...} :: rest, code) = let val _ = resReg = op1Reg orelse raise InternalError "codeGenICode: ArithmeticFunction" in codeGenICode(rest, ArithToGenReg { opc=oper, output=resReg, source=sourceAsGenRegOrMem operand2 } :: code) end | codeGenICode(ArithmeticFunction _ :: _, _) = raise InternalError "codeGenICode: TODO codeGenICode - ArithmeticFunction" | codeGenICode(TestTagBit {arg, ...} :: rest, code) = codeGenICode(rest, TestTagR(argAsGenReg arg) :: code) | codeGenICode(PushValue { arg = RegisterArgument(GenReg r) } :: rest, code) = codeGenICode(rest, PushToStack(RegisterArg r) :: code) | codeGenICode(PushValue { arg = IntegerConstant v } :: rest, code) = codeGenICode(rest, PushToStack(NonAddressConstArg v) :: code) + | codeGenICode(PushValue { arg = AddressConstant v } :: rest, code) = + codeGenICode(rest, PushToStack(AddressConstArg v) :: code) + + | codeGenICode(PushValue { arg = StackLocation {adjustment, wordOffset} } :: rest, code) = + (* The X86 manual says that the address is computed before the push. *) + codeGenICode(rest, PushToStack(MemoryArg{base=esp, offset=(adjustment+wordOffset)*wordSize, index=NoIndex}) :: code) + | codeGenICode(PushValue _ :: _, _) = raise InternalError "codeGenICode: TODO PushValue" | codeGenICode(ResetStackPtr {numWords} :: rest, code) = ( numWords >= 0 orelse raise InternalError "codeGenICode: ResetStackPtr - negative offset"; codeGenICode(rest, ResetStack numWords :: code) ) | codeGenICode(TagValue _ :: _, _) = raise InternalError "codeGenICode: TODO TagValue" | codeGenICode(UntagValue _ :: _, _) = raise InternalError "codeGenICode: TODO UntagValue" | codeGenICode(LoadEffectiveAddress { base, offset, index, dest } :: rest, code) = let val bReg = Option.map asGenReg base val indexR = memoryIndexAsIndex index in codeGenICode(rest, LoadAddress{ output=asGenReg dest, offset=offset, base=bReg, index=indexR } :: code) end | codeGenICode( ShiftOperation{ shift, resultReg, operand, shiftAmount=IntegerConstant shiftValue, ...} :: rest, code) = let val resReg = asGenReg resultReg and opReg = argAsGenReg operand val _ = resReg = opReg orelse raise InternalError "codeGenICode: ShiftOperation" in codeGenICode(rest, ShiftConstant{ shiftType=shift, output=resReg, shift=Word8.fromLargeInt shiftValue } :: code) end | codeGenICode(ShiftOperation { shift, resultReg, operand, shiftAmount, ...} :: rest, code) = let val resReg = asGenReg resultReg and opReg = argAsGenReg operand val _ = resReg = opReg orelse raise InternalError "codeGenICode: ShiftOperation" (* The amount to shift must be in ecx. The shift is masked to 5 or 6 bits so we have to check for larger shift values at a higher level. *) val _ = argAsGenReg shiftAmount = ecx orelse raise InternalError "codeGenICode: ShiftOperation" in codeGenICode(rest, ShiftVariable{ shiftType=shift, output=resReg } :: code) end | codeGenICode(Multiplication { resultReg, operand1, operand2=MemoryLocation{offset, base, index=NoMemIndex}, ... } :: rest, code) = let val resReg = asGenReg resultReg and op1Reg = argAsGenReg operand1 and baseReg = asGenReg base val _ = resReg = op1Reg orelse raise InternalError "codeGenICode: Multiplication" in codeGenICode(rest, MultiplyRM { base=baseReg, offset=offset, output=resReg } :: code) end | codeGenICode(Multiplication { resultReg, operand1, operand2, ... } :: rest, code) = let val resReg = asGenReg resultReg and op1Reg = argAsGenReg operand1 and op2Reg = argAsGenReg operand2 val _ = resReg = op1Reg orelse raise InternalError "codeGenICode: Multiplication" in codeGenICode(rest, MultiplyRR { source=op2Reg, output=resReg } :: code) end | codeGenICode(Division { isSigned, dividend, divisor, quotient, remainder } :: rest, code) = let val dividendReg = asGenReg dividend and divisorReg = argAsGenReg divisor and quotientReg = asGenReg quotient and remainderReg = asGenReg remainder val _ = dividendReg = eax orelse raise InternalError "codeGenICode: Division" val _ = divisorReg <> eax andalso divisorReg <> edx orelse raise InternalError "codeGenICode: Division" val _ = quotientReg = eax orelse raise InternalError "codeGenICode: Division" val _ = remainderReg = edx orelse raise InternalError "codeGenICode: Division" (* rdx needs to be set to the high order part of the dividend. For signed division that means sign-extending rdx, for unsigned division we clear it. *) val setRDX = if isSigned then SignExtendForDivide else ArithToGenReg{ opc=XOR, output=edx, source=RegisterArg edx } in codeGenICode(rest, DivideAccR {arg=divisorReg, isSigned=isSigned} :: setRDX :: code) end | codeGenICode(AtomicExchangeAndAdd{ base, source } :: rest, code) = let val baseReg = asGenReg base and outReg = asGenReg source in codeGenICode(rest, AtomicXAdd{base=baseReg, output=outReg} :: code) end | codeGenICode(CompareByteVectors { vec1Addr, vec2Addr, length, ... } :: rest, code) = let (* The arguments must be in specific registers. *) val _ = asGenReg vec1Addr = esi orelse raise InternalError "CompareByteVectors: esi" val _ = asGenReg vec2Addr = edi orelse raise InternalError "CompareByteVectors: edi" val _ = asGenReg length = ecx orelse raise InternalError "CompareByteVectors: ecx" in codeGenICode(rest, RepeatOperation CMPSB :: code) end | codeGenICode(BlockMove { srcAddr, destAddr, length, isByteMove } :: rest, code) = let (* The arguments must be in specific registers. *) val _ = asGenReg srcAddr = esi orelse raise InternalError "BlockMove: esi" val _ = asGenReg destAddr = edi orelse raise InternalError "BlockMove: edi" val _ = asGenReg length = ecx orelse raise InternalError "BlockMove: ecx" in codeGenICode(rest, RepeatOperation(if isByteMove then MOVSB else MOVSL) :: code) end | codeGenICode( CompareFloatingPt { arg1=RegisterArgument(FPReg fpReg), arg2=MemoryLocation{offset, base=(GenReg baseReg), index=NoMemIndex}, ... } :: rest, code) = let val _ = fpReg = fp0 orelse raise InternalError "codeGenICode: CompareFloatingPt not fp0" (* This currently pops the value. *) (*val _ = fpMode = FPModeX87 orelse raise InternalError "codeGenICode: FCOMP in SSE2 mode"*) in codeGenICode(rest, FPArithMemory{opc=FCOMP, base=baseReg, offset=offset} :: code) end | codeGenICode(CompareFloatingPt {arg1=RegisterArgument(XMMReg xmmReg), arg2, ... } :: rest, code) = codeGenICode(rest, XMMArith { opc= SSE2Comp, output=xmmReg, source=sourceAsXMMRegOrMem arg2} :: code) | codeGenICode(CompareFloatingPt _ :: _, _) = raise InternalError "codeGenICode: CompareFloatingPt: TODO" | codeGenICode(X87FPGetCondition { dest, ... } :: rest, code) = let val _ = asGenReg dest = eax orelse raise InternalError "codeGenICode: GetFloatingPtCondition not eax" (* This currently pops the value. *) (*val _ = fpMode = FPModeX87 orelse raise InternalError "codeGenICode: FPStatusToEAX in SSE2 mode"*) in codeGenICode(rest, FPStatusToEAX :: code) end | codeGenICode( X87FPArith { opc, resultReg=(FPReg fpResReg), arg1=RegisterArgument(FPReg fpArgReg), arg2=MemoryLocation{offset, base=(GenReg baseReg), index=NoMemIndex} } :: rest, code) = let val _ = fpResReg = fp0 orelse raise InternalError "codeGenICode: FloatingPointArith not fp0" val _ = fpArgReg = fp0 orelse raise InternalError "codeGenICode: FloatingPointArith not fp0" in codeGenICode(rest, FPArithMemory{opc=opc, base=baseReg, offset=offset} :: code) end | codeGenICode(X87FPArith _ :: _, _) = raise InternalError "codeGenICode: X87FPArith: TODO" | codeGenICode( SSE2FPArith { opc, resultReg=(XMMReg xmmResReg), arg1=RegisterArgument(XMMReg xmmArgReg), arg2 } :: rest, code) = let val _ = xmmResReg = xmmArgReg orelse raise InternalError "codeGenICode: FloatingPointArith - different regs" in codeGenICode(rest, XMMArith{ opc=opc, output=xmmResReg, source=sourceAsXMMRegOrMem arg2} :: code) end | codeGenICode(SSE2FPArith _ :: _, _) = raise InternalError "codeGenICode: SSE2FPArith: TODO" | codeGenICode(X87FPUnaryOps {fpOp, dest=(FPReg fpResReg), source=RegisterArgument(FPReg fpArgReg)} :: rest, code) = let val _ = fpResReg = fp0 orelse raise InternalError "codeGenICode: X87FPUnaryOps not fp0" val _ = fpArgReg = fp0 orelse raise InternalError "codeGenICode: X87FPUnaryOps not fp0" in codeGenICode(rest, FPUnary fpOp :: code) end | codeGenICode(X87FPUnaryOps _ :: _, _) = raise InternalError "codeGenICode: FloatingPointNeg: TODO" | codeGenICode(FloatFixedInt { dest=(XMMReg xmmResReg), source=RegisterArgument(GenReg srcReg) } :: rest, code) = codeGenICode(rest, XMMConvertFromInt{ output=xmmResReg, source=srcReg} :: code) | codeGenICode(FloatFixedInt { dest=(FPReg fpReg), source=MemoryLocation{base, offset, index=NoMemIndex} } :: rest, code) = let val _ = fpReg = fp0 orelse raise InternalError "codeGenICode: FloatFixedInt not fp0" in codeGenICode(rest, FPLoadInt{ base=asGenReg base, offset=offset} :: code) end | codeGenICode(FloatFixedInt _ :: _, _) = raise InternalError "codeGenICode: FloatFixedInt: TODO" (* ReserveContainer should have been removed by earlier passes. *) | codeGenICode(ReserveContainer _ :: _, _) = raise InternalError "codeGenICode: ReserveContainer" (* BoxValue should have been removed by earlier passes. *) | codeGenICode(BoxValue _ :: _, _) = raise InternalError "codeGenICode: BoxValue" (* The stack limit register is set at least twice this far from the end of the stack so we can simply compare the stack pointer with the stack limit register if we need less than this much. Setting it at twice this value means that functions that use up to this much stack and do not call any other functions do not need to check the stack at all. *) (* TODO: The only functions that don't check the stack are RTS functions and any hand-coded functions. *) val minStackCheck = 20 (* Adds the constants onto the code, and copies the code into a new segment *) (* Prelude consists of stack checking code. *) fun testRegAndTrap(reg, entryPt) = let (* If we need to take the trap we save the argument and closure registers across the trap. *) val saveRegs = List.mapPartial(fn GenReg r => SOME r | _ => NONE) inputRegisters fun pushThenPop [] = [CallRTS entryPt] | pushThenPop (aReg::regs) = PushToStack(RegisterArg aReg) :: (pushThenPop regs @ [PopR aReg]) (* Normally we won't have a stack overflow so we will skip the check. *) fun condBranch(test, predict) = let val label as Labels{uses, ...} = mkLabel() in uses := 1; ([ConditionalBranch{test=test, predict=predict, label=label}], label) end val (skipCheck, skipCheckLab) = condBranch(JNB, PredictTaken) in [ArithToGenReg{ opc=CMP, output=reg, source=MemoryArg{offset=memRegStackLimit, base=ebp, index=NoIndex} }] @ skipCheck @ pushThenPop saveRegs @ [JumpLabel skipCheckLab] end val preludeCode = if stackRequired >= minStackCheck then let (* Compute the necessary amount in edi and compare that. *) val stackByteAdjust = ~wordSize * stackRequired val testEdiCode = testRegAndTrap (edi, memRegStackOverflowCallEx) in [LoadAddress{output=edi, base=SOME esp, index=NoIndex, offset=stackByteAdjust}] @ testEdiCode end else testRegAndTrap (esp, memRegStackOverflowCall) val newCode = codeCreate (functionName, profileObject, debugSwitches) val ops = codeGenICode(icode, []) in createCodeSegment(X86OPTIMISE.optimise(newCode, preludeCode @ List.rev ops), newCode) end structure Sharing = struct type genReg = genReg and 'reg argument = 'reg argument and iLabel = iLabel and 'reg x86ICode = 'reg x86ICode and branchOps = branchOps and reg = reg and abstract = abstract end end; diff --git a/mlsource/MLCompiler/CodeTree/X86Code/X86ICodeTransform.ML b/mlsource/MLCompiler/CodeTree/X86Code/X86ICodeTransform.ML index 53f70234..5693de83 100644 --- a/mlsource/MLCompiler/CodeTree/X86Code/X86ICodeTransform.ML +++ b/mlsource/MLCompiler/CodeTree/X86Code/X86ICodeTransform.ML @@ -1,3269 +1,3339 @@ (* Copyright David C. J. Matthews 2016 This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License version 2.1 as published by the Free Software Foundation. This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with this library; if not, write to the Free Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA *) functor X86ICodeTransform( structure ICODE: ICodeSig structure DEBUG: DEBUGSIG structure IDENTIFY: X86IDENTIFYREFSSIG structure PRETTY: PRETTYSIG + structure STRONGLY: sig type node val stronglyConnectedComponents: node list -> node list list end + where type node = {src: ICODE.reg ICODE.argument, stack: int} sharing ICODE.Sharing = IDENTIFY.Sharing ) : X86ICODETRANSFORMSIG = struct open ICODE open Address open IDENTIFY val totalFns = ref 0 and successFns = ref 0 val notDoneInstr = ref 0 and tooManyRegs = ref 0 and mustPushReg = ref 0 and anOther = ref 0 exception InternalError = Misc.InternalError (* tag a short constant *) fun tag c = 2 * c + 1 fun argAsPReg(RegisterArgument(PReg(n, PRegGeneral))) = n | argAsPReg _ = raise InternalError "argAsPReg" and argAsUReg(RegisterArgument(PReg(n, PRegUntagged))) = n | argAsUReg _ = raise InternalError "argAsUReg" fun pRegNum(PReg(n, PRegGeneral)) = n | pRegNum _ = raise InternalError "pRegNum" and uRegNum(PReg(n, PRegUntagged)) = n | uRegNum _ = raise InternalError "uRegNum" fun loadMemory(reg, base, offset) = [LoadArgument{ source=MemoryLocation{base=(GenReg base), offset=offset, index=NoMemIndex}, dest=GenReg reg, kind=MoveWord}] and loadStack(reg, offset) = loadMemory(reg, esp, offset) and storeMemory(reg, base, offset) = [StoreArgument{ source=RegisterArgument(GenReg reg), base=(GenReg base), offset=offset, index=NoMemIndex, kind=MoveWord}] val raxAsArg = (GenReg eax) and rbxAsArg = (GenReg ebx) and rcxAsArg = (GenReg ecx) and rsiAsArg = (GenReg esi) and rdxAsArg = (GenReg edx) and rdiAsArg = (GenReg edi) val generalRegisters = List.map GenReg (if isX64 then [r14, r13, r12, r11, r10, r9, r8, edi, esi, edx, ecx, ebx, eax] else [edi, esi, edx, ecx, ebx, eax]) (* Generally we have an offset in words and no index register. *) fun wordOffsetAddress(offset, baseReg) = MemoryLocation{offset=offset*wordSize, base=(GenReg baseReg), index=NoMemIndex} (* Transform the version of the ICode generated from the codetree by replacing the pseudo-registers by real locations. When this is complete it passes it on to the next phase for code-generation. This is currently very simple-minded and just uses rax as an accumulator and the stack for the rest. *) datatype pregLoc = InRax | OnStack of int (* The state of the condition codes. *) datatype ccState = CCIndeterminate | CCState of ccRef * (branchOps->branchOps) datatype state = NormalState of normalState | Exited withtype normalState = { valueStack : {preg: int, loc: pregLoc} list, ccState: ccState, untaggedRegs: {ureg: int, reg: reg} list } val initialState:normalState = {valueStack=[], ccState=CCIndeterminate, untaggedRegs=[]} (* Initial and final state. *) (* Return the location on the real stack immediately above the top item. *) local fun stackP [] = 0 | stackP ({loc=OnStack sp, ...} :: _) = sp+1 | stackP (_ :: stack) = stackP stack in fun stackPtr({valueStack, ...}: normalState) = stackP valueStack end local fun findE (_, []) = raise InternalError "findEntry: not found" | findE (reg, {preg, loc} :: rest) = if reg = preg then loc else findE(reg, rest) in fun findEntry(reg, {valueStack, ...}) = findE(reg, valueStack) end fun loadSource(RegisterArgument reg, dest, state) = loadRegister(reg: abstract, dest, state) | loadSource(AddressConstant a, dest, _) = [LoadArgument{ source=AddressConstant a, dest=GenReg dest, kind=MoveWord}] | loadSource(IntegerConstant i, dest, _) = [LoadArgument{ source=IntegerConstant i, dest=GenReg dest, kind=MoveWord}] | loadSource(MemoryLocation{ base, offset, index=NoMemIndex }, dest, state) = (* Use the destination register as a base address. *) LoadArgument { source=MemoryLocation {base=(GenReg dest), offset=offset, index=NoMemIndex }, dest=GenReg dest, kind=MoveWord} :: loadRegister(base, dest, state) | loadSource _ = raise InternalError "loadSource" and loadRegister(PReg(src, PRegGeneral), dest, state) = ( case findEntry (src, state) of InRax => if dest = eax then [] else [LoadArgument{ source=RegisterArgument(GenReg eax), dest=GenReg dest, kind=MoveWord}] | OnStack s => loadStack(dest, (stackPtr state - s - 1) * wordSize) ) | loadRegister _ = raise InternalError "loadRegister" val loadSource = fn(arg, dest, state as {valueStack={preg=_, loc=InRax } :: _, ...}) => if dest = eax then raise InternalError "loadSource: eax" else loadSource(arg, dest, state) | (arg, dest, state) => loadSource(arg, dest, state) fun clearCC({valueStack, untaggedRegs, ...}:normalState): normalState = {valueStack=valueStack, ccState=CCIndeterminate, untaggedRegs=untaggedRegs} (* After we use an untagged value remove it from the state. We only have a few registers and only use at most two untagged values before tagging them. For now, if we tag a value we clear the untagged set. Division returns two tagged values but only one is actually used. *) fun removeAfterTag({valueStack, ccState, ...}, _) = {valueStack=valueStack, ccState=ccState, untaggedRegs=[]} fun codeICodeFunctionToX86{icode, functionName, maxLabels, maxPRegs, argRegsUsed, hasFullClosure, currentStackArgs, debugSwitches} = let (* We may need to create additional labels. *) val labelCounter = ref maxLabels fun newLabel() = ILabel(!labelCounter) before labelCounter := !labelCounter + 1 val maxStack = ref 0 (* High-water mark *) (* If the top of the stack is in RAX push it otherwise do nothing. *) fun pushRax (state as {valueStack={preg, loc=InRax} :: stack, ccState, untaggedRegs }) = let val sp = stackPtr state val () = if sp >= !maxStack then maxStack := sp+1 else () in (* Return the updated state with the value pushed. Pushing does not affect condition codes. *) ({valueStack={preg=preg, loc=OnStack sp} :: stack, ccState=ccState, untaggedRegs=untaggedRegs}, [PushValue{arg=RegisterArgument raxAsArg}]) end | pushRax stack = (stack, []) (* Add a pseudo-register containing rax to the top of the stack. *) fun addRaxToState({valueStack, ccState, untaggedRegs}, destReg) = {valueStack={preg=destReg, loc=InRax} :: valueStack, ccState=ccState, untaggedRegs=untaggedRegs} (* Check that the top of the stack is the required pseudo-register and the value is in Rax. Returns the state with this item popped. *) fun checkTopInRax({valueStack={preg, loc=InRax } :: resultState, ccState, untaggedRegs}, checkReg) = if preg = checkReg then {valueStack=resultState, ccState=ccState, untaggedRegs=untaggedRegs} else raise InternalError "checkTopInRax" | checkTopInRax _ = raise InternalError "checkTopInRax" fun loadToRax(state, arg) = let val (pushedState, pushCode) = pushRax state val load = loadSource(arg, eax, pushedState) in (pushedState, load @ pushCode) end (* Reset the stack to value in the original state except that the target register should be moved into the result state. *) fun resetStack(state, oldState, target) = let (* Check that the target is on the top of the stack and in rax. *) val _ = checkTopInRax(state, target) (* Check that the top of the old state is not in a register. *) val () = case oldState of {valueStack={loc=InRax, ...} :: _, ...} => raise InternalError "resetStack" | _ => () val currentSp = stackPtr state and oldSp = stackPtr oldState val newState = addRaxToState(oldState, target) val code = if currentSp = oldSp then [] else [resetStackPtr(currentSp - oldSp)] in (* Currently ResetStackPtr uses arithmetic operations that affect the condition codes. *) (clearCC newState, code) end and resetStackPtr numWords = if numWords < 0 then raise InternalError "resetStackPtr" else ResetStackPtr{numWords=numWords} (* Find a real register for an untagged pseudo-register value. *) fun getUreg(iReg, {untaggedRegs, ...}: normalState) = case List.find (fn {ureg, ...} => ureg = iReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "getUreg" fun getFPreg(iReg, {untaggedRegs, ...}: normalState) = case List.find (fn {ureg, ...} => ureg = iReg) untaggedRegs of SOME {reg as XMMReg _, ...} => reg | SOME {reg as FPReg _, ...} => reg | _ => raise InternalError "getFPreg" (* Get a new untagged register. We only handle three at the moment. *) fun newUreg (iReg, {valueStack, untaggedRegs, ccState}: normalState) = let val newReg = case untaggedRegs of [] => edx | [_] => ecx | [_, _] => esi | _ => raise InternalError "newUreg" in ({valueStack=valueStack, ccState=ccState, untaggedRegs={ureg=iReg, reg=GenReg newReg}::untaggedRegs}, (GenReg newReg)) end (* Process the code until the end. The code list is built up in reverse order. *) (* If we reach the end we haven't exited or reached a JumpLoop so we just return the final state. *) fun codeICode{icode=[]: abstract x86ICode list, state: state, code: reg x86ICode list, ...} = (state, code: reg x86ICode list) (* Destination of a forward jump. If the state was Exited this can continue. We should have the label in the list. We need to merge the states associated with dropping through and the state associated with the branch. We can only adjust the state on the "drop through" side so if we need to change the state on the branch side we have to create a new branch. *) | codeICode{icode=(ForwardJumpLabel{label, result}: abstract x86ICode) :: rest, state, code: reg x86ICode list, context as {forwardLabels, loopArgs, handlers}} = let (* Find the label in the list. Remove it if it's there. It may not be if we never used it. That could happen if we have a "drop-through" case in an andalso/orelse or if we didn't generate a jump because we raised an exception or made a tail-jump. *) fun findAndRemoveLabel(label: iLabel, (hd as (l, _)) :: tl) = if label = l then (SOME hd, tl) else let val (found, newTail) = findAndRemoveLabel(label, tl) in (found, hd::newTail) end | findAndRemoveLabel _ = (NONE, []) val (labelCondition, newLabels) = findAndRemoveLabel(label, forwardLabels) in case (state, labelCondition) of (state, NONE) => (* We didn't actually take a branch. Discard the label and continue. *) codeICode{icode=rest, state=state, code=code, context={forwardLabels=newLabels, loopArgs=loopArgs, handlers=handlers}} | (Exited, SOME(_, labelState)) => (* There is no drop-through to consider because the preceding instruction was an unconditional jump or something similar. We can just set the state and continue. *) codeICode{icode=rest, state=NormalState labelState, code=ForwardJumpLabel{label=label, result=NONE} :: code, context={forwardLabels=newLabels, loopArgs=loopArgs, handlers=handlers}} | (NormalState cstate, SOME(_, labelState)) => (* There was a drop-through. Merge the states. We can only actually change the drop-through state i.e. before the label. If the state on the incoming branch needs to be changed we have to add an extra branch. *) let (* We should have the result register on both arms. *) fun removeResult s = case result of NONE => s | SOME resArg => checkTopInRax(s, pRegNum resArg) val dropThrough = removeResult cstate and labState = removeResult labelState (* After removing the top item the tails of the states will match up to the point they diverged. The common part is the resulting state. *) fun matchStates([], _) = [] | matchStates(_, []) = [] | matchStates((hd as {loc=loc1, preg=preg1})::l1, {loc=loc2, preg=preg2}::l2) = if preg1 <> preg2 then [] else if loc1 <> loc2 then raise InternalError "matchStates" else hd :: matchStates(l1, l2) val composite = {valueStack=List.rev(matchStates(List.rev (#valueStack dropThrough), List.rev (#valueStack labState))), ccState=CCIndeterminate, untaggedRegs= []} (* Currently the only thing we need to adjust is the stack pointer. *) val finalSp = stackPtr composite and labelSp = stackPtr labelState val (finalState, adjustSpOnDropThrough) = case result of NONE => let val currentSp = stackPtr cstate and finalSp = stackPtr composite in (composite, if currentSp = finalSp then [] else [resetStackPtr(currentSp-finalSp)]) end | SOME resReg => resetStack(cstate, composite, pRegNum resReg) in if labelSp = finalSp then (* We don't need to do anything to the incoming branch. *) let val newContext = {forwardLabels=newLabels, loopArgs=loopArgs, handlers=handlers} in codeICode{icode=rest, state=NormalState finalState, code=ForwardJumpLabel{label=label, result=NONE} :: adjustSpOnDropThrough @ code, context=newContext} end else (* We're going to have to adjust the stack pointer on the incoming branch. We can't actually do that so instead we have to branch and merge again. *) let val extraLabel = newLabel() in codeICode{ (* Put in an unconditional jump followed by the label we're currently trying to merge in. Because it's following an unconditional jump the state will simply be set to the label state. When we merge in again we will be able to adjust the stack pointer and it should all work. *) icode=UnconditionalForwardJump{label=extraLabel} :: ForwardJumpLabel{label=label, result=result} :: ForwardJumpLabel{label=extraLabel, result=result} :: rest, state=NormalState finalState, code=adjustSpOnDropThrough @ code, context=context (* Original context - we haven't fixed up the label yet. *)} end end end (* Start of a handler. This is similar to a ForwardLabel and should only occur in an Exited state. The handlers form a stack so the one we want should be on the top. *) | codeICode{ icode=(BeginHandler{handleStart, packetReg, ...}) :: rest, state=Exited, code, context={forwardLabels, loopArgs, handlers=(handleLab, handlerStartState) :: otherHandlers}} = let val _ = handleLab = handleStart orelse raise InternalError "codeICode: BeginHandler handler stack mismatch" val resultState = addRaxToState(handlerStartState, pRegNum packetReg) in codeICode{icode=rest, state=NormalState resultState, code=BeginHandler{handleStart=handleStart, workReg=rbxAsArg, packetReg=raxAsArg} :: code, context={forwardLabels=forwardLabels, loopArgs=loopArgs, handlers=otherHandlers}} end | codeICode{icode=BeginHandler _ :: _, ...} = raise InternalError "codeICode: BeginHandler not preceded by jump or not in handler" | codeICode{icode=EndLoop{loopLabel} :: rest, state, code, context={forwardLabels, loopArgs=(_, lab)::otherLoops, handlers}} = let val _ = lab = loopLabel orelse raise InternalError "codeICode: EndLoop - mismatched labels" in codeICode{icode=rest, state=state, code=code, context={forwardLabels=forwardLabels, loopArgs=otherLoops, handlers=handlers}} end | codeICode{icode=EndLoop _ :: _, ...} = raise InternalError "codeICode: EndLoop outside loop" (* Any other Exited conditions. Skip the instructions. There are various situations where this can arise. e.g. OS.Process.exit contains an infinite loop processing atExit functions until it eventually exits by calling a "stop" function. *) | codeICode{icode=_ :: rest, state=Exited, code, context} = codeICode{icode=rest, state=Exited, code=code, context=context} | codeICode{icode=(UnconditionalForwardJump{label}) :: rest, state=NormalState state, code, context={forwardLabels, loopArgs, handlers}} = codeICode{icode=rest, state=Exited, code=UnconditionalForwardJump{label=label} :: code, context={forwardLabels=(label, state) :: forwardLabels, loopArgs=loopArgs, handlers=handlers}} | codeICode{icode=ConditionalForwardJump{ccRef, condition, label} :: rest, state as NormalState labelState, code, context={forwardLabels, loopArgs, handlers}} = let (* Get the condition code. It should be the state we set but we may have to change the test if that wasn't the original. *) val testCondition = case labelState of {ccState=CCState(currentRef, condOp), ...} => if currentRef = ccRef then condOp condition else raise InternalError "codeICode: condition ref incorrect" | _ => raise InternalError "codeICode: condition ref unset" in codeICode{icode=rest, state=state, code=ConditionalForwardJump{ ccRef=ccRef, condition=testCondition, label=label } :: code, context={forwardLabels=(label, labelState) :: forwardLabels, loopArgs=loopArgs, handlers=handlers}} end (* Word comparison. *) | codeICode{icode=WordComparison{arg1 as RegisterArgument(PReg(_, PRegGeneral)), arg2=IntegerConstant i, ccRef} :: rest, state=NormalState state, code, context} = let (* The value on the top of the stack should be in rax and the value we want to test. *) val (startState, loadCode) = loadToRax(state, arg1) (* The resulting state contains the condition we want to test. *) val checkState = {valueStack= #valueStack startState, ccState=CCState(ccRef, fn i=>i), untaggedRegs= []} in codeICode{icode=rest, state=NormalState checkState, code=WordComparison{ arg1=RegisterArgument raxAsArg, arg2=IntegerConstant i, ccRef=ccRef } :: loadCode @ code, context=context} end | codeICode{icode=WordComparison{arg1 as RegisterArgument(PReg(_, PRegGeneral)), arg2=AddressConstant a, ccRef} :: rest, state=NormalState state, code, context} = let (* The value on the top of the stack should be in rax and the value we want to test. *) val (startState, loadCode) = loadToRax(state, arg1) val checkState = {valueStack= #valueStack startState, ccState=CCState(ccRef, fn i=>i), untaggedRegs= []} in codeICode{icode=rest, state=NormalState checkState, code=WordComparison{ arg1=RegisterArgument raxAsArg, arg2=AddressConstant a, ccRef=ccRef } :: loadCode @ code, context=context} end | codeICode{icode=WordComparison{arg1=RegisterArgument(PReg(testR1, PRegGeneral)), arg2 as RegisterArgument(PReg(_, PRegGeneral)), ccRef} :: rest, state=NormalState state, code, context=context} = let (* The second argument should be on the top of the stack and in rax. *) val (startState, loadCode) = loadToRax(state, arg2) val secondArg = case findEntry (testR1, startState) of OnStack s => s | _ => raise InternalError "codeICode: JumpOnWordComparison" (* We want the first argument in the register so that means the condition codes we will test are reversed.. *) fun revCond JA = JB | revCond JNA = JNB | revCond JB = JA | revCond JNB = JNA | revCond JL = JG | revCond JLE = JGE | revCond JG = JL | revCond JGE = JLE | revCond t = t val checkState = {valueStack= #valueStack startState, ccState=CCState(ccRef, revCond), untaggedRegs= []} in codeICode{icode=rest, state=NormalState checkState, code=WordComparison{arg1=RegisterArgument raxAsArg, arg2=wordOffsetAddress(stackPtr startState - secondArg - 1, esp), ccRef=ccRef} :: loadCode @ code, context=context} end | codeICode{ icode=WordComparison{ arg1=RegisterArgument(PReg(arg1Reg, PRegUntagged)), arg2=MemoryLocation{offset=offset2, base=bReg2, index=NoMemIndex}, ccRef} :: rest, state=NormalState state, code, context=context} = (* This is used for LargeWord comparisons. *) let val ({ valueStack, untaggedRegs, ...}, loadArg2Base) = loadToRax(state, RegisterArgument bReg2) val realArgReg = case List.find (fn {ureg, ...} => ureg = arg1Reg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: WordComparison" val resultState = {valueStack= valueStack, ccState=CCState(ccRef, fn i=>i), untaggedRegs= []} in codeICode{icode=rest, state=NormalState resultState, code= WordComparison{arg1=RegisterArgument realArgReg, arg2=MemoryLocation{offset=offset2, base=raxAsArg, index=NoMemIndex}, ccRef=ccRef} :: loadArg2Base @ code, context=context} end | codeICode{icode=WordComparison _ :: _, ...} = raise InternalError "codeICode: JumpOnWordComparison TODO" | codeICode{icode=TestTagBit{arg, ccRef} :: rest, state=NormalState state, code, context} = let (* The value on the top of the stack should be in rax and the value we want to test. *) val (startState, loadCode) = loadToRax(state, arg) val checkState = {valueStack= #valueStack startState, ccState=CCState(ccRef, fn i=>i), untaggedRegs= []} in codeICode{icode=rest, state=NormalState checkState, (* TestTagBit only sets the condition codes. It doesn't affect the register. *) code=TestTagBit{arg=RegisterArgument raxAsArg, ccRef=ccRef} :: loadCode @ code, context=context} end (* Set up an exception handler. *) | codeICode{icode=PushExceptionHandler{ handlerAddr, handleStart } :: rest, state=NormalState state, code, context={forwardLabels, loopArgs, handlers}} = let val sHandle = pRegNum handlerAddr val (pushedState, pushCode) = pushRax state val sp = stackPtr pushedState val thisHandler = (handleStart, pushedState) val startState = {valueStack={preg=sHandle, loc=OnStack(sp+1) (* Two words *)} :: #valueStack pushedState, ccState=CCIndeterminate, untaggedRegs= []} val newContext = {forwardLabels=forwardLabels, loopArgs=loopArgs, handlers=thisHandler :: handlers} in codeICode{icode=rest, state=NormalState startState, code=PushExceptionHandler{handlerAddr=raxAsArg, handleStart=handleStart} :: pushCode @ code, context=newContext} end (* Pop an exception handler at the end of a handled section. Executed if no exception has been raised. *) | codeICode{icode=PopExceptionHandler{ handlerAddr, resultReg, workReg=_ } :: rest, state=NormalState state, code, context} = let val handleAddr = pRegNum handlerAddr (* handlerStartState is the state BEFORE we pushed the handler. *) (* Search down the state until we find the handler. *) fun popState [] = raise InternalError "codeICode: PopExceptionHandler - not found" | popState (hState as ({preg, ...} :: tail)) = if preg = handleAddr then hState else popState tail val handlerStartState = {valueStack=popState(#valueStack state), ccState=CCIndeterminate, untaggedRegs= []} (* Reset to just above the handler. The result state is after the handler has been popped. *) val postPopState = {valueStack=tl(#valueStack handlerStartState), ccState=CCIndeterminate, untaggedRegs= []} val (resultState, resetCode) = case resultReg of SOME(PReg(resReg, _)) => let val (_, resetCode) = resetStack(state, handlerStartState, resReg) val resultState = addRaxToState(postPopState, resReg) in (resultState, resetCode) end | NONE => (postPopState, [resetStackPtr(stackPtr state - stackPtr handlerStartState)]) val workReg = (GenReg ebx) (* Must be different from the return register. *) in codeICode{icode=rest, state=NormalState resultState, code=PopExceptionHandler{ handlerAddr=raxAsArg (* unused*), resultReg=NONE (* unused*), workReg=workReg } :: resetCode @ code, context=context} end (* Create a new Preg containing the contents of another Preg. We only ever want the top item to be in RAX so we push the top of the stack. *) | codeICode{ icode=LoadArgument{source as RegisterArgument(PReg(_, PRegGeneral)), dest=PReg(destReg, PRegGeneral), kind=MoveWord} :: rest, state=NormalState state, code, context} = let val (pushedState, pushCode) = pushRax state val load = loadSource(source, eax, pushedState) in codeICode{ icode=rest, state=NormalState(addRaxToState(pushedState, destReg)), code=load @ pushCode @ code, context=context} end (* Move a constant to a preg. First push anything in RAX then load the constant into RAX. *) | codeICode{icode=LoadArgument{source=AddressConstant srcValue, dest=PReg(destReg, PRegGeneral), kind} :: rest, state=NormalState state, code, context} = let val (pushedState, pushCode) = pushRax state (* The constant should be an address. *) val _ = isShort srcValue andalso raise InternalError "AddressConstant: short" in codeICode{ icode=rest, state=NormalState(addRaxToState(pushedState, destReg)), code=LoadArgument{source=AddressConstant srcValue, dest=raxAsArg, kind=kind} :: pushCode @ code, context=context} end (* Move a short constant to a preg. First push anything in RAX then load the constant into RAX. *) | codeICode{icode=LoadArgument{source=IntegerConstant i, dest=PReg(destReg, PRegGeneral), kind} :: rest, state=NormalState state, code, context} = let val (pushedState, pushCode) = pushRax state in codeICode{ icode=rest, state=NormalState(addRaxToState(pushedState, destReg)), code=LoadArgument{source=IntegerConstant i, dest=raxAsArg, kind=kind} :: pushCode @ code, context=context} end (* Move a short constant to an untagged reg. *) | codeICode{icode=LoadArgument{source=IntegerConstant i, dest=PReg(destReg, PRegUntagged), kind} :: rest, state=NormalState state, code, context} = let val (resultState, resReg) = newUreg(destReg, state) in codeICode{ icode=rest, state=NormalState resultState, code=LoadArgument{source=IntegerConstant i, dest=resReg, kind=kind} :: code, context=context} end (* Load a value from a piece of memory, typically the offset in a tuple. *) | codeICode{ icode=LoadArgument{ source=MemoryLocation{offset, base as PReg(_, PRegGeneral), index=NoMemIndex}, dest=PReg(destReg, dType), kind} :: rest, state=NormalState state, code, context} = let (* This previously replaced the top. Pushing the previous value is safer but means values accumulate on the stack. *) val (pushedState, pushCode) = pushRax state val load = loadSource(RegisterArgument base, eax, pushedState) val (resultState, resultReg) = case dType of PRegGeneral => (addRaxToState(pushedState, destReg), raxAsArg) | PRegUntagged => newUreg(destReg, pushedState) in codeICode{icode=rest, state=NormalState resultState, code=LoadArgument{ source=MemoryLocation{offset=offset, base=raxAsArg, index=NoMemIndex}, dest=resultReg, kind=kind} :: load @ pushCode @ code, context=context} end | codeICode{ icode=LoadArgument{ source=MemoryLocation{offset, base=PReg(bReg, PRegUntagged), index=NoMemIndex}, dest=PReg(destReg, dType), kind} :: rest, state=NormalState(state as {untaggedRegs, ...}), code, context} = let (* CMem loads with a fixed offset *) val realBReg = case List.find (fn {ureg, ...} => ureg = bReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: find tagged" val (resultState, resultReg) = case (dType, kind, fpMode) of (PRegUntagged, MoveFloat, FPModeX87) => ({valueStack= #valueStack state, ccState= #ccState state, untaggedRegs =[{ureg=destReg, reg=FPReg fp0}]}, (FPReg fp0)) | (PRegUntagged, MoveFloat, FPModeSSE2) => ({valueStack= #valueStack state, ccState= #ccState state, untaggedRegs =[{ureg=destReg, reg=XMMReg xmm0}]}, (XMMReg xmm0)) | (PRegUntagged, MoveDouble, FPModeX87) => ({valueStack= #valueStack state, ccState= #ccState state, untaggedRegs =[{ureg=destReg, reg=FPReg fp0}]}, (FPReg fp0)) | (PRegUntagged, MoveDouble, FPModeSSE2) => ({valueStack= #valueStack state, ccState= #ccState state, untaggedRegs =[{ureg=destReg, reg=XMMReg xmm0}]}, (XMMReg xmm0)) | (PRegGeneral, MoveFloat, _) => raise InternalError "MoveFloat to normal register" | (PRegGeneral, MoveDouble, _) => raise InternalError "MoveDouble to normal register" | (PRegGeneral, _, _) => (addRaxToState(state, destReg), raxAsArg) | (PRegUntagged, _, _) => newUreg(destReg, state) in codeICode{icode=rest, state=NormalState resultState, code=LoadArgument{ source=MemoryLocation{offset=offset, base=realBReg, index=NoMemIndex}, dest=resultReg, kind=kind} :: code, context=context} end | codeICode{ icode=LoadArgument{ source=MemoryLocation {offset, base, index=MemIndex1(PReg(iReg, PRegUntagged))}, dest=PReg(destReg, dType), kind} :: rest, state=NormalState (state as {untaggedRegs, ...}), code, context} = let (* The index is an untagged value. *) val realIReg = case List.find (fn {ureg, ...} => ureg = iReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: find tagged" (* The base may be a tagged or untagged register. CMem loads extract the base address from a LargeWord.word boxed value into an untagged register. *) val (realBReg, codeBreg) = case base of PReg(bReg, PRegGeneral) => let val baseOnStack = case findEntry (bReg, state) of OnStack s => s | _ => raise InternalError "codeICode: MoveArgument" val code = [LoadArgument{source=wordOffsetAddress(stackPtr state - baseOnStack - 1, esp), dest=rbxAsArg, kind=MoveWord}] in (rbxAsArg, code) end | PReg(bReg, PRegUntagged) => let val realBReg = case List.find (fn {ureg, ...} => ureg = bReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: find tagged" in (realBReg, []) end val (resultState, resultReg) = case dType of PRegGeneral => (addRaxToState(state, destReg), raxAsArg) | PRegUntagged => ({valueStack= #valueStack state, ccState= #ccState state, untaggedRegs =[{ureg=destReg, reg=GenReg ecx}]}, rcxAsArg) in codeICode{icode=rest, state=NormalState resultState, code = LoadArgument{source=MemoryLocation {offset=offset, base=realBReg, index=MemIndex1 realIReg}, dest=resultReg, kind=kind} :: codeBreg @ code, context=context} end | codeICode{ icode=LoadArgument{ source=MemoryLocation {offset, base, index}, dest=PReg(destReg, dType), kind} :: rest, state=NormalState state, code, context} = let (* CMem operations will have pushed the index. The easiest way to proceed is always to do that. *) val (pushedState as { untaggedRegs, ...}, pushCode) = pushRax state val (iReg, indexed) = case index of MemIndex1 indexArg => (indexArg, MemIndex1 raxAsArg) | MemIndex2 indexArg => (indexArg, MemIndex2 raxAsArg) | MemIndex4 indexArg => (indexArg, MemIndex4 raxAsArg) | MemIndex8 indexArg => (indexArg, MemIndex8 raxAsArg) | _ => raise InternalError "codeICode: MemIndex" val (realBReg, codeBreg) = case base of PReg(_, PRegGeneral) => (rbxAsArg, loadSource(RegisterArgument base, ebx, pushedState)) | PReg(bReg, PRegUntagged) => let val realBReg = case List.find (fn {ureg, ...} => ureg = bReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: find tagged" in (realBReg, []) end val loadCode = codeBreg @ loadSource(RegisterArgument iReg, eax, pushedState) val (resultState, resultReg) = case (dType, kind, fpMode) of (PRegUntagged, MoveFloat, FPModeX87) => ({valueStack= #valueStack pushedState, ccState= #ccState pushedState, untaggedRegs =[{ureg=destReg, reg=FPReg fp0}]}, (FPReg fp0)) | (PRegUntagged, MoveFloat, FPModeSSE2) => ({valueStack= #valueStack pushedState, ccState= #ccState pushedState, untaggedRegs =[{ureg=destReg, reg=XMMReg xmm0}]}, (XMMReg xmm0)) | (PRegUntagged, MoveDouble, FPModeX87) => ({valueStack= #valueStack pushedState, ccState= #ccState pushedState, untaggedRegs =[{ureg=destReg, reg=FPReg fp0}]}, (FPReg fp0)) | (PRegUntagged, MoveDouble, FPModeSSE2) => ({valueStack= #valueStack pushedState, ccState= #ccState pushedState, untaggedRegs =[{ureg=destReg, reg=XMMReg xmm0}]}, (XMMReg xmm0)) | (PRegGeneral, MoveFloat, _) => raise InternalError "MoveFloat to normal register" | (PRegGeneral, MoveDouble, _) => raise InternalError "MoveDouble to normal register" | (PRegGeneral, _, _) => (addRaxToState(pushedState, destReg), raxAsArg) | (PRegUntagged, _, _) => ({valueStack= #valueStack pushedState, ccState= #ccState pushedState, untaggedRegs =[{ureg=destReg, reg=GenReg ecx}]}, rcxAsArg) in codeICode{icode=rest, state=NormalState resultState, code = LoadArgument{source=MemoryLocation {offset=offset, base=realBReg, index=indexed}, dest=resultReg, kind=kind} :: loadCode @ pushCode @ code, context=context} end - | codeICode{icode=LoadArgument{ source=StackLocation{offset, ...}, dest, kind=MoveWord} :: rest, state=NormalState state, code, context} = + | codeICode{icode=LoadArgument{ source=StackLocation{wordOffset, ...}, dest, kind=MoveWord} :: rest, state=NormalState state, code, context} = (* Load from the stack *) let val destReg = pRegNum dest val (pushedState, pushCode) = pushRax state (* We have to adjust the offset. *) - val load = loadStack(eax, stackPtr pushedState * wordSize + offset) + val load = loadStack(eax, (stackPtr pushedState + wordOffset) * wordSize) in codeICode{icode=rest, state=NormalState(addRaxToState(pushedState, destReg)), code=load @ pushCode @ code, context=context} end (* Store a pseudo-register in a memory location. *) | codeICode{ icode=StoreArgument{ source=RegisterArgument(PReg(valueReg, PRegUntagged)), offset, base as PReg(_, PRegGeneral), index=NoMemIndex, kind} :: rest, state=NormalState state, code, context} = let val (pushedState as { valueStack, ccState, untaggedRegs}, pushCode) = pushRax state val baseOnStack = case findEntry (pRegNum base, pushedState) of OnStack s => s | _ => raise InternalError "codeICode: MoveArgument" val realVReg = case List.find (fn {ureg, ...} => ureg = valueReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: find tagged" val loadBaseToEax = loadStack(eax, (stackPtr pushedState - baseOnStack -1) * wordSize) val store = [StoreArgument{ source=RegisterArgument realVReg, base=(GenReg eax), offset=offset, index=NoMemIndex, kind=kind}] val resultState = { valueStack= valueStack, ccState=ccState, untaggedRegs=[]} in codeICode{ icode=rest, state=NormalState resultState, code=store @ loadBaseToEax @ pushCode @ code, context=context} end (* As above except the base register is in an untagged register. This is used for CMem stores. *) | codeICode{ icode=StoreArgument{ source=RegisterArgument(PReg(valueReg, PRegUntagged)), offset, base=PReg(bReg, PRegUntagged), index=NoMemIndex, kind} :: rest, state=NormalState{untaggedRegs, valueStack, ccState, ...}, code, context} = let (* CMem loads with a fixed offset *) val realBReg = case List.find (fn {ureg, ...} => ureg = bReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: find tagged" val realVReg = case List.find (fn {ureg, ...} => ureg = valueReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: find tagged" val store = [StoreArgument{ source=RegisterArgument realVReg, base=realBReg, offset=offset, index=NoMemIndex, kind=kind}] val resultState = { valueStack= valueStack, ccState=ccState, untaggedRegs=[]} in codeICode{ icode=rest, state=NormalState resultState, code=store @ code, context=context} end (* Store an untagged register in a memory location. This is currently used to store the string length word. *) | codeICode{icode=StoreArgument{ source=RegisterArgument(PReg(srcReg, PRegGeneral)), offset, base, index=NoMemIndex, kind} :: rest, state=NormalState state, code, context} = let val (pushedState, pushCode) = pushRax state val baseOnStack = case findEntry (pRegNum base, pushedState) of OnStack s => s | _ => raise InternalError "codeICode: MoveArgument" val valueOnStack = case findEntry (srcReg, pushedState) of OnStack s => s | _ => raise InternalError "codeICode: MoveArgument" val loadValueToEbx = loadStack(ebx, (stackPtr pushedState - valueOnStack -1) * wordSize) val loadBaseToEax = loadStack(eax, (stackPtr pushedState - baseOnStack -1) * wordSize) (* Pop the value to store into ebx and store it in the tuple. *) val store = [StoreArgument{ source=RegisterArgument(GenReg ebx), base=(GenReg eax), offset=offset, index=NoMemIndex, kind=kind}] in codeICode{ icode=rest, state=NormalState pushedState, code=store @ loadBaseToEax @ loadValueToEbx @ pushCode @ code, context=context} end (* Store a constant in memory. *) | codeICode{icode=StoreArgument{ source=AddressConstant value, offset, base, index=NoMemIndex, kind} :: rest, state=NormalState state, code, context} = let val (pushedState, pushCode) = pushRax state val baseOnStack = case findEntry (pRegNum base, pushedState) of OnStack s => s | _ => raise InternalError "codeICode: MoveArgument" val loadBaseToEax = loadStack(eax, (stackPtr pushedState - baseOnStack -1) * wordSize) val store = [StoreArgument{ source=AddressConstant value, base=(GenReg eax), offset=offset, index=NoMemIndex, kind=kind}] in codeICode{ icode=rest, state=NormalState pushedState, code=store @ loadBaseToEax @ pushCode @ code, context=context} end (* Store a constant in memory. *) | codeICode{icode=StoreArgument{ source=IntegerConstant value, offset, base, index=NoMemIndex, kind} :: rest, state=NormalState state, code, context} = let val (pushedState, pushCode) = pushRax state val baseOnStack = case findEntry (pRegNum base, pushedState) of OnStack s => s | _ => raise InternalError "codeICode: MoveArgument" val loadBaseToEax = loadStack(eax, (stackPtr pushedState - baseOnStack -1) * wordSize) val store = [StoreArgument{ source=IntegerConstant value, base=(GenReg eax), offset=offset, index=NoMemIndex, kind=kind}] in codeICode{ icode=rest, state=NormalState pushedState, code=store @ loadBaseToEax @ pushCode @ code, context=context} end | codeICode{icode=StoreArgument{ source=RegisterArgument(PReg(valueReg, PRegGeneral)), offset, base, index, kind} :: rest, state=NormalState state, code, context} = let (* The top of the stack should be the value to store. That will be in rax. We load the base address into rcx and the index into rbx. *) val startState = checkTopInRax(state, valueReg) val (iReg, indexed) = case index of MemIndex1(PReg(r, PRegGeneral)) => (r, MemIndex1 rbxAsArg) | MemIndex2(PReg(r, PRegGeneral)) => (r, MemIndex2 rbxAsArg) | MemIndex4(PReg(r, PRegGeneral)) => (r, MemIndex4 rbxAsArg) | MemIndex8(PReg(r, PRegGeneral)) => (r, MemIndex8 rbxAsArg) | _ => raise InternalError "codeICode: MemIndex" val indexOnStack = case findEntry (iReg, state) of OnStack s => s | _ => raise InternalError "codeICode: MoveArgument" val baseOnStack = case findEntry (pRegNum base, state) of OnStack s => s | _ => raise InternalError "codeICode: MoveArgument" val rcxAsArg = (GenReg ecx) in codeICode{icode=rest, state=NormalState startState, code = StoreArgument{source=RegisterArgument raxAsArg, offset=offset, base=rcxAsArg, index=indexed, kind=kind} :: LoadArgument{source=wordOffsetAddress(stackPtr state - baseOnStack - 1, esp), dest=rcxAsArg, kind=MoveWord} :: LoadArgument{source=wordOffsetAddress(stackPtr state - indexOnStack - 1, esp), dest=rbxAsArg, kind=MoveWord} :: code, context=context} end | codeICode{icode= StoreArgument{ source=RegisterArgument(PReg(valueReg, PRegUntagged)), offset, base, index=MemIndex1(PReg(iReg, PRegUntagged)), kind} :: rest, state=NormalState state, code, context} = let (* This is used for index stores of bytes. N.B. If we're storing a byte from a register we must not use ESI or EDI for the value register in 32-bit mode. That's because the encoding actually refers to DH and BH. In 64-bit mode the REX prefix overrides this. *) val ({ valueStack, ccState, untaggedRegs}, pushCode) = pushRax state (* The index is an untagged value. *) val realIReg = case List.find (fn {ureg, ...} => ureg = iReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: find tagged" val realVReg = case List.find (fn {ureg, ...} => ureg = valueReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: find tagged" (* The base may be a tagged or untagged register. CMem stores extract the base address from a LargeWord.word boxed value into an untagged register. *) val (realBReg, codeBreg) = case base of PReg(bReg, PRegGeneral) => let val baseOnStack = case findEntry (bReg, state) of OnStack s => s | _ => raise InternalError "codeICode: MoveArgument" val code = [LoadArgument{source=wordOffsetAddress(stackPtr state - baseOnStack - 1, esp), dest=rbxAsArg, kind=MoveWord}] in (rbxAsArg, code) end | PReg(bReg, PRegUntagged) => let val realBReg = case List.find (fn {ureg, ...} => ureg = bReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: find tagged" in (realBReg, []) end val resultState = { valueStack= valueStack, ccState=ccState, untaggedRegs=[]} in codeICode{icode=rest, state=NormalState resultState, code = StoreArgument{source=RegisterArgument realVReg, offset=offset, base=realBReg, index=MemIndex1 realIReg, kind=kind} :: codeBreg @ pushCode @ code, context=context} end | codeICode{icode= StoreArgument{ source=RegisterArgument(PReg(valueReg, PRegUntagged)), offset, base, index, kind} :: rest, state=NormalState state, code, context} = (* Store an untagged value with an index value in a tagged register. This is used for CMem stores. *) let val (pushedState as { untaggedRegs, valueStack, ccState, ...}, pushCode) = pushRax state val (iReg, indexed) = case index of MemIndex1 indexArg => (indexArg, MemIndex1 raxAsArg) | MemIndex2 indexArg => (indexArg, MemIndex2 raxAsArg) | MemIndex4 indexArg => (indexArg, MemIndex4 raxAsArg) | MemIndex8 indexArg => (indexArg, MemIndex8 raxAsArg) | _ => raise InternalError "codeICode: MemIndex" (* The base address will be in an untagged register. *) val (realBReg, codeBreg) = case base of PReg(_, PRegGeneral) => (rbxAsArg, loadSource(RegisterArgument base, ebx, pushedState)) | PReg(bReg, PRegUntagged) => let val realBReg = case List.find (fn {ureg, ...} => ureg = bReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: find tagged" in (realBReg, []) end val realVReg = case List.find (fn {ureg, ...} => ureg = valueReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: find tagged" val loadCode = codeBreg @ loadSource(RegisterArgument iReg, eax, pushedState) val resultState = { valueStack= valueStack, ccState=ccState, untaggedRegs=[]} in codeICode{icode=rest, state=NormalState resultState, code = StoreArgument{source=RegisterArgument realVReg, offset=offset, base=realBReg, index=indexed, kind=kind} :: loadCode @ pushCode @ code, context=context} end | codeICode{icode= StoreArgument{ source=MemoryLocation {offset=srcOffset, base=srcBase, index=NoMemIndex}, offset, base=PReg(bReg, PRegUntagged), index=NoMemIndex, kind} :: rest, state=NormalState state, code, context} = let (* This is used to store floating point values into C memory. The source will be a PReg and the base will be an untagged register. *) val _ = kind = MoveFloat orelse kind = MoveDouble orelse raise InternalError "Move memory to memory - not float" val (pushedState as { untaggedRegs, valueStack, ccState, ...}, pushCode) = pushRax state val loadArgAddr = loadSource(RegisterArgument srcBase, ebx, pushedState) val resultReg = case fpMode of FPModeX87 => (FPReg fp0) | FPModeSSE2 => (XMMReg xmm0) val loadToFpReg = LoadArgument{ source=MemoryLocation{offset=srcOffset, base=rbxAsArg, index=NoMemIndex}, dest=resultReg, kind=MoveDouble} (* The base address will be in an untagged register. *) val realBReg = case List.find (fn {ureg, ...} => ureg = bReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: find tagged" val storeToMem = StoreArgument { source=RegisterArgument resultReg, offset=offset, base=realBReg, index=NoMemIndex, kind=kind} val resultState = { valueStack= valueStack, ccState=ccState, untaggedRegs=[]} val cvtToFloat = case (fpMode, kind) of (FPModeSSE2, MoveFloat) => [SSE2FPArith { opc=SSE2DoubleToFloat, resultReg=resultReg, arg1=RegisterArgument resultReg, arg2=RegisterArgument resultReg }] | _ => [] in codeICode{icode=rest, state=NormalState resultState, code = storeToMem :: cvtToFloat @ (loadToFpReg :: loadArgAddr @ pushCode @ code), context=context} end | codeICode{icode= StoreArgument{ source=MemoryLocation {offset=srcOffset, base=srcBase, index=NoMemIndex}, offset, base=PReg(bReg, PRegUntagged), index, kind} :: rest, state=NormalState state, code, context} = let (* This is used to store floating point values into C memory. The source will be a PReg and the base will be an untagged register. The index will be a tagged register. *) val _ = kind = MoveFloat orelse kind = MoveDouble orelse raise InternalError "Move memory to memory - not float" val (pushedState as { untaggedRegs, valueStack, ccState, ...}, pushCode) = pushRax state val loadArgAddr = loadRegister(srcBase, ebx, pushedState) val resultReg = case fpMode of FPModeX87 => (FPReg fp0) | FPModeSSE2 => (XMMReg xmm0) val loadToFpReg = LoadArgument{ source=MemoryLocation{offset=srcOffset, base=rbxAsArg, index=NoMemIndex}, dest=resultReg, kind=MoveDouble} val (iReg, indexed) = case index of MemIndex1 indexArg => (indexArg, MemIndex1 raxAsArg) | MemIndex2 indexArg => (indexArg, MemIndex2 raxAsArg) | MemIndex4 indexArg => (indexArg, MemIndex4 raxAsArg) | MemIndex8 indexArg => (indexArg, MemIndex8 raxAsArg) | _ => raise InternalError "codeICode: MemIndex - move float" (* The base address will be in an untagged register. *) val realBReg = case List.find (fn {ureg, ...} => ureg = bReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: find tagged" val cvtToFloat = case (fpMode, kind) of (FPModeSSE2, MoveFloat) => [SSE2FPArith { opc=SSE2DoubleToFloat, resultReg=resultReg, arg1=RegisterArgument resultReg, arg2=RegisterArgument resultReg }] | _ => [] val storeToMem = StoreArgument { source=RegisterArgument resultReg, offset=offset, base=realBReg, index=indexed, kind=kind} val resultState = { valueStack= valueStack, ccState=ccState, untaggedRegs=[]} in codeICode{icode=rest, state=NormalState resultState, code = storeToMem :: cvtToFloat @ loadRegister(iReg, eax, pushedState) @ (loadToFpReg :: loadArgAddr @ pushCode @ code), context=context} end (* Other combinations of move aren't used at the moment. *) | codeICode{icode=LoadArgument _ :: _, ...} = raise InternalError "codeICode: LoadArgument" | codeICode{icode=StoreArgument _ :: _, ...} = raise InternalError "codeICode: StoreArgument" | codeICode{ icode=LoadMemReg{offset, dest} :: rest, state=NormalState state, code, context} = (* Load from ebp/rbp *) let val destReg = pRegNum dest val (pushedState, pushCode) = pushRax state val load = loadMemory(eax, ebp, offset) in (* We also generate loads from offsets in ebp. *) codeICode{icode=rest, state=NormalState(addRaxToState(pushedState, destReg)), code=load @ pushCode @ code, context=context} end | codeICode { icode=BeginFunction{regArgs} :: rest, state=NormalState state, code, context} = let fun pushRegister([], state , code) = (state, code) | pushRegister((dest, srcReg)::others, state, code) = let val destReg = pRegNum dest val sp = stackPtr state val {valueStack, ccState, untaggedRegs, ...} = state val newState = {valueStack={preg=destReg, loc=OnStack sp} :: valueStack, ccState=ccState, untaggedRegs=untaggedRegs} in pushRegister(others, newState, PushValue{arg=RegisterArgument srcReg} :: code) end val (pushedState, pushCode) = pushRax state val (resultState, resultCode) = pushRegister(regArgs, pushedState, pushCode @ code) in codeICode{icode=rest, state=NormalState resultState, code=resultCode, context=context} end | codeICode{icode=AllocateMemoryOperation{ size, flags, dest, saveRegs=_} :: rest, state=NormalState state, code, context} = let val destReg = pRegNum dest val (pushedState, pushCode) = pushRax state val resultState = clearCC(addRaxToState(pushedState, destReg)) (* Affects CC *) in codeICode{ icode=rest, state=NormalState resultState, code=AllocateMemoryOperation{ size=size, flags=flags, dest=raxAsArg, saveRegs=[]} :: pushCode @ code, context=context} end | codeICode{icode=AllocateMemoryVariable{ size, dest, saveRegs=_} :: rest, state=NormalState state, code, context} = let (* Allocate memory without initialisation. Used for byte segments that don't need to be initialised. *) val destReg = pRegNum dest val (pushedState, pushCode) = pushRax state val loadSize = loadSource(RegisterArgument size, edx, pushedState) (* We put the size in rdx, the flags in rax and the result in rdi. *) val allocMem = [AllocateMemoryVariable{size=rdxAsArg, dest=rdiAsArg, saveRegs=[]}] val moveToRAX = [LoadArgument{source=RegisterArgument rdiAsArg, dest=raxAsArg, kind=MoveWord}] val resultState = clearCC(addRaxToState(pushedState, destReg)) in codeICode{ icode=rest, state=NormalState resultState, code= moveToRAX @ allocMem @ loadSize @ pushCode @ code, context=context} end | codeICode{icode=InitialiseMem{ size, addr, init} :: rest, state=NormalState state, code, context} = let val (pushedState as { untaggedRegs, valueStack, ...}, pushCode) = pushRax state val sizeReg = uRegNum size val realSReg = case List.find (fn {ureg, ...} => ureg = sizeReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: find untagged" val loadSize = [LoadArgument{source=RegisterArgument realSReg, dest=rcxAsArg, kind=MoveWord}] val loadInit = loadSource(RegisterArgument init, eax, pushedState) val loadAddr = loadSource(RegisterArgument addr, edi, pushedState) val initMem = [InitialiseMem{size=rcxAsArg, addr=rdiAsArg, init=raxAsArg}] val resultState = {valueStack=valueStack, untaggedRegs=[], ccState=CCIndeterminate} in codeICode{ icode=rest, state=NormalState resultState, code= initMem @ loadAddr @ loadInit @ loadSize @ pushCode @ code, context=context} end (* Marks the end of setting the fields of a tuple. This is used in the next level to avoid reordering a new allocation until a previously allocated section of memory has been fully initialised. *) | codeICode{icode=(InitialisationComplete _) :: rest, state, code, context} = codeICode{icode=rest, state=state, code=InitialisationComplete{dest=raxAsArg (* unused *)} :: code, context=context} (* Function call. *) | codeICode{icode=FunctionCall{ regArgs, stackArgs, dest, callKind} :: rest, state=NormalState state, code, context} = let val destReg = pRegNum dest val (pushedState, pushCode) = pushRax state (* In an earlier version we assumed that the values were actually pushed to the stack in sequence. That's no longer true. Explicitly push the stack arguments. *) local fun pushAllArgs ([], state, code) = (state, code) | pushAllArgs (arg::args, state as {valueStack, ccState, untaggedRegs}, code) = let (* TODO: We can push constants and memory addresses directly without loading them into a register. *) val load = loadSource(arg, eax, state) val sp = stackPtr state val newState = {valueStack={preg= ~1, loc=OnStack sp} :: valueStack, ccState=ccState, untaggedRegs=untaggedRegs} in pushAllArgs(args, newState, PushValue{arg=RegisterArgument raxAsArg} :: load @ code) end in val (afterArgs, argCode) = pushAllArgs (stackArgs, pushedState, []) end (* Move the register arguments into the correct real registers. *) fun asGenReg(GenReg r) = r | asGenReg _ = raise InternalError "asGenReg" val doLoad = List.foldl (fn ((pr, gr), l) => l @ loadSource(pr, asGenReg gr, afterArgs)) [] regArgs (* After the call the stack arguments will have been removed by the caller. *) val returnState = addRaxToState({valueStack= #valueStack pushedState, ccState= CCIndeterminate, untaggedRegs=[]}, destReg) val functionCode = FunctionCall{regArgs=[], stackArgs=[], dest=raxAsArg, callKind=callKind} :: doLoad @ argCode @ pushCode @ code in codeICode{icode=rest, state=NormalState returnState, code=functionCode, context=context} end (* Jump to a function. The arguments have to be moved into the space currently used by the arguments to this function. That could result in values being overwritten so we have to save them, especially the return address. *) | codeICode{icode=TailRecursiveCall{ regArgs, stackArgs, callKind, ...} :: rest, state=NormalState state, code, context} = let val (pushedState, pushCode) = pushRax state val currentSp = stackPtr pushedState (* Load the earlier arguments into registers. Do that first because they're lower down the stack and we could overwrite them if we wait. *) (* Load until we've done all the arguments or all the registers whichever is earlier. This includes the closure register. *) fun asGenReg(GenReg r) = r | asGenReg _ = raise InternalError "asGenReg" val doLoad = List.foldl (fn ((pr, gr), l) => l @ loadSource(pr, asGenReg gr, pushedState)) [] regArgs (* Load the return address. This could be overwritten by an argument. *) val loadReturn = loadStack(edi, currentSp * wordSize) (* Move the stack arguments into the space occupied by this function's args. *) val numArgsToMove = List.length stackArgs (* There's a bit of a nasty here. If we have several constant arguments that we haven't pushed to the stack we could find that argOffset is negative. To avoid that we push some zeros to line everything up. *) val (argOffset, extraPushes, currentState) = if currentSp + currentStackArgs >= numArgsToMove then (currentSp + currentStackArgs - numArgsToMove, [], pushedState) else let val needExtras = numArgsToMove - (currentSp + currentStackArgs) val extras = List.tabulate(needExtras, fn _ => PushValue { arg=IntegerConstant 0 }) and afterPush = {valueStack= {loc=OnStack(currentSp+needExtras-1), preg= ~1} :: # valueStack pushedState, ccState=CCIndeterminate, untaggedRegs=[]} in (0, extras, afterPush) end fun copyArgs (_, nil) = [] | copyArgs (n, {src=r, ...} :: rl) = let (* N.B. This is reversed *) fun storeToDest src = StoreArgument{source=src, base=(GenReg esp), offset=(argOffset+n)*wordSize, index=NoMemIndex, kind=MoveWord} (* If this is a 32-bit constant we can do a direct memory move. Othewise load it into a register. It might be easier to do some of this in the codetree translation. Treating all constants this way saves loading them into "registers" in order to save the values. *) val copy = case r of IntegerConstant value => if is32bit value then [storeToDest(IntegerConstant value)] else [storeToDest(RegisterArgument rsiAsArg), LoadArgument{source=IntegerConstant value, dest=rsiAsArg, kind=MoveWord}] | AddressConstant a => if isX64 then [storeToDest(RegisterArgument rsiAsArg), LoadArgument{source=AddressConstant a, dest=rsiAsArg, kind=MoveWord}] else [storeToDest(AddressConstant a)] | r => storeToDest(RegisterArgument rsiAsArg) :: loadSource(r, esi, currentState) in copyArgs(n-1, rl) @ copy end val moveArgs = copyArgs(numArgsToMove, stackArgs) val storeReturn = storeMemory(edi, esp, argOffset*wordSize) val functionCode = TailRecursiveCall{regArgs=[], stackArgs=[], callKind=callKind, returnAddr={srcStack=0, stack=0}, stackAdjust=0} :: resetStackPtr argOffset :: (storeReturn @ moveArgs @ extraPushes @ loadReturn @ doLoad @ pushCode @ code) in codeICode{icode=rest, state=Exited, code=functionCode, context=context} end (* Start of a loop. The loop body contains one or more tail jumps to the start. *) | codeICode{icode=StartLoop{arguments, loopLabel} :: rest, state=NormalState state, code, context={forwardLabels, handlers, loopArgs}} = let (* The arguments have been evaluated to the stack. Replace the preg entries in the state with those of the loop variables. *) val (pushedState, pushCode) = pushRax state val numArgs = List.length arguments val headList = List.take(#valueStack pushedState, numArgs) fun repSourceWithDest({source, loopReg}, {preg, loc}) = if argAsPReg source = preg then {preg=pRegNum loopReg, loc=loc} else raise InternalError "codeICode: StartLoop" val newHead = ListPair.mapEq repSourceWithDest (List.rev arguments, headList) val tailList = List.drop(#valueStack pushedState, numArgs) (* The CCstate is indeterminate because we may have looped. *) val bodyState = {valueStack=newHead @ tailList, ccState= CCIndeterminate, untaggedRegs= []} val newContext = {loopArgs=(bodyState, loopLabel) :: loopArgs, forwardLabels=forwardLabels, handlers=handlers} in codeICode{icode=rest, state=NormalState bodyState, code=StartLoop{arguments=[], loopLabel=loopLabel} :: pushCode @ code, context=newContext} end (* A loop tail jump. The arguments have been evaluated to the stack. *) | codeICode{icode=(JumpLoop{arguments, loopLabel}) :: rest, state=NormalState state, code, context=context as {loopArgs=(startState, lab) :: _, ...}} = let val _ = loopLabel = lab orelse raise InternalError "codeICode: JumpLoop - mismatched labels" val (pushedState, pushCode) = pushRax state (* Move each argument from the source to the loop variable. This isn't the same as MoveArgument because the destination already exists. *) fun moveArg{source, loopReg} = let val load = loadSource(source, eax, pushedState) val store = case findEntry (pRegNum loopReg, pushedState) of OnStack s => storeMemory(eax, esp, (stackPtr pushedState - s - 1) * wordSize) | InRax => raise InternalError "codeICode: JumpLoop" in store @ load end val storeAll = List.foldl(fn (arg, l) => l @ moveArg arg) [] arguments val instrs = JumpLoop{arguments=[], loopLabel=loopLabel} :: resetStackPtr(stackPtr pushedState - stackPtr startState) :: storeAll in codeICode{icode=rest, state=Exited, code=instrs @ pushCode @ code, context=context} end | codeICode{icode=JumpLoop _ :: _, ...} = raise InternalError "codeICode: JumpLoop out of loop" (* Raise an exception using the value in the "packet" register as the exception packet. Since this exits we can ignore any further code and return the code and state. *) | codeICode{icode=RaiseExceptionPacket{packet} :: rest, state=NormalState state, code, context} = let val (pushedState, pushCode) = pushRax state val load = loadSource(RegisterArgument packet, eax, pushedState) in codeICode{icode=rest, state=Exited, code=RaiseExceptionPacket {packet=raxAsArg } :: load @ pushCode @ code, context=context} end (* Reserve a contiguous area of memory on the stack. This is used to receive the results of a tuple. It may be set within the same function or the address may be passed into another function to allow it to return multiple results. *) | codeICode{icode=ReserveContainer{size, address} :: rest, state=NormalState state, code, context} = let val addrReg = pRegNum address val (pushedState, pushCode) = pushRax state (* The memory must be cleared in case we have a GC. *) val pushAll = List.tabulate(size, fn _ => PushValue{arg=IntegerConstant(tag 0)}) val sp = stackPtr pushedState in codeICode{icode=rest, state=NormalState( {valueStack={loc=InRax, preg=addrReg} :: {loc=OnStack(sp+size-1), preg= ~1} :: #valueStack pushedState, ccState=CCIndeterminate, untaggedRegs= []}), code=LoadArgument{source=RegisterArgument(GenReg esp), dest=raxAsArg, kind=MoveWord} :: (pushAll @ pushCode) @ code, context=context} end | codeICode{icode=IndexedCaseOperation{ testReg, workReg=_, cases, startValue} :: rest, state=NormalState state, code, context={loopArgs, handlers, forwardLabels}} = let val tReg = pRegNum testReg (* We should have the value to test at the top of the stack. *) val startState = checkTopInRax(state, tReg) (* This behaves rather like an unconditional branch except that it can go to several places. The case labels and the default label have to be added to the label list. *) val labelsFromCase = map(fn ilab => (ilab, startState)) cases @ forwardLabels in codeICode{icode=rest, state=Exited, code=IndexedCaseOperation{ testReg=raxAsArg, workReg=(GenReg ebx), cases=cases, startValue=startValue} :: code, context={loopArgs=loopArgs, handlers=handlers, forwardLabels=labelsFromCase}} end (* Lock a mutable segment. *) | codeICode{icode=LockMutable{ addr } :: rest, state=NormalState state, code, context} = let val (pushedState, pushCode) = pushRax state val load = loadSource(addr, eax, pushedState) val lockCode = LockMutable {addr=RegisterArgument raxAsArg} :: (load @ pushCode) val resultState = clearCC pushedState (* May affect the CC *) in codeICode{icode=rest, state=NormalState resultState, code=lockCode @ code, context=context} end | codeICode{icode=ReturnResultFromFunction{ resultReg, numStackArgs } :: rest, state=NormalState state, code, context} = let val resReg = pRegNum resultReg val (_, resetCode) = resetStack(state, initialState, resReg) val returnCode = ReturnResultFromFunction{resultReg=raxAsArg, numStackArgs=numStackArgs } :: resetCode in (* We may have more than one return point so we can't just stop here. *) codeICode{icode=rest, state=Exited, code=returnCode @ code, context=context} end | codeICode{icode=ArithmeticFunction{ oper, resultReg=PReg(resReg, PRegGeneral), operand1 as RegisterArgument(PReg(_, PRegGeneral)), operand2=IntegerConstant i, ccRef } :: rest, state=NormalState state, code, context} = let (* The result is a tagged register. This is used when the constant operand can be untagged. *) val (pushedState, pushCode) = pushRax state val loadCode = loadSource(operand1, eax, pushedState) val resultState = addRaxToState(pushedState, resReg) val checkState = {valueStack= #valueStack resultState, ccState=CCState(ccRef, fn i=>i), untaggedRegs= #untaggedRegs resultState} in codeICode{icode=rest, state=NormalState checkState, code=ArithmeticFunction { oper=oper, resultReg=raxAsArg, operand1=RegisterArgument raxAsArg, operand2=IntegerConstant i, ccRef=ccRef } :: loadCode @ pushCode @ code, context=context} end | codeICode{icode=ArithmeticFunction{ oper, resultReg=PReg(dReg, PRegUntagged), operand1 as RegisterArgument(PReg(_, PRegGeneral)), operand2=IntegerConstant i, ccRef } :: rest, state=NormalState state, code, context} = let (* The result is an untagged register. Typically used to untag a value before an operation when we don't want to shift the argument. *) val (pushedState, pushCode) = pushRax state (* Simplifies things *) (* Find a spare untagged register. *) val {valueStack, untaggedRegs, ...} = pushedState val spareReg = case untaggedRegs of [] => edx | [_] => ecx | _ => raise InternalError "codeICode: ArithmeticFunction" val resReg = (GenReg spareReg) val loadCode = loadSource(operand1, spareReg, pushedState) val resultState = {valueStack= valueStack, ccState= CCState(ccRef, fn i=>i), untaggedRegs ={ureg=dReg, reg=GenReg spareReg} :: untaggedRegs} in codeICode{icode=rest, state=NormalState resultState, code=ArithmeticFunction { oper=oper, resultReg=resReg, operand1=RegisterArgument resReg, operand2=IntegerConstant i, ccRef=ccRef } :: loadCode @ pushCode @ code, context=context} end | codeICode{icode=ArithmeticFunction{ oper, resultReg=PReg(resReg, PRegGeneral), operand1=RegisterArgument(PReg(oper1Reg, PRegUntagged)), operand2=IntegerConstant i, ccRef } :: rest, state=NormalState (state as {untaggedRegs, ...}), code, context} = let (* The result is a tagged register but the argument is untagged. This is typically when we want to set the tag on a value. *) val realSReg = case List.find (fn {ureg, ...} => ureg = oper1Reg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: ArithmeticFunction" val (pushedState, pushCode) = pushRax state val addState = addRaxToState(pushedState, resReg) val resultState = removeAfterTag(addState, oper1Reg) in codeICode{icode=rest, state=NormalState resultState, code= (* TODO: We could use LEA since this is normally (always?) ADD *) LoadArgument{source=RegisterArgument realSReg, dest=raxAsArg, kind=MoveWord} :: ArithmeticFunction { oper=oper, resultReg=realSReg, operand1=RegisterArgument realSReg, operand2=IntegerConstant i, ccRef=ccRef } :: pushCode @ code, context=context} end | codeICode{icode=ArithmeticFunction{ oper, resultReg=PReg(resReg, PRegUntagged), operand1=RegisterArgument(PReg(oper1Reg, PRegUntagged)), operand2=IntegerConstant i, ccRef } :: rest, state=NormalState ({valueStack, untaggedRegs, ...}), code, context} = let (* The result and argument are both untagged. This is used in computing floating point comparisons. *) val realSReg = case List.find (fn {ureg, ...} => ureg = oper1Reg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: ArithmeticFunction" (* Leave the untagged register where it was but add the condition code. *) val resultState = {valueStack=valueStack, ccState=CCState(ccRef, fn i => i), untaggedRegs=[{ureg=resReg, reg=realSReg}]} in codeICode{icode=rest, state=NormalState resultState, code= ArithmeticFunction { oper=oper, resultReg=realSReg, operand1=RegisterArgument realSReg, operand2=IntegerConstant i, ccRef=ccRef } :: code, context=context} end | codeICode{icode=ArithmeticFunction{ oper, resultReg, operand1=RegisterArgument(PReg(oper1Reg, PRegGeneral)), operand2 as RegisterArgument(PReg(_, PRegGeneral)), ccRef } :: rest, state=NormalState state, code, context} = let (* The top item should be in RAX but that is the second argument. That's all right for addition but wrong for subtraction. Move the first argument into RBX, load the second into RAX and then do the operation. *) val resReg = pRegNum resultReg val (topState, loadArg2Base) = loadToRax(state, operand2) val secondArg = case findEntry (oper1Reg, topState) of OnStack s => s | _ => raise InternalError "codeICode: ArithmeticFunction" val resultState = addRaxToState(topState, resReg) val checkState = {valueStack= #valueStack resultState, ccState=CCState(ccRef, fn i=>i), untaggedRegs= #untaggedRegs resultState} in codeICode{icode=rest, state=NormalState checkState, code= (* N.B. In reverse order *) ArithmeticFunction { oper=oper, resultReg=raxAsArg, operand1=RegisterArgument raxAsArg, operand2=RegisterArgument(GenReg ebx), ccRef=ccRef } :: LoadArgument { source=MemoryLocation{offset=(stackPtr topState - secondArg - 1) * wordSize, base=(GenReg esp), index=NoMemIndex}, dest=raxAsArg, kind=MoveWord } :: LoadArgument { source=RegisterArgument raxAsArg, dest=GenReg ebx, kind=MoveWord} :: loadArg2Base @ code, context=context} end | codeICode{ icode=ArithmeticFunction{ oper, resultReg=PReg(resReg, PRegUntagged), operand1=RegisterArgument(PReg(oper1Reg, PRegUntagged)), operand2=MemoryLocation{offset=offset2, base=bReg2, index=NoMemIndex}, ccRef } :: rest, state=NormalState state, code, context} = (* This is used for LargeWord operations. *) let val ({ valueStack, untaggedRegs, ...}, loadArg2Base) = loadToRax(state, RegisterArgument bReg2) (* The result and argument are both untagged. *) val realSReg = case List.find (fn {ureg, ...} => ureg = oper1Reg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: ArithmeticFunction" val resultState = {valueStack=valueStack, ccState=CCState(ccRef, fn i => i), untaggedRegs=[{ureg=resReg, reg=realSReg}]} in codeICode{icode=rest, state=NormalState resultState, code= ArithmeticFunction { oper=oper, resultReg=realSReg, operand1=RegisterArgument realSReg, operand2=MemoryLocation{offset=offset2, base=raxAsArg, index=NoMemIndex}, ccRef=ccRef } :: loadArg2Base @ code, context=context} end | codeICode{icode=ArithmeticFunction _ :: _, ...} = raise InternalError "TODO: CodeTransform ArithmeticFunction" | codeICode{icode=TagValue { source, dest } :: rest, state=NormalState (state as {untaggedRegs, ...}), code, context} = let val sReg = uRegNum source and destReg = pRegNum dest val realSReg = case List.find (fn {ureg, ...} => ureg = sReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: TagValue" val (pushedState, pushCode) = pushRax state val addState = addRaxToState(pushedState, destReg) val resultState = removeAfterTag(addState, sReg) in codeICode{icode=rest, state=NormalState resultState, code=LoadEffectiveAddress { base=NONE, offset=1, index=MemIndex2 realSReg, dest=raxAsArg } :: pushCode @ code, context=context} end | codeICode{icode=UntagValue { source, dest, isSigned } :: rest, state=NormalState state, code, context} = let val dReg = uRegNum dest val (pushedState, pushCode) = pushRax state (* Simplifies things *) val (resultState, regAsArg) = newUreg(dReg, pushedState) val resReg = case regAsArg of (GenReg r) => r | _ => raise Match val loadCode = loadSource(source, resReg, pushedState) val resultState = clearCC resultState in codeICode{icode=rest, state=NormalState resultState, code= ShiftOperation{shift=if isSigned then SAR else SHR, resultReg=regAsArg, operand=RegisterArgument regAsArg, shiftAmount=IntegerConstant 1, ccRef=CcRef 0 } :: loadCode @ pushCode @ code, context=context} end | codeICode{ icode=LoadEffectiveAddress { base=SOME baseSource, offset, index=MemIndex1(PReg(iReg, PRegUntagged)), dest=PReg(dReg, PRegUntagged) } :: rest, state=NormalState state, code, context} = let (* This is used to compute the address for a CompareByteVectors instruction. We have to reuse the untagged register for the result. Use eax for the base. *) val (pushedState as { untaggedRegs, valueStack, ccState}, pushCode) = pushRax state (* Simplifies things *) val realIReg = case List.find (fn {ureg, ...} => ureg = iReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: LoadEffectiveAddress" val loadCode = loadRegister(baseSource, eax, pushedState) val filteredUntagged = List.filter (fn {ureg, ...} => ureg <> iReg) untaggedRegs val resultState = {valueStack=valueStack, ccState=ccState, untaggedRegs={ureg=dReg, reg=realIReg}::filteredUntagged} in codeICode{icode=rest, state=NormalState resultState, code= LoadEffectiveAddress {base=SOME raxAsArg, offset=offset, index=MemIndex1(realIReg), dest=realIReg} :: loadCode @ pushCode@code, context=context} end | codeICode{ icode=LoadEffectiveAddress { base=SOME baseSource, offset, index=NoMemIndex, dest=PReg(dReg, PRegUntagged)} :: rest, state=NormalState state, code, context} = let (* Used to compute the base address for block operations. The result is always an untagged register because it points into a block of ML memory. *) val (pushedState, pushCode) = pushRax state (* Simplifies things *) val loadCode = loadRegister(baseSource, eax, pushedState) val (resultState, iReg) = newUreg(dReg, pushedState) in codeICode{icode=rest, state=NormalState resultState, code= LoadEffectiveAddress {base=SOME raxAsArg, offset=offset, index=NoMemIndex, dest=iReg} :: loadCode @ pushCode@code, context=context} end | codeICode{ icode=LoadEffectiveAddress { base=SOME baseSource, offset, index, dest=PReg(dReg, PRegUntagged)} :: rest, state=NormalState state, code, context} = let (* Used to compute the base address for block word moves. Unlike the MemIndex1 case the index register is not an untagged register. *) val (pushedState, pushCode) = pushRax state (* Simplifies things *) val (iReg, indexed) = case index of MemIndex2 src => (src, MemIndex2 raxAsArg) | MemIndex4 src => (src, MemIndex4 raxAsArg) | MemIndex8 src => (src, MemIndex8 raxAsArg) | _ => raise InternalError "codeICode: MemIndex" val loadCode = loadRegister(baseSource, ebx, pushedState) @ loadRegister(iReg, eax, pushedState) val (resultState, realDReg) = newUreg(dReg, pushedState) in codeICode{icode=rest, state=NormalState resultState, code= LoadEffectiveAddress {base=SOME rbxAsArg, offset=offset, index=indexed, dest=realDReg} :: loadCode @ pushCode @ code, context=context} end (* | codeICode{icode=LoadEffectiveAddress { base=NONE, offset, index=MemIndex2(PReg iReg), dest } :: rest, state=NormalState state, code, context} = (* Currently just used for tagging. *) let val resReg = argToPReg dest val topState = checkTopInRax(state, iReg) val resultState = addRaxToState(topState, resReg) in codeICode{icode=rest, state=NormalState resultState, code=LoadEffectiveAddress{ base=NONE, offset=offset, index=MemIndex2 raxAsArg, dest=raxAsArg } :: code, context=context} end*) | codeICode{icode=LoadEffectiveAddress _ :: _, ...} = raise InternalError "TODO: CodeTransform LoadEffectiveAddress" | codeICode{icode=ShiftOperation {shift, resultReg, operand=RegisterArgument(PReg(operReg, PRegGeneral)), shiftAmount=IntegerConstant i, ccRef } :: rest, state=NormalState state, code, context} = let val resReg = pRegNum resultReg val topState = checkTopInRax(state, operReg) val resultState = addRaxToState(topState, resReg) val checkState = {valueStack= #valueStack resultState, ccState=CCState(ccRef, fn i=>i), untaggedRegs= #untaggedRegs resultState} in codeICode{icode=rest, state=NormalState checkState, code=ShiftOperation { shift=shift, resultReg=raxAsArg, operand=RegisterArgument raxAsArg, shiftAmount=IntegerConstant i, ccRef=ccRef } :: code, context=context} end | codeICode{icode=ShiftOperation {shift, resultReg, operand=RegisterArgument(PReg(operReg, PRegUntagged)), shiftAmount=RegisterArgument(PReg(shiftReg, PRegUntagged)), ccRef } :: rest, state=NormalState ({untaggedRegs, valueStack, ...}), code, context} = let (* Shift by a variable. This should be in rcx which is where we want it. *) val resReg = uRegNum resultReg val realOperReg = case List.find (fn {ureg, ...} => ureg = operReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: ShiftOperation" val realShiftReg = case List.find (fn {ureg, ...} => ureg = shiftReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: ShiftOperation" val _ = realShiftReg = GenReg ecx orelse raise InternalError "ShiftOperation: not ecx" val resultState = {valueStack=valueStack, ccState=CCState(ccRef, fn i=>i), untaggedRegs =[{ureg=resReg, reg=realOperReg}]} in codeICode{icode=rest, state=NormalState resultState, code=ShiftOperation{ shift=shift, resultReg=realOperReg, operand=RegisterArgument realOperReg, shiftAmount=RegisterArgument realShiftReg, ccRef=ccRef} :: code, context=context} end | codeICode{ icode=ShiftOperation {shift, resultReg, operand as MemoryLocation{index=NoMemIndex, ...}, shiftAmount=RegisterArgument(PReg(shiftReg, PRegUntagged)), ccRef } :: rest, state=NormalState (state as {untaggedRegs, valueStack, ...}), code, context} = let (* Shift by a variable. This is used for LargeWord shifts. The argument is boxed rather than untagged so we will have loaded the shift amount, which is tagged, into edx. *) val resReg = uRegNum resultReg val realShiftReg = case List.find (fn {ureg, ...} => ureg = shiftReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: ShiftOperation" val _ = realShiftReg = GenReg edx orelse raise InternalError "ShiftOperation: it is ecx" (* Move the shift amount into ecx then load the value to be shifted into edx. *) val loadCode = loadSource(operand, edx, state) val resultState = {valueStack=valueStack, ccState=CCState(ccRef, fn i=>i), untaggedRegs =[{ureg=resReg, reg=GenReg edx}]} in codeICode{icode=rest, state=NormalState resultState, code=ShiftOperation{ shift=shift, resultReg=rdxAsArg, operand=RegisterArgument rdxAsArg, shiftAmount=RegisterArgument rcxAsArg, ccRef=ccRef} :: loadCode @ (LoadArgument{source=RegisterArgument rdxAsArg, dest=rcxAsArg, kind=MoveWord} :: code), context=context} end | codeICode{icode=ShiftOperation _ :: _, ...} = raise InternalError "TODO: CodeTransform ShiftOperation" | codeICode{icode=Multiplication { resultReg, operand1, operand2, ccRef } :: rest, state=NormalState ({untaggedRegs, valueStack, ...}), code, context} = let (* For the moment we only implement the case of multiplying two values in registers. The X86 supports various other multiplication forms if one of the arguments is a constant including one which takes three arguments. *) val resReg = uRegNum resultReg and op1Reg = argAsUReg operand1 and op2Reg = argAsUReg operand2 val realOp1Reg = case List.find (fn {ureg, ...} => ureg = op1Reg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: Multiplication" val realOp2Reg = case List.find (fn {ureg, ...} => ureg = op2Reg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: Multiplication" (* We can replace both the untagged registers. *) val resultState = {valueStack=valueStack, ccState=CCState(ccRef, fn i=>i), untaggedRegs =[{ureg=resReg, reg=realOp1Reg}]} in codeICode{icode=rest, state=NormalState resultState, code=Multiplication{ resultReg=realOp1Reg, operand1=RegisterArgument realOp1Reg, operand2=RegisterArgument realOp2Reg, ccRef=ccRef} :: code, context=context} end (* | codeICode{ icode=Division { isSigned, dividend as MemoryLocation{index=NoMemIndex, ...}, divisor as MemoryLocation{index=NoMemIndex, ...}, quotient, remainder } :: rest, state=NormalState state, code, context} = let (* We need the dividend in Rax so we can't use it as the base reg for the divisor. *) val (pushState, pushCode) = pushRax state (* We need RAX. *) val loadDivisor = loadSource(divisor, ecx, pushState) val loadDividend = loadSource(dividend, eax, pushState) val resultState = {valueStack= #valueStack pushState, ccState=CCIndeterminate, untaggedRegs =[{ureg=uRegNum quotient, reg=GenReg eax}, {ureg=uRegNum remainder, reg=GenReg edx}]} in codeICode{icode=rest, state=NormalState resultState, code= Division{ isSigned=isSigned, dividend=RegisterArgument raxAsArg, divisor=RegisterArgument rcxAsArg, quotient=raxAsArg, remainder=rdxAsArg} :: loadDividend @ loadDivisor @ pushCode @ code, context=context} end*) | codeICode{icode=Division { isSigned, dividend, divisor, quotient, remainder } :: rest, state=NormalState state, code, context} = let val dividendReg = uRegNum dividend and divisorReg = argAsUReg divisor val ({ untaggedRegs, valueStack, ...}, pushCode) = pushRax state (* We need RAX. *) val realDividend = case List.find (fn {ureg, ...} => ureg = dividendReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: Division" val realDivisor = case List.find (fn {ureg, ...} => ureg = divisorReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: Division" val resultState = {valueStack=valueStack, ccState=CCIndeterminate, untaggedRegs =[{ureg=uRegNum quotient, reg=GenReg eax}, {ureg=uRegNum remainder, reg=GenReg edx}]} (* The untagging code puts the first value into edx and the second into ecx. We have to move the dividend into eax. *) val _ = realDividend = GenReg edx orelse raise InternalError "codeICode: dividend" val _ = realDivisor = GenReg ecx orelse raise InternalError "codeICode: divisor" in codeICode{icode=rest, state=NormalState resultState, code= Division{ isSigned=isSigned, dividend=raxAsArg, divisor=RegisterArgument rcxAsArg, quotient=raxAsArg, remainder=rdxAsArg} :: LoadArgument { source=RegisterArgument realDividend, dest=raxAsArg, kind=MoveWord } :: pushCode @ code, context=context} end | codeICode{icode=AtomicExchangeAndAdd{ base, source } :: rest, state=NormalState state, code, context} = let val (pushedState, pushCode) = pushRax state (* Load the "destination" address into rax. *) val load = loadSource(RegisterArgument base, eax, pushedState) (* The "source" is an untagged register. *) val srcReg = getUreg(uRegNum source, pushedState) in codeICode{icode=rest, state=NormalState pushedState, code=AtomicExchangeAndAdd{base=raxAsArg, source=srcReg} :: load @ pushCode @ code, context=context} end | codeICode{icode=BoxValue{ boxKind=BoxLargeWord, dest, source, saveRegs=_ } :: rest, state=NormalState state, code, context} = let (* Allocate a one word cell and store the untagged value into it. *) val destReg = pRegNum dest val srcReg = getUreg(uRegNum source, state) val realSource = case srcReg of (GenReg r) => r | _ => raise InternalError "BoxLargeWord" val (newSrcReg, pushedState, pushCode) = if realSource = eax then let (* If the value we want to store is in eax i.e. the quotient, we must move it to another register before the allocation. *) val pushCode = [LoadArgument{ source=RegisterArgument srcReg, dest=rcxAsArg, kind=MoveWord}] in (rcxAsArg, state, pushCode) end else let val (pushedState, pushCode) = pushRax state in (srcReg, pushedState, pushCode) end val resultState = removeAfterTag(clearCC(addRaxToState(pushedState, destReg)) (* Affects CC *), srcReg) in codeICode{ icode=rest, state=NormalState resultState, code= InitialisationComplete{dest=raxAsArg} :: StoreArgument{ source=RegisterArgument newSrcReg, offset=0, base=GenReg eax, index=NoMemIndex, kind=MoveWord} :: AllocateMemoryOperation{ size=1, flags=0wx1, dest=raxAsArg, saveRegs=[]} :: pushCode @ code, context=context} end | codeICode{icode=BoxValue{ boxKind=BoxFloat, dest, source, saveRegs=_ } :: rest, state=NormalState state, code, context} = let (* Allocate a one or two word cell and store the untagged value into it. *) val destReg = pRegNum dest val srcReg = getFPreg(uRegNum source, state) val (pushedState, pushCode) = pushRax state val resultState = removeAfterTag(clearCC(addRaxToState(pushedState, destReg)) (* Affects CC *), srcReg) val boxSize = Int.quot(8, wordSize) in codeICode{ icode=rest, state=NormalState resultState, code= InitialisationComplete{dest=raxAsArg} :: StoreArgument{ source=RegisterArgument srcReg, offset=0, base=GenReg eax, index=NoMemIndex, kind=MoveDouble} :: AllocateMemoryOperation{ size=boxSize, flags=0wx1, dest=raxAsArg, saveRegs=[]} :: pushCode @ code, context=context} end | codeICode{icode=CompareByteVectors { vec1Addr, vec2Addr, length, ccRef } :: rest, state=NormalState state, code, context} = let val {untaggedRegs, ...} = state val vec1Reg = uRegNum vec1Addr and vec2Reg = uRegNum vec2Addr val realVec1Reg = case List.find (fn {ureg, ...} => ureg = vec1Reg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: CompareByteVectors" val realVec2Reg = case List.find (fn {ureg, ...} => ureg = vec2Reg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: CompareByteVectors" (* Put the length into RCX. *) (* There's a complication here. CompareByteVectors generates REPE CMPSB to compare the vectors but the condition code is only set if CMPSB is executed at least once. If the value in RCX/ECX is zero it will never be executed and the condition code will be unchanged. We want the result to be "equal" in that case so we need to ensure that is the case. It's quite possible that the condition code has just been set by shifting RCX/ECX to remove the tag in which case it will have set "equal" if the value was zero. We use CMP R/ECX,R/ECX which is two bytes in 32-bit but three in 64-bit. *) val (lengthCode, setZeroFlag) = let val lenReg = uRegNum length val realLenReg = case List.find (fn {ureg, ...} => ureg = lenReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: CompareByteVectors" val _ = realLenReg = GenReg esi orelse raise InternalError "codeICode: lenReg" in (LoadArgument{source=RegisterArgument realLenReg, dest=rcxAsArg, kind=MoveWord}, [WordComparison {arg1=RegisterArgument rcxAsArg, arg2=RegisterArgument rcxAsArg, ccRef=ccRef}]) (* Set CC - any reg will do. *) end (* These aren't in the registers we want so we have to shuffle them. *) val _ = realVec1Reg = GenReg edx orelse raise InternalError "codeICode: vec1Reg" val _ = realVec2Reg = GenReg ecx orelse raise InternalError "codeICode: vec2Reg" val resultState = {valueStack= #valueStack state, ccState=CCState(ccRef, fn i=>i), untaggedRegs= []} in codeICode{ icode=rest, state=NormalState resultState, code = CompareByteVectors{vec1Addr=rsiAsArg, vec2Addr=rdiAsArg, length=rcxAsArg, ccRef=ccRef} :: setZeroFlag @ ( LoadArgument{source=RegisterArgument realVec1Reg, dest=rsiAsArg, kind=MoveWord} :: lengthCode :: LoadArgument{source=RegisterArgument realVec2Reg, dest=rdiAsArg, kind=MoveWord} :: code), context=context} end | codeICode{icode=BlockMove { srcAddr, destAddr, length, isByteMove } :: rest, state=NormalState state, code, context} = let val {untaggedRegs, ...} = state val srcReg = uRegNum srcAddr and destReg = uRegNum destAddr and lenReg = uRegNum length val realSrcReg = case List.find (fn {ureg, ...} => ureg = srcReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: BlockMove" val realDestReg = case List.find (fn {ureg, ...} => ureg = destReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: BlockMove" val realLenReg = case List.find (fn {ureg, ...} => ureg = lenReg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: BlockMove" (* These aren't in the registers we want so we have to shuffle them. *) val _ = realSrcReg = GenReg edx orelse raise InternalError "codeICode: vec1Reg" val _ = realDestReg = GenReg ecx orelse raise InternalError "codeICode: vec2Reg" val _ = realLenReg = GenReg esi orelse raise InternalError "codeICode: lenReg" val resultState = {valueStack= #valueStack state, ccState=CCIndeterminate, untaggedRegs= []} in codeICode{ icode=rest, state=NormalState resultState, code = BlockMove{srcAddr=rsiAsArg, destAddr=rdiAsArg, length=rcxAsArg, isByteMove=isByteMove} :: LoadArgument{source=RegisterArgument realSrcReg, dest=rsiAsArg, kind=MoveWord} :: LoadArgument{source=RegisterArgument realLenReg, dest=rcxAsArg, kind=MoveWord} :: LoadArgument{source=RegisterArgument realDestReg, dest=rdiAsArg, kind=MoveWord} :: code, context=context} end | codeICode{ icode=CompareFloatingPt{ arg1=MemoryLocation{offset=offset1, base=bReg1, index=NoMemIndex}, arg2=MemoryLocation{offset=offset2, base=bReg2, index=NoMemIndex}, ccRef} :: rest, state=NormalState state, code, context=context} = let (* Load the first argument into an SSE2 register or the X87 stack. Compare with the second. *) val (startState as { valueStack, ...}, arg2Code) = loadToRax(state, RegisterArgument bReg2) val arg1Code = loadRegister(bReg1, ebx, startState) val floatingPointReg = case fpMode of FPModeX87 => FPReg fp0 | FPModeSSE2 => XMMReg xmm0 val checkState = {valueStack= valueStack, ccState=CCState(ccRef, fn c => c), untaggedRegs= []} in codeICode{icode=rest, state=NormalState checkState, code= CompareFloatingPt{arg1=RegisterArgument floatingPointReg, arg2=MemoryLocation{offset=offset2, base=raxAsArg, index=NoMemIndex}, ccRef=ccRef} :: LoadArgument{source=MemoryLocation{offset=offset1, base=rbxAsArg, index=NoMemIndex}, dest=floatingPointReg, kind=MoveDouble} :: arg1Code @ arg2Code @ code, context=context} end | codeICode{icode=CompareFloatingPt _ :: _, ...} = raise InternalError "codeICode: CompareFloatingPt" | codeICode{ icode=X87FPGetCondition{ ccRef, dest } :: rest, state=NormalState state, code, context=context} = let val destReg = uRegNum dest (* Check we have the condition. *) (* We can only use RAX here. *) val ({valueStack, ccState, ...}, pushCode) = pushRax state val () = case ccState of CCState(currentRef, _) => if currentRef = ccRef then () else raise InternalError "codeICode: condition ref incorrect" | _ => raise InternalError "codeICode: condition ref unset" val resultState = {valueStack=valueStack, ccState=ccState, untaggedRegs=[{ureg=destReg, reg=GenReg eax}]} in codeICode{icode=rest, state=NormalState resultState, code= X87FPGetCondition{ ccRef=ccRef, dest=raxAsArg } :: pushCode @ code, context=context} end | codeICode{ icode=X87FPArith{ opc, resultReg, arg1=MemoryLocation{offset=offset1, base=bReg1, index=NoMemIndex}, arg2=MemoryLocation{offset=offset2, base=bReg2, index=NoMemIndex}} :: rest, state=NormalState state, code, context=context} = let (* The address of the first argument will be on the stack. The second will be in Rax. *) val startState as {valueStack, ...} = checkTopInRax(state, pRegNum bReg2) val loadArgAddr = loadRegister(bReg1, ebx, startState) val floatingPointReg = FPReg fp0 val destReg = uRegNum resultReg val resultState = {valueStack=valueStack, ccState=CCIndeterminate, untaggedRegs=[{ureg=destReg, reg=floatingPointReg}]} in codeICode{icode=rest, state=NormalState resultState, code= X87FPArith{ opc=opc, resultReg=floatingPointReg, arg1=RegisterArgument floatingPointReg, arg2=MemoryLocation{offset=offset2, base=raxAsArg, index=NoMemIndex}} :: LoadArgument{source=MemoryLocation{offset=offset1, base=rbxAsArg, index=NoMemIndex}, dest=floatingPointReg, kind=MoveDouble} :: loadArgAddr @ code, context=context} end | codeICode{icode=X87FPArith _ :: _, ...} = raise InternalError "codeICode: X87FPArith" | codeICode{ icode=SSE2FPArith{ opc, resultReg, arg1=MemoryLocation{offset=offset1, base=bReg1, index=NoMemIndex}, arg2=MemoryLocation{offset=offset2, base=bReg2, index=NoMemIndex}} :: rest, state=NormalState state, code, context=context} = let (* The address of the first argument will be on the stack. The second will be in Rax. *) val startState as {valueStack, ...} = checkTopInRax(state, pRegNum bReg2) val loadArgAddr = loadRegister(bReg1, ebx, startState) val floatingPointReg = XMMReg xmm0 val destReg = uRegNum resultReg val resultState = {valueStack=valueStack, ccState=CCIndeterminate, untaggedRegs=[{ureg=destReg, reg=floatingPointReg}]} (* We can't use this for the logical operations since they require 128-bit args. *) val () = case opc of SSE2Xor => raise InternalError "codeICode: SSE2FPArith - SSE2Xor" | SSE2And => raise InternalError "codeICode: SSE2FPArith - SSE2And" | _ => () in codeICode{icode=rest, state=NormalState resultState, code= SSE2FPArith{ opc=opc, resultReg=floatingPointReg, arg1=RegisterArgument floatingPointReg, arg2=MemoryLocation{offset=offset2, base=raxAsArg, index=NoMemIndex}} :: LoadArgument{source=MemoryLocation{offset=offset1, base=rbxAsArg, index=NoMemIndex}, dest=floatingPointReg, kind=MoveDouble} :: loadArgAddr @ code, context=context} end | codeICode{ icode=SSE2FPArith{ opc, resultReg, arg1=MemoryLocation{offset=offset1, base=bReg1, index=NoMemIndex}, arg2=AddressConstant a} :: rest, state=NormalState state, code, context=context} = let (* This is used for the logical operations to invert or mask the sign bit. Both arguments need to be loaded into registers because any memory argument must be a 128-bit value. *) val {valueStack, ...} = checkTopInRax(state, pRegNum bReg1) val floatingPointReg0 = XMMReg xmm0 val floatingPointReg1 = XMMReg xmm1 val destReg = uRegNum resultReg val resultState = {valueStack=valueStack, ccState=CCIndeterminate, untaggedRegs=[{ureg=destReg, reg=floatingPointReg0}]} in codeICode{icode=rest, state=NormalState resultState, code= SSE2FPArith{ opc=opc, resultReg=floatingPointReg0, arg1=RegisterArgument floatingPointReg0, arg2=RegisterArgument floatingPointReg1} :: LoadArgument{source=AddressConstant a, dest=floatingPointReg1, kind=MoveDouble} :: LoadArgument{source=MemoryLocation{offset=offset1, base=raxAsArg, index=NoMemIndex}, dest=floatingPointReg0, kind=MoveDouble} :: code, context=context} end | codeICode{icode=SSE2FPArith _ :: _, ...} = raise InternalError "codeICode: SSE2FPArith" | codeICode{ icode=X87FPUnaryOps{ fpOp, dest, source=MemoryLocation{offset=offset, base=bReg, index=NoMemIndex}} :: rest, state=NormalState state, code, context=context} = let (* The address of the argument will be on the stack. *) val {valueStack, ...} = checkTopInRax(state, pRegNum bReg) val floatingPointReg = FPReg fp0 val destReg = uRegNum dest val resultState = {valueStack=valueStack, ccState=CCIndeterminate, untaggedRegs=[{ureg=destReg, reg=floatingPointReg}]} in codeICode{icode=rest, state=NormalState resultState, code= X87FPUnaryOps{fpOp=fpOp, dest=floatingPointReg, source=RegisterArgument floatingPointReg} :: LoadArgument{source=MemoryLocation{offset=offset, base=raxAsArg, index=NoMemIndex}, dest=floatingPointReg, kind=MoveDouble} :: code, context=context} end | codeICode{icode=X87FPUnaryOps _ :: _, ...} = raise InternalError "codeICode: X87FPUnaryOps" | codeICode{icode=FloatFixedInt{ dest, source} :: rest, state=NormalState ({untaggedRegs, valueStack, ...}), code, context=context} = let (* The fixed point value should be in an untagged register. *) val op1Reg = argAsUReg source val realOpReg = case List.find (fn {ureg, ...} => ureg = op1Reg) untaggedRegs of SOME {reg as GenReg _, ...} => reg | _ => raise InternalError "codeICode: Multiplication" val (floatingPointReg, floatCode) = case fpMode of FPModeX87 => let (* This is complicated. The integer value has to be in memory not in a register so we have to push it to the stack and then make sure it is popped afterwards. Because it is untagged it is unsafe to leave it. *) val fpReg = FPReg fp0 val fpCode = [ ResetStackPtr {numWords=1}, FloatFixedInt{dest=fpReg, source=wordOffsetAddress(0, esp)}, PushValue{arg=RegisterArgument realOpReg} ] in (fpReg, fpCode) end | FPModeSSE2 => let val fpReg = XMMReg xmm0 in (fpReg, [FloatFixedInt{dest=fpReg, source=RegisterArgument realOpReg}]) end val destReg = uRegNum dest val resultState = {valueStack=valueStack, ccState=CCIndeterminate, untaggedRegs=[{ureg=destReg, reg=floatingPointReg}]} in codeICode{icode=rest, state=NormalState resultState, code=floatCode @ code,context=context} end | codeICode{icode=ResetStackPtr _ :: rest, state, code, context} = (* This can be skipped. *) codeICode{icode=rest, state=state, code=code, context=context} (* These should not occur here. They are only added during this phase. *) | codeICode{icode=PushValue _ :: _, ...} = raise InternalError "codeICode: PushValue" | codeICode{icode=ExchangeRegisters _ :: _, ...} = raise InternalError "codeICode: ExchangeRegisters" datatype tooHardReason = NotEnoughRegs | MustPushReg | NotDoneInstr | OtherReason exception TooHard of tooHardReason val (identifiedCode, regStates) = identifyRegisters {icode=icode, maxPRegs=maxPRegs} val reportSuccess = ref false (* Process arithmetic operations in the code. Arithmetic operations require at least one operand in a register and deliver the result in the same register. We need to check whether we can reuse an argument and copy it into a new register if necessary. *) (* local val pregCounter = ref 0 val pregMap = Array.array(maxPRegs, NONE: int option) fun mapSrcReg(PReg(n, kind)) = PReg(valOf(Array.sub(pregMap, n)), kind) fun mapIndex NoMemIndex = NoMemIndex | mapIndex(MemIndex1 r) = MemIndex1(mapSrcReg r) | mapIndex(MemIndex2 r) = MemIndex2(mapSrcReg r) | mapIndex(MemIndex4 r) = MemIndex4(mapSrcReg r) | mapIndex(MemIndex8 r) = MemIndex8(mapSrcReg r) fun mapSource(RegisterArgument reg) = RegisterArgument(mapSrcReg reg) | mapSource(MemoryLocation{base, offset, index}) = MemoryLocation{base=mapSrcReg base, offset=offset, index=mapIndex index} | mapSource(c as AddressConstant _) = c | mapSource(c as IntegerConstant _) = c (* Map the destination. If we're returning the result from a conditional we can have several points that use the same destination register. *) fun mapDest(PReg(n, kind)) = case Array.sub(pregMap, n) of SOME newReg => PReg(newReg, kind) | NONE => let val newReg = !pregCounter before pregCounter := !pregCounter+1 in Array.update(pregMap, n, SOME newReg); PReg(newReg, kind) end fun codeArithmetic((LoadArgument{source, dest=dest, kind}, _)) = LoadArgument{source=mapSource source, dest=mapDest dest, kind=kind} | codeArithmetic((StoreArgument{source, offset, base, index, kind}, _)) = StoreArgument{source=mapSource source, base=mapSrcReg base, offset=offset, index=mapIndex index, kind=kind} | codeArithmetic((LoadStack { offset, dest}, _)) = LoadStack { offset=offset, dest=mapDest dest} | codeArithmetic((LoadMemReg { offset, dest}, _)) = LoadMemReg { offset=offset, dest=mapDest dest} | codeArithmetic((BeginFunction {regArgs}, _)) = BeginFunction {regArgs=map(fn (p, r) => (mapDest p, r)) regArgs} | codeArithmetic((FunctionCall{callKind, regArgs, stackArgs, dest, isTail}, _)) = FunctionCall{ callKind=callKind, regArgs=map(fn (p, r) => (mapSource p, r)) regArgs, stackArgs=map mapSource stackArgs, dest=mapDest dest, isTail=isTail} | codeArithmetic((AllocateMemoryOperation{size, flags, dest}, _)) = AllocateMemoryOperation{size=size, flags=flags, dest=mapDest dest} | codeArithmetic((AllocateMemoryVariable{size, flags, dest, initialiser}, _)) = AllocateMemoryVariable{size=mapSource size, flags=mapSource flags, dest=mapDest dest, initialiser=Option.map mapSrcReg initialiser} | codeArithmetic((InitialisationComplete{dest}, _)) = InitialisationComplete{dest=mapSrcReg dest} | codeArithmetic((StartLoop{arguments, loopLabel}, _)) = StartLoop{ arguments=map (fn {loopReg, source} => {loopReg=mapDest loopReg, source=mapSource source}) arguments, loopLabel=loopLabel} | codeArithmetic((EndLoop{loopLabel}, _)) = EndLoop{loopLabel=loopLabel} | codeArithmetic((JumpLoop{arguments, loopLabel}, _)) = JumpLoop{ arguments=map (fn {loopReg, source} => {loopReg=mapSrcReg loopReg, source=mapSource source}) arguments, loopLabel=loopLabel} | codeArithmetic((RaiseExceptionPacket{packet}, _)) = RaiseExceptionPacket{packet=mapSource packet} | codeArithmetic((ReserveContainer{size, address}, _)) = ReserveContainer{size=size, address=mapDest address} | codeArithmetic((IndexedCaseOperation{testReg, workReg, cases, startValue}, _)) = IndexedCaseOperation{testReg=mapSrcReg testReg, workReg=mapDest workReg, cases=cases, startValue=startValue} | codeArithmetic((LockMutable{addr}, _)) = LockMutable{addr=mapSource addr} | codeArithmetic((ForwardJumpLabel{label, result}, _)) = ForwardJumpLabel{label=label, result=Option.map mapSrcReg result} | codeArithmetic((UnconditionalForwardJump{label}, _)) = UnconditionalForwardJump{label=label} | codeArithmetic((ConditionalForwardJump{condition, label, ccRef}, _)) = ConditionalForwardJump{condition=condition, label=label, ccRef=ccRef} | codeArithmetic((WordComparison{arg1, arg2, ccRef}, _)) = WordComparison{arg1=mapSource arg1, arg2=mapSource arg2, ccRef=ccRef} | codeArithmetic((PushExceptionHandler{handlerAddr, handleStart}, _)) = PushExceptionHandler{handlerAddr=mapDest handlerAddr, handleStart=handleStart} | codeArithmetic((PopExceptionHandler{handlerAddr, resultReg, workReg}, _)) = PopExceptionHandler{handlerAddr=mapSrcReg handlerAddr, resultReg=Option.map mapSrcReg resultReg, workReg=mapDest workReg} | codeArithmetic((BeginHandler{handleStart, packetReg, workReg}, _)) = BeginHandler{handleStart=handleStart, packetReg=mapDest packetReg, workReg=mapDest workReg} | codeArithmetic((ReturnResultFromFunction{resultReg, numStackArgs}, _)) = ReturnResultFromFunction{resultReg=mapSrcReg resultReg, numStackArgs=numStackArgs} | codeArithmetic((ArithmeticFunction{oper, resultReg, operand1, operand2, ccRef}, _)) = ArithmeticFunction{oper=oper, resultReg=mapDest resultReg, operand1=mapSource operand1, operand2=mapSource operand2, ccRef=ccRef} | codeArithmetic((TestTagBit{arg, ccRef}, _)) = TestTagBit{arg=mapSource arg, ccRef=ccRef} | codeArithmetic((PushValue{arg}, _)) = PushValue{arg=mapSource arg} | codeArithmetic((ResetStackPtr{numWords}, _)) = ResetStackPtr{numWords=numWords} | codeArithmetic((TagValue{source, dest}, _)) = TagValue{source=mapSrcReg source, dest=mapDest dest} | codeArithmetic((UntagValue{source, dest, isSigned}, _)) = UntagValue{source=mapSource source, dest=mapDest dest, isSigned=isSigned} | codeArithmetic((LoadEffectiveAddress{base, offset, index, dest}, _)) = LoadEffectiveAddress{base=Option.map mapSrcReg base, offset=offset, index=mapIndex index, dest=mapDest dest} | codeArithmetic((ShiftOperation{shift, resultReg, operand, shiftAmount, ccRef}, _)) = ShiftOperation{shift=shift, resultReg=mapDest resultReg, operand=mapSource operand, shiftAmount=mapSource shiftAmount, ccRef=ccRef} | codeArithmetic((Multiplication{resultReg, operand1, operand2, ccRef}, _)) = Multiplication{resultReg=mapDest resultReg, operand1=mapSource operand1, operand2=mapSource operand2, ccRef=ccRef} | codeArithmetic((Division{isSigned, dividend, divisor, quotient, remainder}, _)) = Division{isSigned=isSigned, dividend=mapSource dividend, divisor=mapSource divisor, quotient=mapDest quotient, remainder=mapDest remainder} | codeArithmetic((AtomicExchangeAndAdd{destAddr, source}, _)) = AtomicExchangeAndAdd{destAddr=mapSource destAddr, source=mapSrcReg source} | codeArithmetic((BoxValue{boxKind, source, dest}, _)) = BoxValue{boxKind=boxKind, source=mapSrcReg source, dest=mapDest dest} | codeArithmetic((CompareByteVectors{vec1Addr, vec2Addr, length, ccRef}, _)) = CompareByteVectors{vec1Addr=mapSrcReg vec1Addr, vec2Addr=mapSrcReg vec2Addr, length=mapSource length, ccRef=ccRef} | codeArithmetic((BlockMove{srcAddr, destAddr, length, isByteMove}, _)) = BlockMove{srcAddr=mapSrcReg srcAddr, destAddr=mapSrcReg destAddr, length=mapSource length, isByteMove=isByteMove} | codeArithmetic((CompareFloatingPt{arg1, arg2, ccRef}, _)) = CompareFloatingPt{arg1=mapSource arg1, arg2=mapSource arg2, ccRef=ccRef} | codeArithmetic((X87FPGetCondition{dest, ccRef}, _)) = X87FPGetCondition{dest=mapDest dest, ccRef=ccRef} | codeArithmetic((X87FPArith{opc, resultReg, arg1, arg2}, _)) = X87FPArith{opc=opc, resultReg=mapDest resultReg, arg1=mapSource arg1, arg2=mapSource arg2} | codeArithmetic((X87FPUnaryOps{fpOp, dest, source}, _)) = X87FPUnaryOps{fpOp=fpOp, dest=mapDest dest, source=mapSource source} | codeArithmetic((FloatFixedInt{dest, source}, _)) = FloatFixedInt{dest=mapDest dest, source=mapSource source} | codeArithmetic((SSE2FPArith{opc, resultReg, arg1, arg2}, _)) = SSE2FPArith{opc=opc, resultReg=mapDest resultReg, arg1=mapSource arg1, arg2=mapSource arg2} in val postArithCode = map codeArithmetic decoratedCode val postArithPRegCount = !pregCounter end *) (* Allocated registers. This is set to the real register that is used for a specific pseudo-register. Once a register is allocated that is fixed. *) val allocatedRegs = Array.array(maxPRegs, NONE: reg option) (* Hint values. The idea of hints is that by using a hinted register we may avoid an unnecessary move instruction. realHints is set when a pseudo-register is going to be loaded from a specific register e.g. a register argument, or moved into one e.g. ecx for a shift. friends is set to the other pseudo-registers that may be associated with the pseudo-register. E.g. the argument and destination of an arithmetic operation where choosing the same register for each may avoid a move. *) val realHints = Array.array(maxPRegs, NONE: reg option) val friends = Array.array(maxPRegs, []: int list) fun addRealHint(r, reg) = case Array.sub(realHints, r) of NONE => Array.update(realHints, r, SOME reg) | SOME _ => () fun addFriends(f1, f2) = let val {conflicts, ...} = Vector.sub(regStates, f1) fun addF (f, toF) = let val currentFriends = Array.sub(friends, toF) in if List.exists(fn i => i=f) currentFriends then () else Array.update(friends, toF, f :: currentFriends) end in (* Add a friend if there's no conflict. *) if List.exists(fn i => i=f2) conflicts then () else (addF(f1, f2); addF(f2, f1)) end (* Find a real register for a preg. 1. If a register is already allocated use that. 2. Try the "preferred" register if one has been given. 3. Try the realHints value if there is one. 4. See if there is a "friend" that has an appropriate register 5. Look at all the registers and find one. *) fun findRegister(r, pref, regSet) = case Array.sub(allocatedRegs, r) of SOME reg => reg | NONE => let val {conflicts, realConflicts, pushState, ...} = Vector.sub(regStates, r) (* If we must push this we've got a problem. *) val _ = pushState <> MustPush orelse raise TooHard MustPushReg (* Find the registers we've already allocated that may conflict. *) val conflictingRegs = List.mapPartial(fn i => Array.sub(allocatedRegs, i)) conflicts @ realConflicts fun isFree aReg = not (List.exists(fn i => i=aReg) conflictingRegs) fun tryAReg NONE = NONE | tryAReg (somePref as SOME prefReg) = if isFree prefReg then (Array.update(allocatedRegs, r, somePref); somePref) else NONE fun findAReg [] = raise TooHard NotEnoughRegs | findAReg (reg::regs) = if isFree reg then (Array.update(allocatedRegs, r, SOME reg); reg) else findAReg regs (* See if there is a friend that has a register already or a hint. Friends are registers that don't conflict and can possibly avoid an extra move. *) fun findAFriend([], _) = NONE | findAFriend(friend :: tail, old) = let val possReg = case Array.sub(allocatedRegs, friend) of v as SOME _ => tryAReg v | NONE => tryAReg(Array.sub(realHints, friend)) in case possReg of reg as SOME _ => reg | NONE => let (* Add a friend of a friend to the list if we haven't already seen it and it doesn't conflict. *) fun newFriend f = not(List.exists (fn n => n=f) old) andalso not(List.exists (fn n => n=f) conflicts) val fOfF = List.filter newFriend (Array.sub(friends, friend)) in findAFriend(tail @ fOfF, friend :: old) end end in case tryAReg pref of SOME r => r | NONE => ( case tryAReg (Array.sub(realHints, r)) of SOME r => r | NONE => ( case findAFriend(Array.sub(friends, r), []) of SOME r => r (* Look through the registers to find one that's free. *) | NONE => findAReg regSet ) ) end fun findGeneralReg r = findRegister(r, NONE, generalRegisters) fun codeExtArgument(RegisterArgument(PReg(r, _))) = RegisterArgument(findGeneralReg r) | codeExtArgument(AddressConstant m) = AddressConstant m | codeExtArgument(IntegerConstant i) = IntegerConstant i | codeExtArgument(MemoryLocation{base=PReg(bReg, _), offset, index}) = MemoryLocation{base=findGeneralReg bReg, offset=offset, index=codeExtIndex index} - | codeExtArgument(StackLocation{offset, adjustment}) = - MemoryLocation{base=GenReg esp, offset=offset+adjustment, index=NoMemIndex} + | codeExtArgument(StackLocation{wordOffset, adjustment}) = + MemoryLocation{base=GenReg esp, offset=(wordOffset+adjustment)*wordSize, index=NoMemIndex} and codeExtIndex NoMemIndex = NoMemIndex | codeExtIndex(MemIndex1(PReg(r, _))) = MemIndex1(findGeneralReg r) | codeExtIndex(MemIndex2(PReg(r, _))) = MemIndex2(findGeneralReg r) | codeExtIndex(MemIndex4(PReg(r, _))) = MemIndex4(findGeneralReg r) | codeExtIndex(MemIndex8(PReg(r, _))) = MemIndex8(findGeneralReg r) fun moveRR{src, dst} = LoadArgument{source=RegisterArgument src, dest=dst, kind=MoveWord} fun moveIfNecessary{src, dst} = if src = dst then [] else [moveRR{src=src, dst=dst}] (* Where we have multiple specific registers as either source or destination there is the potential that a destination register if currently in use as a source. We have to do the moves in the right order and use exchanges if necessary. Since we're only dealing with a very few registers there's no need to avoid quadratic performance. *) fun moveMultipleRegisters regPairList = (* Filter out cases where they're (now) in the right registers. *) case List.filter(fn {src, dst} => src <> dst) regPairList of [] => [] | filtered => let (* Look for destinations that don't appear as sources. For those we can use simple moves. *) val (simpleMove, needXchng) = List.partition(fn {dst, ...} => List.all(fn {src, ...} => src <> dst) filtered) filtered val moveInstrs = List.map moveRR simpleMove (* What's left are items that appear as both sources and destinations. If we exchange the source and destination of an item we will set that destination as the correct value. Afterwards the old destination value is in the source register and vice versa. *) val (exchangeCode, remainder) = case needXchng of [] => ([], []) | {src=oldSrc, dst=oldDest} :: rest => let (* Swap the values. *) fun swapSrcs {src, dst} = {src=if src=oldSrc then oldDest else if src=oldDest then oldSrc else src, dst=dst} val swapped = List.map swapSrcs rest in ([ExchangeRegisters{regX=oldSrc, regY=oldDest}], swapped) end in moveInstrs @ exchangeCode @ moveMultipleRegisters remainder end + (* Tail recursive calls are complicated because we generally have to overwrite the existing stack. + That means storing the arguments in the right order to avoid overwriting a + value that we are using for a different argument. *) + fun codeTailCall(callKind, regArgs, stackArgs, stackAdjust) = + if stackAdjust < 0 + then + let + (* If the function we're calling takes more arguments on the stack than the + current function we will have to extend the stack. Do that by pushing the + argument whose offset is at -1. Then adjust all the offsets and repeat. *) + val {src=argM1, ...} = valOf(List.find(fn {stack= ~1, ...} => true | _ => false) stackArgs) + fun renumberArgs [] = [] + | renumberArgs ({stack= ~1, ...} :: args) = renumberArgs args (* Remove the one we've done. *) + | renumberArgs ({stack, src=StackLocation{wordOffset, adjustment}} :: args) = + {stack=stack+1, src=StackLocation{wordOffset=wordOffset+1, adjustment=adjustment}} :: renumberArgs args + | renumberArgs ({stack, src} :: args) = {stack=stack+1, src=src} :: renumberArgs args + in + PushValue{arg=argM1} :: codeTailCall(callKind, regArgs, renumberArgs stackArgs, stackAdjust+1) + end + else + let + (* Now deal with the stack arguments. The worst case is when all the arguments are + permuted. It's unlikely with hand-written code but quite possible with machine- + generated code. + At this point we have space on the stack for all the stack arguments. + We may also have arguments in registers and some of these will go into + the argument registers. + At the moment we don't save p-registers to the stack but eventually we + could also find that some of our register arguments have stack addresses. *) + local + (* Remove cases where we're storing to the same location. *) + fun filterCopy {src=StackLocation{wordOffset, adjustment}, stack} = + stack <> wordOffset+adjustment + | filterCopy _ = true + in + val filteredCopies = List.filter filterCopy stackArgs + end + + (* stronglyConnectedComponents does two things. It detects loops where + it's not possible to move items without breaking the loop but more + importantly it orders the dependencies so that if there are no loops we + can load the source and store it in the destination knowing that + we won't overwrite anything we might later need. *) + (*val getConnections = STRONGLY.stronglyConnectedComponents filteredCopies*) + + fun storeStack{src as RegisterArgument _, stack} = + StoreArgument{source=src, base=GenReg esp, index=NoMemIndex, offset = stack*wordSize, kind=MoveWord} + | storeStack _ = raise TooHard OtherReason + + val storeStackArgs = List.map storeStack filteredCopies + + (* The register argument list contains "argument" values. The entries are + either RegisterArgument or constants. Do the register arguments first. + We may be using some of the registers that need to contain constants. *) + fun getRegArgs((RegisterArgument src, reg)) = SOME{dst=reg, src=src} + | getRegArgs _ = NONE + val loadRegArgs = moveMultipleRegisters(List.mapPartial getRegArgs regArgs) + + fun getConstArgs(RegisterArgument _, _) = NONE (* Already done. *) + | getConstArgs(AddressConstant m, reg) = + SOME(LoadArgument{source=AddressConstant m, dest=reg, kind=MoveWord}) + | getConstArgs(IntegerConstant i, reg) = + SOME(LoadArgument{source=IntegerConstant i, dest=reg, kind=MoveWord}) + | getConstArgs(MemoryLocation _, _) = raise InternalError "FunctionCall - tail - MemoryLocation" + | getConstArgs(StackLocation _, _) = raise InternalError "FunctionCall - tail - StackLocation" + val loadConstArgs = List.mapPartial getConstArgs regArgs + val adjustStack = + if stackAdjust = 0 + then [] + else [ResetStackPtr{numWords=stackAdjust}] + in + storeStackArgs @ loadRegArgs @ loadConstArgs @ adjustStack @ + [TailRecursiveCall{regArgs=[], stackArgs=[], callKind=callKind, returnAddr={srcStack=0, stack=0}, stackAdjust=0}] + end + fun codeExtended([], _) = [] | codeExtended(LoadArgument{ kind=MoveFloat, ... } :: _, _) = raise TooHard NotDoneInstr | codeExtended(LoadArgument{ kind=MoveDouble, ... } :: _, _) = raise TooHard NotDoneInstr | codeExtended(LoadArgument{source=RegisterArgument(PReg(sreg, _)), dest=PReg(dreg, _), kind=MoveWord} :: rest, context) = (* Register to register move. Try to use the same register for the source as the destination to eliminate the instruction. *) let val () = addFriends (sreg, dreg) val code = codeExtended(rest, context) in case Array.sub(allocatedRegs, dreg) of NONE => (* The result was never used *) code | SOME realDestReg => let (* Get the source register using the current destination as a preference. *) val realSrcReg = findRegister(sreg, SOME realDestReg, generalRegisters) in (* If the source is the same as the destination we don't need to do anything. *) moveIfNecessary{src=realSrcReg, dst=realDestReg} @ code end end | codeExtended(LoadArgument{source, dest=PReg(pr, _), kind} :: rest, context) = (* Loads of constants or from an address. *) let val code = codeExtended(rest, context) in (* If we don't have a register that means the result is never used. *) case Array.sub(allocatedRegs, pr) of SOME regResult => LoadArgument{source=codeExtArgument source, dest=regResult, kind=kind} :: code | NONE => code end | codeExtended(StoreArgument{ kind=MoveFloat, ... } :: _, _) = raise TooHard NotDoneInstr | codeExtended(StoreArgument{ kind=MoveDouble, ... } :: _, _) = raise TooHard NotDoneInstr | codeExtended( StoreArgument{ source as RegisterArgument(PReg(sReg, _)), base=PReg(bReg, _), offset, index, kind=MoveByte, ... } :: rest, context) = if isX64 then let val code = codeExtended(rest, context) in StoreArgument{ source=codeExtArgument source, base=findGeneralReg bReg, offset=offset, index=codeExtIndex index, kind=MoveByte} :: code end else (* This is complicated on X86/32. We can't use edi or esi for the store registers. Instead we reserve ecx (see special case in "identify") and use that if we have to. *) let val () = addRealHint(sReg, GenReg ecx) val code = codeExtended(rest, context) val realStoreReg = findRegister(sReg, SOME(GenReg ecx), generalRegisters) val (moveCode, storeReg) = if realStoreReg = GenReg edi orelse realStoreReg = GenReg esi then (moveIfNecessary{src=realStoreReg, dst=GenReg ecx}, GenReg ecx) else ([], realStoreReg) in moveCode @ (StoreArgument{ source=RegisterArgument storeReg, base=findGeneralReg bReg, offset=offset, index=codeExtIndex index, kind=MoveByte} :: code) end | codeExtended(StoreArgument{ source, base=PReg(bReg, _), offset, index, kind as MoveWord } :: rest, context) = let val code = codeExtended(rest, context) in StoreArgument{ source=codeExtArgument source, base=findGeneralReg bReg, offset=offset, index=codeExtIndex index, kind=kind} :: code end | codeExtended(StoreArgument{ source, base=PReg(bReg, _), offset, index, kind } :: rest, context) = let val code = codeExtended(rest, context) in StoreArgument{ source=codeExtArgument source, base=findGeneralReg bReg, offset=offset, index=codeExtIndex index, kind=kind} :: code end | codeExtended(LoadMemReg { offset, dest=PReg(pr, _)} :: rest, context) = (* Load from the "memory registers" pointed at by ebp. *) let val code = codeExtended(rest, context) in (* If we don't have a register that means the result is never used. *) case Array.sub(allocatedRegs, pr) of SOME regResult => LoadArgument{source=MemoryLocation{base=GenReg ebp, offset=offset, index=NoMemIndex}, dest=regResult, kind=MoveWord} :: code | NONE => code end | codeExtended(ExchangeRegisters _ :: _, _) = (* This is only generated in this pass. *) raise InternalError "codeExtended - ExchangeRegisters" | codeExtended(BeginFunction{regArgs} :: rest, context) = let val () = List.app (fn (PReg(pr, _), reg) => addRealHint(pr, reg)) regArgs val code = codeExtended(rest, context) (* Look up the register we need to move the argument into. If there's no register then we don't use this argument and can drop it. *) fun mkPair(PReg(pr, _), rr) = case Array.sub(allocatedRegs, pr) of NONE => NONE | SOME regResult => SOME{src=rr,dst=regResult} val regPairs = List.mapPartial mkPair regArgs in moveMultipleRegisters regPairs @ code end - | codeExtended(TailRecursiveCall{callKind, regArgs, stackArgs=[], returnAddr as {srcStack, stack}, stackAdjust} :: rest, context) = + | codeExtended(TailRecursiveCall{callKind, regArgs, stackArgs, returnAddr={srcStack, stack}, stackAdjust} :: rest, context) = let - (* Currently just handle the case where neither the function being called - nor this function have stack args. That means that the return address - stays where it is. *) - val _ = currentStackArgs = 0 orelse raise TooHard NotDoneInstr - val _ = stackAdjust >= 0 orelse raise InternalError "codeExtended - stack adjust" - val _ = if stackAdjust > 0 then reportSuccess := true else () + val _ = case stackArgs of [] => () | _ => reportSuccess := true val () = List.app (fn (RegisterArgument(PReg(pr, _)), reg) => addRealHint(pr, reg) | _ => ()) regArgs val code = codeExtended(rest, context) - (* The register argument list contains "argument" values. The entries are - either RegisterArgument or constants. Do the register arguments first. - We may be using some of the registers that need to contain constants. *) - fun getRegArgs(RegisterArgument(PReg(pr, _)), reg) = - SOME{dst=reg, src=findRegister(pr, SOME reg, generalRegisters)} - | getRegArgs _ = NONE - val loadRegArgs = moveMultipleRegisters(List.mapPartial getRegArgs regArgs) - - fun getConstArgs(AddressConstant m, reg) = - SOME(LoadArgument{source=AddressConstant m, dest=reg, kind=MoveWord}) - | getConstArgs(IntegerConstant i, reg) = - SOME(LoadArgument{source=IntegerConstant i, dest=reg, kind=MoveWord}) - | getConstArgs(RegisterArgument _, _) = NONE - | getConstArgs(MemoryLocation _, _) = raise InternalError "FunctionCall - tail - MemoryLocation" - | getConstArgs(StackLocation _, _) = raise InternalError "FunctionCall - tail - StackLocation" - val loadConstArgs = List.mapPartial getConstArgs regArgs - val adjustStack = - if stackAdjust = 0 - then [] - else [ResetStackPtr{numWords=stackAdjust}] + (* Add the return address as an extra argument. This is a temporary hack because codeICode doesn't + do it that way. *) + val returnEntry = {src=StackLocation{wordOffset=srcStack, adjustment=0}, stack=stack} + val extStackArgs = map (fn {stack, src} => {stack=stack, src=codeExtArgument src}) stackArgs + val extRegArgs = map (fn (a, r) => (codeExtArgument a, r)) regArgs in - loadRegArgs @ loadConstArgs @ adjustStack @ - (TailRecursiveCall{regArgs=[], stackArgs=[], callKind=callKind, returnAddr={srcStack=0, stack=0}, stackAdjust=0} :: code) + codeTailCall(callKind, extRegArgs, returnEntry :: extStackArgs, stackAdjust) @ code end - | codeExtended(TailRecursiveCall _ :: _, _) = raise TooHard NotDoneInstr - - | codeExtended(FunctionCall{callKind, regArgs, stackArgs=[], dest=PReg(dReg, _)} :: rest, context) = + | codeExtended(FunctionCall{callKind, regArgs, stackArgs, dest=PReg(dReg, _)} :: rest, context) = let + val () = case stackArgs of [] => () | _ => reportSuccess := true val () = List.app (fn (RegisterArgument(PReg(pr, _)), reg) => addRealHint(pr, reg) | _ => ()) regArgs val () = addRealHint(dReg, GenReg eax) val code = codeExtended(rest, context) val destReg = findRegister(dReg, SOME(GenReg eax), generalRegisters) + fun pushStackArgs [] = [] + | pushStackArgs (arg ::args) = + let + (* We don't currently generate MemoryLocations or StackLocations. + If we have stack locations we'll need to adjust the stack + pointer to account for items we've already pushed. *) + val _ = + case arg of + MemoryLocation _ => raise InternalError "FunctionCall - MemoryLocation" + | StackLocation _ => raise InternalError "FunctionCall - StackLocation" + | _ => () + in + PushValue {arg=codeExtArgument arg} :: pushStackArgs args + end + val pushedArgs = pushStackArgs stackArgs + (* We don't currently allow the arguments to be memory locations and instead force them into registers. That may be simpler especially if we can get the - values directly into the required register. *) + values directly into the required register. + If we allow stack arguments we'll have to adjust the stack pointer here. *) fun getRegArgs(RegisterArgument(PReg(pr, _)), reg) = SOME{dst=reg, src=findRegister(pr, SOME reg, generalRegisters)} | getRegArgs _ = NONE val loadRegArgs = moveMultipleRegisters(List.mapPartial getRegArgs regArgs) fun getConstArgs(AddressConstant m, reg) = SOME(LoadArgument{source=AddressConstant m, dest=reg, kind=MoveWord}) | getConstArgs(IntegerConstant i, reg) = SOME(LoadArgument{source=IntegerConstant i, dest=reg, kind=MoveWord}) | getConstArgs(RegisterArgument _, _) = NONE | getConstArgs(MemoryLocation _, _) = raise InternalError "FunctionCall - MemoryLocation" | getConstArgs(StackLocation _, _) = raise InternalError "FunctionCall - StackLocation" val loadConstArgs = List.mapPartial getConstArgs regArgs in - loadRegArgs @ loadConstArgs @ + pushedArgs @ loadRegArgs @ loadConstArgs @ (FunctionCall{regArgs=[], stackArgs=[], dest=raxAsArg, callKind=callKind} :: moveIfNecessary{dst=destReg, src=GenReg eax}) @ code end - | codeExtended(FunctionCall _ :: _, _) = raise TooHard OtherReason - | codeExtended(AllocateMemoryOperation{ size, flags, dest=PReg(dReg, _), saveRegs} :: rest, context) = let val code = codeExtended(rest, context) val preserve = List.map(fn (PReg(r, _)) => findGeneralReg r) saveRegs in AllocateMemoryOperation{ size=size, flags=flags, dest=findGeneralReg dReg, saveRegs=preserve} :: code end | codeExtended(AllocateMemoryVariable{size=PReg(sReg, _), dest=PReg(dReg, _), saveRegs} :: rest, context) = let (* Simple case - no initialiser. *) val code = codeExtended(rest, context) val preserve = List.map(fn (PReg(r, _)) => findGeneralReg r) saveRegs val destReg = findGeneralReg dReg in AllocateMemoryVariable{size=findGeneralReg sReg, dest=destReg, saveRegs=preserve} :: code end | codeExtended(InitialiseMem{size=PReg(sReg, _), addr=PReg(aReg, _), init=PReg(iReg, _)} :: rest, context) = let (* We are going to use rep stosl/q to set the memory. That requires the length to be in ecx, the initialiser to be in eax and the destination to be edi. *) val () = addRealHint(aReg, GenReg edi) val () = addRealHint(iReg, GenReg eax) val () = addRealHint(sReg, GenReg ecx) val code = codeExtended(rest, context) val realAddrReg = findRegister(aReg, SOME(GenReg edi), generalRegisters) val realInitReg = findRegister(iReg, SOME(GenReg eax), generalRegisters) val realSizeReg = findRegister(sReg, SOME(GenReg ecx), generalRegisters) in moveMultipleRegisters[ {src=realInitReg, dst=GenReg eax}, {src=realSizeReg, dst=GenReg ecx}, {src=realAddrReg, dst=GenReg edi}] @ InitialiseMem{size=GenReg ecx, addr=GenReg edi, init=GenReg eax} :: code end | codeExtended(InitialisationComplete _ :: rest, context) = InitialisationComplete{dest=raxAsArg (* unused *)} :: codeExtended(rest, context) | codeExtended(StartLoop{arguments, loopLabel} :: rest, context) = let (* Make the loop arguments and the sources "friends". *) fun makeFriends {loopReg=PReg(dReg, _), source=RegisterArgument(PReg(sReg, _))} = addFriends(dReg, sReg) | makeFriends _ = () val () = List.app makeFriends arguments val code = codeExtended(rest, context) (* Evaluate the arguments. We currently just generate register arguments and that may be simpler anyway. *) fun moveArg {loopReg=PReg(dReg, _), source=RegisterArgument(PReg(sReg, _))} = let val destReg = findGeneralReg dReg val srcReg = findRegister(sReg, SOME destReg, generalRegisters) in {src=srcReg, dst=destReg} end | moveArg _ = raise InternalError "moveArg" val moveList = List.map moveArg arguments in moveMultipleRegisters moveList @ (StartLoop{arguments=[], loopLabel=loopLabel} :: code) end | codeExtended(EndLoop _ :: rest, context) = (* Don't need to do anything. *) codeExtended(rest, context) | codeExtended(JumpLoop{arguments, loopLabel} :: rest, context) = let (* TODO: Make the sources and destinations "friends". *) val code = codeExtended(rest, context) (* Evaluate the arguments. We currently just generate register arguments and that may be simpler anyway. *) fun moveArg {loopReg=PReg(dReg, _), source=RegisterArgument(PReg(sReg, _))} = let val destReg = findGeneralReg dReg val srcReg = findRegister(sReg, SOME destReg, generalRegisters) in {src=srcReg, dst=destReg} end | moveArg _ = raise InternalError "moveArg" val moveList = List.map moveArg arguments in moveMultipleRegisters moveList @ (JumpLoop{arguments=[], loopLabel=loopLabel} :: code) end | codeExtended(RaiseExceptionPacket{ packet=PReg(preg, _) } :: rest, context) = let val () = addRealHint(preg, GenReg eax) val code = codeExtended(rest, context) (* The argument must be put into rax. *) val argReg = findRegister(preg, SOME(GenReg eax), generalRegisters) in moveIfNecessary{src=argReg, dst=raxAsArg} @ RaiseExceptionPacket {packet= raxAsArg } :: code end | codeExtended(ReserveContainer{size, address=PReg(aReg, _)} :: rest, context) = let val code = codeExtended(rest, context) val addrReg = findRegister(aReg, NONE, generalRegisters) (* The memory must be cleared in case we have a GC. *) val pushAll = List.tabulate(size, fn _ => PushValue{arg=IntegerConstant(tag 0)}) in pushAll @ LoadArgument{source=RegisterArgument(GenReg esp), dest=addrReg, kind=MoveWord} :: code end | codeExtended(IndexedCaseOperation{testReg, workReg, cases, startValue} :: rest, context) = raise TooHard NotDoneInstr | codeExtended(LockMutable{addr=RegisterArgument(PReg(pr, _))} :: rest, context) = (* Currently it's always a register. *) let val code = codeExtended(rest, context) val argReg = findRegister(pr, NONE, generalRegisters) in LockMutable{addr=RegisterArgument argReg} :: code end | codeExtended(LockMutable _ :: _, _) = raise InternalError "codeExtended - LockMutable" | codeExtended(ForwardJumpLabel{ label, result=_ } :: rest, context) = ForwardJumpLabel{ label=label, result=NONE } :: codeExtended(rest, context) | codeExtended(UnconditionalForwardJump { label } :: rest, context) = UnconditionalForwardJump { label=label } :: codeExtended(rest, context) | codeExtended(ConditionalForwardJump{ ccRef, condition, label } :: rest, context) = ConditionalForwardJump{ ccRef=ccRef, condition=condition, label=label } :: codeExtended(rest, context) | codeExtended(WordComparison{ arg1 as RegisterArgument _, arg2, ccRef } :: rest, context) = let val code = codeExtended(rest, context) in WordComparison{ arg1=codeExtArgument arg1, arg2=codeExtArgument arg2, ccRef=ccRef } :: code end | codeExtended(WordComparison _ :: _, _) = raise InternalError "codeExtended - WordComparison" (* Set up an exception handler. *) | codeExtended(PushExceptionHandler{handlerAddr=PReg(hReg, _), handleStart} :: rest, context) = let (* handlerAddr is really a work register. *) val code = codeExtended(rest, context) val handleReg = findGeneralReg hReg in PushExceptionHandler{handlerAddr=handleReg, handleStart=handleStart} :: code end (* Pop an exception handler at the end of a handled section. Executed if no exception has been raised. This removes items from the stack. *) | codeExtended(PopExceptionHandler{workReg=PReg(wReg, _), ...} :: rest, context) = let val code = codeExtended(rest, context) val realWork = findGeneralReg wReg in PopExceptionHandler{handlerAddr=realWork (* Not used. *), resultReg=NONE, workReg=realWork} :: code end (* Start of a handler. Sets the address associated with PushExceptionHandler and provides a register for the packet. There is a work register but we could use any register other than rax since we will have pushed anything we need. *) | codeExtended(BeginHandler{handleStart, packetReg=PReg(pReg, _), workReg=_} :: rest, context) = let (* The exception packet is in rax. *) val () = addRealHint(pReg, GenReg eax) val code = codeExtended(rest, context) val realPktReg = findRegister(pReg, SOME(GenReg eax), generalRegisters) in BeginHandler{handleStart=handleStart, workReg=GenReg ebx, packetReg=GenReg eax} :: (moveIfNecessary{src=GenReg eax, dst=realPktReg } @ code) end | codeExtended(ReturnResultFromFunction { resultReg=PReg(resReg, _), numStackArgs } :: rest, context) = let val () = addRealHint(resReg, GenReg eax) val code = codeExtended(rest, context) val resultReg = findRegister(resReg, SOME(GenReg eax), generalRegisters) (* If for some reason it's not in the right register we have to move it there. *) val moveCode = moveIfNecessary{src=resultReg, dst=raxAsArg} in moveCode @ (ReturnResultFromFunction{resultReg=raxAsArg, numStackArgs=numStackArgs} :: code) end | codeExtended(ArithmeticFunction{oper=SUB, resultReg=PReg(resReg, _), operand1=RegisterArgument(PReg(op1Reg, _)), operand2, ccRef} :: rest, context) = (* Subtraction - this is special because it can only be done one way round. The first argument must be in a register. *) let val () = addFriends (resReg, op1Reg) val code = codeExtended(rest, context) val realDestReg = findRegister(resReg, NONE, generalRegisters) (* Try to put the argument into the same register as the result. *) val realOp1Reg = findRegister(op1Reg, SOME realDestReg, generalRegisters) val op2Arg = codeExtArgument operand2 (* If we couldn't put it in the result register we have to copy it there. *) in moveIfNecessary{src=realOp1Reg, dst=realDestReg} @ (ArithmeticFunction{oper=SUB, resultReg=realDestReg, operand1=RegisterArgument realDestReg, operand2=op2Arg, ccRef=ccRef} :: code) end | codeExtended(ArithmeticFunction{oper=SUB, ...} :: _, _) = raise InternalError "codeExtended - ArithmeticFunction" | codeExtended(ArithmeticFunction{oper, resultReg=PReg(resReg, _), operand1=RegisterArgument(PReg(op1Reg, _)), operand2=RegisterArgument(PReg(op2Reg, _)), ccRef} :: rest, context) = (* Arithmetic operation with both arguments as registers. These operations are all symmetric so we can try to put either argument into the result reg and then do the operation on the other arg. *) let val () = addFriends (resReg, op1Reg) val () = addFriends (resReg, op2Reg) val code = codeExtended(rest, context) val realDestReg = findRegister(resReg, NONE, generalRegisters) val realOp1Reg = findRegister(op1Reg, SOME realDestReg, generalRegisters) and realOp2Reg = findRegister(op2Reg, SOME realDestReg, generalRegisters) val (operandReg, moveInstr) = if realOp1Reg = realDestReg then (realOp2Reg, []) else if realOp2Reg = realDestReg then (realOp1Reg, []) else (realOp2Reg, [moveRR{src=realOp1Reg, dst=realDestReg}]) in moveInstr @ (ArithmeticFunction{oper=oper, resultReg=realDestReg, operand1=RegisterArgument realDestReg, operand2=RegisterArgument operandReg, ccRef=ccRef} :: code) end | codeExtended(ArithmeticFunction{oper, resultReg=PReg(resReg, _), operand1=RegisterArgument(PReg(op1Reg, _)), operand2, ccRef} :: rest, context) = (* Arithemtic operation with the first argument in a register and the second a constant or memory location. *) let val () = addFriends (resReg, op1Reg) val code = codeExtended(rest, context) val realDestReg = findRegister(resReg, NONE, generalRegisters) val realOp1Reg = findRegister(op1Reg, SOME realDestReg, generalRegisters) val op2Arg = codeExtArgument operand2 (* If we couldn't put it in the result register we have to copy it there. *) in moveIfNecessary{src=realOp1Reg, dst=realDestReg} @ (ArithmeticFunction{oper=oper, resultReg=realDestReg, operand1=RegisterArgument realDestReg, operand2=op2Arg, ccRef=ccRef} :: code) end | codeExtended(ArithmeticFunction{oper, resultReg=PReg(resReg, _), operand1, operand2=RegisterArgument(PReg(op2Reg, _)), ccRef} :: rest, context) = (* Arithemtic operation with the second argument in a register and the first a constant or memory location. *) let val () = addFriends (resReg, op2Reg) val code = codeExtended(rest, context) val realDestReg = findRegister(resReg, NONE, generalRegisters) val realOp2Reg = findRegister(op2Reg, SOME realDestReg, generalRegisters) val op1Arg = codeExtArgument operand1 in moveIfNecessary{src=realOp2Reg, dst=realDestReg} @ (ArithmeticFunction{oper=oper, resultReg=realDestReg, operand1=RegisterArgument realDestReg, operand2=op1Arg, ccRef=ccRef} :: code) end | codeExtended(ArithmeticFunction _ :: _, _) = raise InternalError "codeExtended - ArithmeticFunction" | codeExtended(TestTagBit{arg as RegisterArgument _, ccRef} :: rest, context) = let (* We currently only handle register arguments but testing a memory operand is perfectly possible. *) val code = codeExtended(rest, context) in TestTagBit{ arg=codeExtArgument arg, ccRef=ccRef } :: code end | codeExtended(TestTagBit _ :: _, _) = raise InternalError "codeExtended - TestTagBit" (* Not currently generated. *) | codeExtended(PushValue _ :: _, _) = raise InternalError "codeExtended - PushValue" | codeExtended(ResetStackPtr {numWords} :: rest, context) = (* This is needed to remove containers on the stack. *) ResetStackPtr{numWords=numWords} :: codeExtended(rest, context) | codeExtended(TagValue{source=PReg(srcReg, _), dest=PReg(dReg, _)} :: rest, context) = let val code = codeExtended(rest, context) in case Array.sub(allocatedRegs, dReg) of SOME regResult => let (* If we're using LEA to tag there's we can use any source register. *) val realSReg = findRegister(srcReg, NONE, generalRegisters) in LoadEffectiveAddress { base=NONE, offset=1, index=MemIndex2 realSReg, dest=regResult } :: code end | NONE => code end | codeExtended(UntagValue{source=RegisterArgument(PReg(sReg, _)), dest=PReg(dReg, _), isSigned} :: rest, context) = (* Always generates register argument at the moment. *) let val () = addFriends (sReg, dReg) val code = codeExtended(rest, context) in case Array.sub(allocatedRegs, dReg) of SOME regResult => let val realSReg = findRegister(sReg, SOME regResult, generalRegisters) in moveIfNecessary{src=realSReg, dst=regResult} @ (ShiftOperation{shift=if isSigned then SAR else SHR, resultReg=regResult, operand=RegisterArgument regResult, shiftAmount=IntegerConstant 1, ccRef=CcRef 0 } :: code) end | NONE => code end | codeExtended(UntagValue _ :: _, _) = raise InternalError "UntagValue" | codeExtended(LoadEffectiveAddress{base=SOME base, offset=0, index=NoMemIndex, dest} :: rest, context) = (* This should be handled at the higher level. *) codeExtended(LoadArgument{source=RegisterArgument base, dest=dest, kind=MoveWord} :: rest, context) | codeExtended(LoadEffectiveAddress{base, offset, index, dest=PReg(dReg, _)} :: rest, context) = let val code = codeExtended(rest, context) val destReg = findGeneralReg dReg val bReg = case base of SOME(PReg(br, _)) => SOME(findGeneralReg br) | NONE => NONE val iReg = codeExtIndex index in LoadEffectiveAddress{base=bReg, offset=offset, index=iReg, dest=destReg} :: code end | codeExtended(ShiftOperation{shift, resultReg=PReg(resReg, _), operand=RegisterArgument(PReg(operReg, _)), shiftAmount=IntegerConstant i, ccRef} :: rest, context) = let val () = addFriends (resReg, operReg) val code = codeExtended(rest, context) val realDestReg = findRegister(resReg, NONE, generalRegisters) val realOpReg = findRegister(operReg, SOME realDestReg, generalRegisters) in moveIfNecessary{src=realOpReg, dst=realDestReg} @ (ShiftOperation{shift=shift, resultReg=realDestReg, operand=RegisterArgument realDestReg, shiftAmount=IntegerConstant i, ccRef=ccRef} :: code) end | codeExtended(ShiftOperation{shift, resultReg=PReg(resReg, _), operand=RegisterArgument(PReg(operReg, _)), shiftAmount=RegisterArgument(PReg(shiftReg, _)), ccRef} :: rest, context) = let val () = addFriends (resReg, operReg) val () = addRealHint(shiftReg, GenReg ecx) val code = codeExtended(rest, context) val realDestReg = findRegister(resReg, NONE, generalRegisters) val realShiftReg = findRegister(shiftReg, SOME(GenReg ecx), generalRegisters) val realOpReg = findRegister(operReg, SOME realDestReg, generalRegisters) (* We want the shift in ecx. We may not have got it there but the register should be free. *) in moveIfNecessary{src=realOpReg, dst=realDestReg} @ moveIfNecessary{src=realShiftReg, dst=GenReg ecx} @ (ShiftOperation{shift=shift, resultReg=realDestReg, operand=RegisterArgument realDestReg, shiftAmount=RegisterArgument(GenReg ecx), ccRef=ccRef} :: code) end | codeExtended(ShiftOperation _ :: _, _) = raise InternalError "codeExtended - ShiftOperation" | codeExtended( Multiplication{resultReg=PReg(resReg, _), operand1=RegisterArgument(PReg(op1Reg, _)), operand2=RegisterArgument(PReg(op2Reg, _)), ccRef} :: rest, context) = let (* Treat exactly the same as ArithmeticFunction. *) val () = addFriends (resReg, op1Reg) val () = addFriends (resReg, op2Reg) val code = codeExtended(rest, context) val realDestReg = findRegister(resReg, NONE, generalRegisters) val realOp1Reg = findRegister(op1Reg, SOME realDestReg, generalRegisters) and realOp2Reg = findRegister(op2Reg, SOME realDestReg, generalRegisters) val (operandReg, moveInstr) = if realOp1Reg = realDestReg then (realOp2Reg, []) else if realOp2Reg = realDestReg then (realOp1Reg, []) else (realOp2Reg, [moveRR{src=realOp1Reg, dst=realDestReg}]) in moveInstr @ (Multiplication{resultReg=realDestReg, operand1=RegisterArgument realDestReg, operand2=RegisterArgument operandReg, ccRef=ccRef} :: code) end (* We currently only generate the register/register case. *) | codeExtended(Multiplication _ :: _, _) = raise InternalError "codeExtended - multiplication TODO" | codeExtended(Division{isSigned, dividend=PReg(regDivid, _), divisor, quotient=PReg(regQuot, _), remainder=PReg(regRem, _)} :: rest, context) = let (* Division is specific as to the registers. The dividend must be eax, quotient is eax and the remainder is edx. *) val () = addRealHint(regDivid, GenReg eax) val () = addRealHint(regQuot, GenReg eax) val () = addRealHint(regRem, GenReg edx) val code = codeExtended(rest, context) val realDiviReg = findRegister(regDivid, SOME(GenReg eax), generalRegisters) val realQuotReg = findRegister(regQuot, SOME(GenReg eax), generalRegisters) val realRemReg = findRegister(regRem, SOME(GenReg edx), generalRegisters) val divisorArg = codeExtArgument divisor in (* We may need to move one or more of the registers although normally that won't be necessary. Almost certainly only either the remainder or the quotient will actually be used. *) moveIfNecessary{src=realDiviReg, dst=GenReg eax} @ Division{isSigned=isSigned, dividend=GenReg eax, divisor=divisorArg, quotient=GenReg eax, remainder=GenReg edx} :: moveMultipleRegisters[{src=GenReg eax, dst=realQuotReg}, {src=GenReg edx, dst=realRemReg}] @ code end | codeExtended(AtomicExchangeAndAdd{base=PReg(bReg, _), source=PReg(sReg, _)} :: rest, context) = let val code = codeExtended(rest, context) val srcReg = findGeneralReg sReg val baseReg = findGeneralReg bReg in AtomicExchangeAndAdd{base=baseReg, source=srcReg} :: code end | codeExtended(BoxValue{boxKind=BoxLargeWord, source=PReg(sReg, _), dest=PReg(dReg, _), saveRegs} :: rest, context) = let val code = codeExtended(rest, context) val preserve = List.map(fn (PReg(r, _)) => findGeneralReg r) saveRegs val srcReg = findGeneralReg sReg and dstReg = findGeneralReg dReg in AllocateMemoryOperation{ size=1, flags=0wx1, dest=dstReg, saveRegs=preserve} :: StoreArgument{ source=RegisterArgument srcReg, offset=0, base=dstReg, index=NoMemIndex, kind=MoveWord} :: InitialisationComplete{dest=dstReg (* unused *)} :: code end | codeExtended(BoxValue{boxKind, source, dest, saveRegs} :: rest, context) = let in raise TooHard NotDoneInstr end | codeExtended(CompareByteVectors{vec1Addr=PReg(v1Reg, _), vec2Addr=PReg(v2Reg, _), length=PReg(lReg, _), ccRef} :: rest, context) = let val () = addRealHint(v1Reg, GenReg esi) val () = addRealHint(v2Reg, GenReg edi) val () = addRealHint(lReg, GenReg ecx) val code = codeExtended(rest, context) val realV1Reg = findRegister(v1Reg, SOME(GenReg esi), generalRegisters) val realV2Reg = findRegister(v2Reg, SOME(GenReg edi), generalRegisters) val realLengthReg = findRegister(lReg, SOME(GenReg ecx), generalRegisters) (* There's a complication here. CompareByteVectors generates REPE CMPSB to compare the vectors but the condition code is only set if CMPSB is executed at least once. If the value in RCX/ECX is zero it will never be executed and the condition code will be unchanged. We want the result to be "equal" in that case so we need to ensure that is the case. It's quite possible that the condition code has just been set by shifting RCX/ECX to remove the tag in which case it will have set "equal" if the value was zero. We use CMP R/ECX,R/ECX which is two bytes in 32-bit but three in 64-bit. If we knew the length was non-zero (e.g. a constant) we could avoid this. *) in moveIfNecessary{src=realV1Reg, dst=GenReg esi} @ moveIfNecessary{src=realV2Reg, dst=GenReg edi} @ moveIfNecessary{src=realLengthReg, dst=GenReg ecx} @ (WordComparison {arg1=RegisterArgument rcxAsArg, arg2=RegisterArgument rcxAsArg, ccRef=ccRef} :: CompareByteVectors{vec1Addr=GenReg esi, vec2Addr=GenReg edi, length=GenReg ecx, ccRef=ccRef} :: code) end | codeExtended(BlockMove{srcAddr=PReg(sReg, _), destAddr=PReg(dReg, _), length=PReg(lReg, _), isByteMove} :: rest, context) = let val () = addRealHint(sReg, GenReg esi) val () = addRealHint(dReg, GenReg edi) val () = addRealHint(lReg, GenReg ecx) val code = codeExtended(rest, context) val realSrcReg = findRegister(sReg, SOME(GenReg esi), generalRegisters) val realDestReg = findRegister(dReg, SOME(GenReg edi), generalRegisters) val realLengthReg = findRegister(lReg, SOME(GenReg ecx), generalRegisters) in moveIfNecessary{src=realSrcReg, dst=GenReg esi} @ moveIfNecessary{src=realDestReg, dst=GenReg edi} @ moveIfNecessary{src=realLengthReg, dst=GenReg ecx} @ (BlockMove{srcAddr=GenReg esi, destAddr=GenReg edi, length=GenReg ecx, isByteMove=isByteMove} :: code) end | codeExtended(CompareFloatingPt{arg1, arg2, ccRef} :: rest, context) = raise TooHard NotDoneInstr | codeExtended(X87FPGetCondition{dest, ccRef} :: rest, context) = raise TooHard NotDoneInstr | codeExtended(X87FPArith{opc, resultReg, arg1, arg2} :: rest, context) = raise TooHard NotDoneInstr | codeExtended(X87FPUnaryOps{fpOp, dest, source} :: rest, context) = raise TooHard NotDoneInstr | codeExtended(FloatFixedInt{dest, source} :: rest, context) = raise TooHard NotDoneInstr | codeExtended(SSE2FPArith{opc, resultReg, arg1, arg2} :: rest, context) = raise TooHard NotDoneInstr val icodeTabs = [8, 20, 60] val () = (* Print the code before the transformation. *) if DEBUG.getParameter DEBUG.icodeTag debugSwitches then let val printStream = PRETTY.getSimplePrinter(debugSwitches, icodeTabs) fun printRegs([], _) = () | printRegs(_, 0) = printStream "..." | printRegs([i], _) = printStream(Int.toString i) | printRegs(i::l, n) = (printStream(Int.toString i ^ ","); printRegs(l, n-1)) fun printCode c = ( printICodeAbstract(c, printStream); printStream "\n" ) fun printRegData(i, { conflicts, realConflicts=_, active, defs, refs, pushState }) = ( printStream (Int.toString i ^ "\t"); printStream ("Conflicts="); printRegs(conflicts, 20); printStream (" Active=" ^ Int.toString active); printStream (" Rfs=" ^ Int.toString refs); printStream (" Defs=" ^ Int.toString defs); case pushState of MustPush => printStream " Must push" | MustNotPush => printStream " No push" | MayPush => (); printStream "\n" ) in printStream(functionName ^ "\n"); List.app printCode identifiedCode; printStream "\n"; Vector.appi printRegData regStates end else () val () = totalFns := !totalFns + 1 val postTransformCode = let val code = codeExtended(identifiedCode, []) val _ = if !reportSuccess then print("-------Done " ^ functionName ^ "\n") else () val () = successFns := !successFns + 1 in code end handle TooHard reason => let val () = reportSuccess := false val incrReg = case reason of NotEnoughRegs => tooManyRegs | MustPushReg => mustPushReg | NotDoneInstr => notDoneInstr | OtherReason => anOther val () = incrReg := !incrReg + 1 val (fnState, fnCode) = codeICode{icode=icode, state=NormalState initialState, code=[], context={loopArgs=[], forwardLabels=[], handlers=[]}} val _ = case fnState of Exited => () | _ => raise InternalError "fnstate not exited" in List.rev fnCode (* Reverse the list *) end val () = if !totalFns mod 200 = 0 then print(concat["---Succeeded ", Int.toString(!successFns), " of ", Int.toString(!totalFns), " Not done=", Int.toString(!notDoneInstr), " Too many regs=", Int.toString(!tooManyRegs), " Must push=", Int.toString(!mustPushReg), " Another=", Int.toString(!anOther), "\n"]) else () val () = (* Print the code after the transformation. *) if DEBUG.getParameter DEBUG.icodeTag debugSwitches then let val printStream = PRETTY.getSimplePrinter(debugSwitches, icodeTabs) fun printCode c = ( printICodeConcrete(c, printStream); printStream "\n") in printStream(functionName ^ "\n"); List.app printCode postTransformCode; printStream "\n" end else () in (* Ccode-generate it. *) codeAsX86Code{icode=postTransformCode, maxLabels = !labelCounter, stackRequired = !maxStack, inputRegisters= argRegsUsed @ (if hasFullClosure then [GenReg edx] else []), debugSwitches=debugSwitches, functionName=functionName} end structure Sharing = struct type 'reg x86ICode = 'reg x86ICode and abstract = abstract and reg = reg end end; diff --git a/mlsource/MLCompiler/CodeTree/X86Code/ml_bind.ML b/mlsource/MLCompiler/CodeTree/X86Code/ml_bind.ML index 8a4d6a90..57b260d7 100644 --- a/mlsource/MLCompiler/CodeTree/X86Code/ml_bind.ML +++ b/mlsource/MLCompiler/CodeTree/X86Code/ml_bind.ML @@ -1,69 +1,81 @@ (* Copyright David C. J. Matthews 2015-16 This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License version 2.1 as published by the Free Software Foundation. This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with this library; if not, write to the Free Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA *) local structure X86OutputCode = X86OUTPUTCODE( structure DEBUG = Debug structure PRETTY = Pretty ) structure X86Optimise = X86OPTIMISE( structure X86CODE = X86OutputCode ) structure X86ForeignCall = X86FOREIGNCALL ( structure DEBUG = Debug structure X86CODE = X86OutputCode structure X86OPTIMISE = X86Optimise ) structure X86ICode = X86ICodeToX86Code ( structure DEBUG = Debug structure X86CODE = X86OutputCode structure X86OPTIMISE = X86Optimise ) structure X86ICodeIdentify = X86ICodeIdentifyReferences ( structure DEBUG = Debug structure ICODE = X86ICode ) + structure Strongly = + StronglyConnected ( + structure Graph = + struct + open X86ICode + type node = {src: reg argument, stack: int} + fun nodeAddress({stack, ...}: node) = stack + fun arcs({src=StackLocation{wordOffset, ...}, ...}: node) = [wordOffset] | arcs _ = [] + end + ) + structure X86ICodeTransform = X86ICodeTransform ( structure DEBUG = Debug structure ICODE = X86ICode structure IDENTIFY = X86ICodeIdentify structure PRETTY = Pretty + structure STRONGLY = Strongly ) in structure X86Code = X86CodetreeToICode ( structure BACKENDTREE = BackendIntermediateCode structure DEBUG = Debug structure ICODE = X86ICode structure X86FOREIGN = X86ForeignCall structure ICODETRANSFORM = X86ICodeTransform ) end; diff --git a/mlsource/MLCompiler/CodeTree/ml_bind.ML b/mlsource/MLCompiler/CodeTree/ml_bind.ML index 4ed4e2fb..2752a1bd 100644 --- a/mlsource/MLCompiler/CodeTree/ml_bind.ML +++ b/mlsource/MLCompiler/CodeTree/ml_bind.ML @@ -1,88 +1,100 @@ (* Copyright (c) 2000 Cambridge University Technical Services Limited This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 2.1 of the License, or (at your option) any later version. This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. You should have received a copy of the GNU Lesser General Public License along with this library; if not, write to the Free Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA *) local + structure StronglyConnectMutuals = + StronglyConnected( + structure Graph = + struct + open BaseCodeTree + type node = { addr: int, lambda: lambdaForm, use: codeUse list } + fun nodeAddress({addr, ...}: node) = addr + and arcs({lambda={closure, ...}, ...}: node) = + List.foldl(fn (LoadLocal addr, l) => addr :: l | (_, l) => l) [] closure + end + ) + structure CodetreeFunctions = - CODETREE_FUNCTIONS(structure BASECODETREE = BaseCodeTree) + CODETREE_FUNCTIONS(structure BASECODETREE = BaseCodeTree and STRONGLY = StronglyConnectMutuals) structure CodetreeBackend = CODETREE_STATIC_LINK_AND_CASES( structure PRETTY = Pretty structure GCODE = GCode structure DEBUG = Debug structure BASECODETREE = BaseCodeTree structure BACKENDTREE = BackendIntermediateCode structure CODETREE_FUNCTIONS = CodetreeFunctions ) structure CodetreeLamdbaLift = CODETREE_LAMBDA_LIFT ( structure BASECODETREE = BaseCodeTree and CODETREE_FUNCTIONS = CodetreeFunctions and BACKEND = CodetreeBackend and PRETTY = Pretty and DEBUG = Debug ) structure CodetreeCodegenConstantFns = CODETREE_CODEGEN_CONSTANT_FUNCTIONS ( structure BASECODETREE = BaseCodeTree and CODETREE_FUNCTIONS = CodetreeFunctions and BACKEND = CodetreeLamdbaLift and PRETTY = Pretty and DEBUG = Debug ) structure CodetreeRemoveRedundant = CODETREE_REMOVE_REDUNDANT( structure BASECODETREE = BaseCodeTree structure CODETREE_FUNCTIONS = CodetreeFunctions ) structure CodetreeSimplifier = CODETREE_SIMPLIFIER( structure BASECODETREE = BaseCodeTree structure CODETREE_FUNCTIONS = CodetreeFunctions structure REMOVE_REDUNDANT = CodetreeRemoveRedundant ) structure CodetreeOptimiser = CODETREE_OPTIMISER( structure PRETTY = Pretty structure DEBUG = Debug structure BASECODETREE = BaseCodeTree structure CODETREE_FUNCTIONS = CodetreeFunctions structure BACKEND = CodetreeCodegenConstantFns structure REMOVE_REDUNDANT = CodetreeRemoveRedundant structure SIMPLIFIER = CodetreeSimplifier ) in structure CodeTree = CODETREE ( structure PRETTY = Pretty structure DEBUG = Debug structure BASECODETREE = BaseCodeTree structure CODETREE_FUNCTIONS = CodetreeFunctions structure BACKEND = CodetreeCodegenConstantFns structure OPTIMISER = CodetreeOptimiser ) end; diff --git a/mlsource/MLCompiler/StronglyConnected.sml b/mlsource/MLCompiler/StronglyConnected.sml new file mode 100644 index 00000000..4e9e56e6 --- /dev/null +++ b/mlsource/MLCompiler/StronglyConnected.sml @@ -0,0 +1,123 @@ +(* + Copyright (c) 2016 David C.J. Matthews + + This library is free software; you can redistribute it and/or + modify it under the terms of the GNU Lesser General Public + License version 2.1 as published by the Free Software Foundation. + + This library is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU + Lesser General Public License for more details. + + You should have received a copy of the GNU Lesser General Public + License along with this library; if not, write to the Free Software + Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA +*) + +functor StronglyConnected( +structure Graph: +sig + (* A node has an address and arcs are the addresses of other nodes. *) + type node + val nodeAddress: node -> int + val arcs: node -> int list +end): +sig + type node + val stronglyConnectedComponents: node list -> node list list +end += +struct + open Graph + + fun stronglyConnectedComponents [] = [] + | stronglyConnectedComponents (rlist as firstNode :: _) = + (* In general any mutually recursive declaration can refer to any + other. It's better to partition the recursive declarations into + strongly connected components i.e. those that actually refer + to each other. *) + let + local + val anAddr = nodeAddress firstNode + in + val (startAddress, lastAddress) = + List.foldl (fn(item, (mn, mx)) => let val addr = nodeAddress item in (Int.min(addr, mn), Int.max(addr+1, mx)) end) (anAddr, anAddr) rlist + end + (* *) + val mapArray = Array.array(lastAddress - startAddress, NONE) + + fun updateMin(addr, try) = + let + val off = addr - startAddress + val { lowLink, index } = valOf(Array.sub(mapArray, off)) + in + Array.update(mapArray, off, SOME{ index = index, lowLink = Int.min(lowLink, try) }) + end + + fun addrInList a = List.exists(fn item => a = nodeAddress item) + + fun strongcomponent(item, (thisIndex, stack, resList)) = + let + val addr = nodeAddress item + val allArcs = arcs item + val newStack = item :: stack + val v = addr - startAddress + (* Mark this item as processed. *) + val () = Array.update(mapArray, v, SOME{index = thisIndex, lowLink = thisIndex}) + + (* Process links that refer to other items *) + fun processLink(a: int, args as (_, stack, _)) = + if addrInList a rlist + then (* It refers to another within this declaration *) + let + val w = a - startAddress + in + case Array.sub(mapArray, w) of + NONE => (* Not yet processed. *) + let + val result = strongcomponent(valOf(List.find(fn item => nodeAddress item = a) rlist), args); + in + updateMin(addr, #lowLink(valOf(Array.sub(mapArray, w)))); + result + end + | SOME _ => + ( + (* Already processed - was it in this pass or a previous? *) + if addrInList a stack (* On the stack so in the current SCC *) + then updateMin(addr, #index(valOf(Array.sub(mapArray, w)))) + else (); (* Processed in previous pass *) + args + ) + end + else args + + val (nextIndex, stack', subRes) = List.foldl processLink (thisIndex+1, newStack, resList) allArcs + in + (* Process references from this function. *) + if #lowLink(valOf(Array.sub(mapArray, v))) = thisIndex (* This is the minimum *) + then (* Create an SCC *) + let + fun popItems([], _) = raise Fail "stack empty" + | popItems(item :: r, l) = + if nodeAddress item = addr + then (r, item :: l) + else popItems(r, item :: l) + val (newStack, scc) = popItems(stack', []) + in + (nextIndex, newStack, scc :: subRes) + end + else (nextIndex, stack', subRes) + end + + (* Process items that have not yet been reached *) + fun processUnprocessed (item, args) = + case Array.sub(mapArray, nodeAddress item-startAddress) of + NONE => strongcomponent(item, args) + | _ => args + + val (_, _, result) = List.foldl processUnprocessed (0, [], []) rlist + in + result + end +end; diff --git a/polyml.pyp b/polyml.pyp index f5297c0f..e90f10a1 100644 --- a/polyml.pyp +++ b/polyml.pyp @@ -1,231 +1,232 @@ +