8
$\begingroup$

I'm writing my Bsc thesis about type systems of various languages and I want to have a short section about assembly languages. Initially I thought I'll bring up assembly as a counter example to languages with advanced type systems. My goal was to explore the reasons why assembly omits most (all?) type system features but eventually I found papers about typed assembly languages and I started to get confused. So here are my questions:

  • Can we say that assembly is generally untyped? If so, what is the reason we don't have assemblers with advanced types and type checkers?
  • Arguments for having a typed assembly language?

Here is a list of papers about typed assembly languages from the end of the last century: http://www.cs.cornell.edu/talc/papers.html. Links to other papers are highly appreciated!

$\endgroup$
  • 2
    $\begingroup$ There are a number of strongly-typed intermediate languages for various runtime environments, which often have similarities to assembly languages while enforcing high-level type safety guarantees. Examples include JVM .class file bytecode and .NET CIL. $\endgroup$ – Aaron Rotenberg Dec 27 '19 at 22:24
3
$\begingroup$

Assembly language is normally untyped, in the sense that there is no type-checking. Adding type-checking is a non-trivial research challenge (hence the papers you see). Papers on typed assembly language should explain the motivation. One application is that they can be used to support proof-carrying code, which can be used to securely execute untrusted code. Another potential application is to support formal verification. But I suggest reading some of the key papers to see what they say about the applications and motivation for typed assembly language.

You can find other papers yourself by doing a literature search -- see https://crypto.stackexchange.com/q/8316/351.

| cite | improve this answer | |
$\endgroup$
3
$\begingroup$
  • Can we say that assembly is generally untyped?

If you mean "assembly" as, e.g. x86 assembly language, then I think yes, to some degree. Types are some constraints that we can statically checked/proved, then there is so little (but not nothing) we can do given an x86 assembly program, e.g.

add rcx, [@addr]
jmp rcx

so it's possible to infer that [@addr] is a 64-bit memory values starting from @addr, but it's very hard to statically check whether the next jmp rcx is safe or not because we must know whether rcx is a valid address which contains executable code.

Another example is

mov rax, @pointer0
mov rcx, @pointer1
add rax, rcx

suppose that @pointer0 and @pointer1 are valid pointers, then this program should not type-check because adding two pointers seems meaningless. But x86 assembly allows that.

If we add an "advanced" type system into x86 assembly language, then... it wouldn't be this language anymore (the type system isn't independent from the language).

  • Arguments for having a typed assembly language?

Typed assembly language (TAL) means intermediate languages (not adding type system into existing x86 assembly language), its goals is (verbatim from the paper):

...to provide a fully automatic way to verify that programs will not violate the primitive abstractions of the language.

that means, given some program (at a high-level language) which has been type-checked to satisfy some properties, then when the program is compiled into another program (in TAL), we can still check (in TAL) that these properties are satisfied.

| cite | improve this answer | |
$\endgroup$
2
$\begingroup$

Many assembly languages do have certain features that could be considered static typing. Most often this is for making programming easier, rather than type checking.

In many assembly languages you can define the equivalent of C's structs and unions. Many assembly languages also allow the usage of arrays, where the type (in the sense of byte-count) of the elements is determined at assemble time.

n.b. "x86 assembly" is a very vague term; every assembler has its own dialect. I'll refer to MASM, as it is the most featureful assembler.

It says a lot that MASM has the TYPEDEF keyword. It also has the ASSUME keyword which marks the value of a register as a pointer to a specific type which will affect later usages of the register. You can also use LENGTHOF, SIZEOF, and TYPE for arrays which return statically-available information.

In MASM, there is a distinction between near and far addresses and variables can be declared with certain types. Structs can be defined with a particular alignment which influences how the fields are accessed. Structs, unions and arrays can be nested. Bitfield types also exist.

ARM assembly is intended to be a compiler target rather than convenient for humans (as far as assemblies go) so it doesn't have any of these features.

Regarding machine code itself: Theoretically it is possible for a computer architecture to use extra bits to determine the type of that word. Some old computer architectures did use an extra bit to distinguish data from pointers.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ This is an interesting distinction from the situation with intermediate languages that I mentioned in a comment on the question. MASM has some data type support, but this is only present at the assembler level and disappears when you get down to machine code. By contrast, JVM bytecode includes type information that is checked by the virtual machine as part of the classloading process at runtime. $\endgroup$ – Aaron Rotenberg Dec 29 '19 at 4:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.