Typed Assembly Language (2000)

▲ Typed Assembly Language (2000)(cs.cornell.edu)

43 points by luu 3 days ago | 17 comments

▲ addaon 3 days ago | parent | next [-]

I think a challenge to me for typing assembly, unless you’re doing old-school C style minimally-useful types, is that assembly types tend to be both more ad hoc and more transient than types in higher level languages, because these types come from the intersection of the problem domain and the way of expressing the solution, instead of just from the problem domain. In C++ I might have a type for “aircraft velocity in mm/s”, but in assembly I might have that type on one line, and then go to velocity in 2x mm/s the next line to save a renormalization; or have types for various state flags, but have them pack differently into a word in different places in the code. This is all expressible, but I think it would make me favor a more implicit typing with a heavier emphasis on deduction, just to minimize the description of types that exist but are not in themselves interesting.

	▲	noduerme an hour ago \| parent [-]
		Just thinking about an aircraft's velocity as a specific type, rather than a vector with three floats, has my mind whirling. I can imagine a lot of terrifying things I wish I didn't think could be added later to that struct in some avionics system. What would you need a type for that for? Am I thinking too high level, where this type might include its own getters and function calls?

▲ estimator7292 3 days ago | parent | prev | next [-]

If you're gonna make a website for your programming language, you NEED to put an example of the language front and center on the landing page.

Three links deep and I finally found some code... packaged in a gz archive. I still have not seen a line of TAL

▲ impl 7 hours ago | parent | next [-]

This website is at least 25 years old. It uses one of the pre-canned templates from FrontPage 2000. Cut 'em a little slack. :-)

This was obviously someone's research project, and some of the papers have example code in them, e.g. see https://www.cs.cornell.edu/talc/papers/talx86-wcsss.pdf.

	▲	hackingonempty 5 hours ago \| parent [-]
		> This website is at least 25 years old. That would explain why it only supports IA32.

▲ az09mugen 2 days ago | parent | prev | next [-]

Same here, partial code from stackcodegen.ml in the said archive :

open Op;; open Var;; open Ctx;; open Ltal;; open Util;;

let debug msg = ();;

let rs = mkvar "rs";; let ra = mkvar "ra";; let rf = mkvar "rf";; let rt = mkvar "rt";; let rr = mkvar "rr";; let ru = mkvar "ru";;

let retty stackty aty = (Code(Ctx.from_list[(rs,stackty); (ra,aty); (rt,toptp); (rf,listtp); (rr,toptp)]))

let rec tt tctx ctx tp = match tp with Il.TVar a -> if bound tctx a then TVar a else lookup ctx a | Il.Int -> DTp Word | Il.Top -> DTp Top (* for now ) | Il.Tensor(t1,t2) -> Ref(Tcltal.mkpair (tt tctx ctx t1, tt tctx ctx t2)) | Il.Exists (alpha, tp) -> let beta = rename alpha in Exists (beta, W, tt tctx (extend ctx alpha (TVar beta)) tp) | Il.List t -> let tv = mkvar "list" in Mu(tv,NRef(Tcltal.mkpair(tt tctx ctx t, TVar tv))) | _ -> DTp(arrowtt tctx ctx tp)

and arrowtt tctx ctx t = match t with Il.Forall(alpha,t) -> let beta = Var.rename alpha in Forall(beta, W, arrowtt tctx (extend ctx alpha (TVar beta)) t) | Il.Arrow(t1,t2) -> let t1' = tt tctx ctx t1 in let t2' = tt tctx ctx t2 in let stk = mkvar "s" in Forall (stk,M, Code(Ctx.from_list[(rs,Stack(Tensor(t1',MTVar stk))); (ra,toptp); (rt,toptp); (rf,listtp); (rr,DTp(retty (Stack(MTVar stk)) t2'))]))

  | _ -> tcfail "expected a function type in forall"

let typetrans tctx tp = tt tctx Ctx.emp tp let arrowtypetrans tctx t1 t2 = arrowtt tctx Ctx.emp (Il.Arrow (t1,t2))

( Need to specify the type ty of "the rest of the stack", in most cases alpha )

type code_env = {cctx : cctx; cs : code_section; fctx : Il.ctx; lctx : var Ctx.ctx; fp : int}

let get_fctx cenv = cenv.fctx let get_lctx cenv = cenv.lctx

type block_env = {cenv : code_env; ilist : instruction list; lab : clab; tctx : Ltal.tctx; rctx : Ltal.rctx}

let get_from_cenv f benv = f benv.cenv

exception CodeFail of string code_env exception BlockFail of string * block_env

(* val begin_fn : code_env -> clab -> register_file -> block_env val end_fn : block_env -> code_env val emit_label : fn_env -> clab -> dtp -> block_env val emit : block_env -> instruction -> block_env -> block_env val emit_end : end_instruction -> block_env -> fn_env val drop : reg -> block_env -> block_env val free : reg -> block_env -> block_env val push : reg -> reg -> block_env -> block_env val pop : reg -> reg -> block_env -> block_env val malloc : reg -> block_env -> block_env )

let do_print y x = (debug y; x)

let (>>) f g x = g(f(x)) let (>>=) f h x = let y = f x in h y x

let rec mkltp tctx rctx = Ctx.fold (fun t sk dtp -> let k = match sk with _,W -> W | _,M -> M in Forall(t,k,dtp)) tctx (Code (rctx))

let current_ltp benv = debug ("Generalizing "^(Ctx.pp_ctx (fun _ -> "") benv.tctx)^"\n"); ( rt is caller-save *) let rctx = update benv.rctx rt toptp in (mkltp benv.tctx rctx)

▲ geocar 6 hours ago | parent | prev [-]

> If you're gonna make a website for your programming language, you NEED to put an example of the language front and center on the landing page.

Did you consider the possibility that this sort of thing was done to avoid wasting time with non-experts who think an "example" of a language they don't know is enough to make comments about?

> I still have not seen a line of TAL

My suggestion: Start with the "Papers" and then look at the paper that introduces TAL. It has an example program with analysis

▲

makerofthings 6 hours ago | parent [-]

I’m an expert and I find it very frustrating when I don’t find some example code front and centre. It might not reveal the detail, but it sets the scene quickly and lets me know what sort of a thing I’m dealing with.

▲

geocar 6 hours ago | parent [-]

> I’m an expert and I find it very frustrating

So you say, but I think _I'm_ an expert too, and I wasn't frustrated in the slightest. Maybe you're just not an expert in this space. Did you consider that?

Of course it would be nice if everyone communicated to us in our preferred way, but I think making the reader work a little bit before they have a conversation is a good way to figure out if you're dealing with an expert or not, because an expert actually worth talking to about your ideas will not find it to be too much work to understand them

Students can especially benefit from this advice, because they are still too new to be able to recognise experts from the substance of their words

▲

nananana9 5 hours ago | parent [-]

"I don't like having my time wasted" does not imply anything about one's skill in a field.

It's not 1995. Most of the internet is noise, and if you're showcasing something it's good form to immediately show your readers what actually is, and why they may or may not care about it.

Not showing the syntax of a programming language on the homepage of a programming language is poor communication. If you're OK with that - great, but not valuing your time and willingness to have it wasted in no way implies that you're an "expert".

	▲	geocar 5 hours ago \| parent [-]
		> "I don't like having my time wasted" does not imply anything about one's skill in a field. I have no idea what you think you just said, but I did not say anything like that. > Most of the internet is noise, and if you're showcasing something it's good form to immediately show your readers what actually is So you say, but without responding to either of my suggestions for not doing this, and after saying something that doesn't sound relevant at all. Of what exactly are you trying to convince me to do? I'm not the author of this page, I'm not confused by what TAL is, and I'm not going to agree that you don't deserve to have your time wasted when you're here wasting mine, so what is it?

▲ fnky 2 hours ago | parent | prev | next [-]

You know it's good when all the members have their home addresses listed on their personal websites.

Too bad there's no examples of how this looked like.

▲ Surac 6 hours ago | parent | prev | next [-]

Reinventing C?

▲ leptons 7 hours ago | parent | prev [-]

I feel like this is a solution in search of a problem that was already solved by C.

▲

geocar 6 hours ago | parent | next [-]

These "types" are hindley-milner types and have almost nothing to do with what C calls a type.

Your "feelings" may help you make snap judgements that can keep you alive, but they cannot help you code and they will conspire against you when you effort to learn new things. Nobody wants to feel wrong, and you will feel wrong many times when you learn something new, but it is the only way to actually learn the thing. Remember this the next time you have "feelings" about knowledge

	▲	leptons 6 hours ago \| parent [-]
		You don't know me.

▲

pjmlp 2 hours ago | parent | prev [-]

Except C being typed Assembly is a myth, first of all there were already high level systems languages during the decade that predates C, secondly there are plenty of CPU capabilities not exposed in C, if at all only via compiler specific language extensions, beyond the language standard.