Skip to content

GitLab

Commit 891c3d2d authored by mb0's avatar mb0
Browse files

Up.

parent f7022e80
Hide whitespace changes
Inline Side-by-side
Showing with 239 additions and 129 deletions
detail/codegen/codegen-mangle.sml
View file @ 891c3d2d
......@@ -69,9 +69,9 @@ structure Mangle = struct
| #"=" => "_eq_"
| #"!" => "_ex_"
| #"*" => "_star_"
| #"-" => "_minus_"
| #"-" => "_"
| #"+" => "_plus_"
| #"^" => "_concat_"
| #"^" => "_hat_"
| #"/" => "_slash_"
| #"?" => "_q_"
| _ => String.str c
......
detail/semantic/inference.sml
View file @ 891c3d2d
......@@ -131,7 +131,7 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
(* define a second traversal that is a full inference of the tree *)
(*local helper function to infer types for a binding group*)
val maxIter = 1
val maxIter = 2
fun calcSubset printWarn env =
let
fun checkUsage sym (s, unstable) =
......@@ -762,7 +762,7 @@ fun typeInferencePass (errStrm, ti : TI.type_info, ast) = let
) toplevelEnv (ast : SpecAbstractTree.specification)
val toplevelEnv = calcFixpoint toplevelEnv
handle TypeError => toplevelEnv
(*val _ = TextIO.print ("toplevel environment:\n" ^ E.toString toplevelEnv)*)
val _ = TextIO.print ("toplevel environment:\n" ^ E.toString toplevelEnv)
(* check if all exported functions can be run with an empty state *)
fun checkDecoder s sym = case E.forceNoInputs (sym,toplevelEnv) of
......
specifications/basis/bbtree.ml
View file @ 891c3d2d
......@@ -18,18 +18,18 @@ export =
bbtree-empty
bbtree-singleton
bbtree-add
bbtree-addWith
bbtree-add-with
bbtree-intersection
bbtree-difference
bbtree-contains?
bbtree-simpleUnion
bbtree-splitLessThan
bbtree-splitGreaterThan
bbtree-simple-union
bbtree-split-less-than
bbtree-split-greater-than
bbtree-union
bbtree-remove
bbtree-removeMin
bbtree-remove-min
bbtree-get
bbtree-getOrElse
bbtree-get-orelse
bbtree-fold
bbtree-pretty
......@@ -42,7 +42,7 @@ export =
intset-contains?
intset-union
intset-remove
intset-removeMin
intset-remove-min
intset-fold
fitree-lt?
......@@ -52,10 +52,11 @@ export =
fitree-add
fitree-intersection
fitree-difference
fitree-interval-difference
fitree-contains?
fitree-union
fitree-remove
fitree-removeMin
#fitree-remove
fitree-remove-min
fitree-fold
fitree-pretty
fitree-mk
......@@ -63,9 +64,9 @@ export =
#type intset = bbtree [a=int]
#type fitree = bbtree [a={lo:int,hi:int}]
type bbtree =
type bbtree [a] =
Lf
| Br of {size: int, left: bbtree, right: bbtree, payload: int}
| Br of {size: int, left: bbtree, right: bbtree, payload: a}
val bbtree-size t =
case t of
......@@ -187,14 +188,14 @@ val bbtree-add lt? bt x =
else mkBr x t.size t.left t.right
end
val bbtree-addWith lt? f bt x =
val bbtree-add-with lt? f bt x =
case bt of
Lf: mkBr x 1 bt bt
| Br t:
if lt? x t.payload
then mkT t.payload (bbtree-addWith lt? f t.left x) t.right
then mkT t.payload (bbtree-add-with lt? f t.left x) t.right
else if lt? t.payload x
then mkT t.payload t.left (bbtree-addWith lt? f t.right x)
then mkT t.payload t.left (bbtree-add-with lt? f t.right x)
else mkBr (f t.payload x) t.size t.left t.right
end
......@@ -215,16 +216,16 @@ val bbtree-remove2 btl btr =
| Br l:
case btr of
Lf: btl
| Br r: mkT (bbtree-min btr) btl (bbtree-removeMin btr)
| Br r: mkT (bbtree-min btr) btl (bbtree-remove-min btr)
end
end
val bbtree-removeMin bt =
val bbtree-remove-min bt =
case bt of
Br t:
case t.left of
Lf: t.right
| Br l: mkT t.payload (bbtree-removeMin t.left) t.right
| Br l: mkT t.payload (bbtree-remove-min t.left) t.right
end
end
......@@ -264,25 +265,25 @@ val bbtree-concat3 lt? btl x btr =
end
end
val bbtree-splitLessThan lt? bt x =
val bbtree-split-less-than lt? bt x =
case bt of
Lf: bt
| Br t:
if lt? x t.payload
then bbtree-splitLessThan lt? t.left x
then bbtree-split-less-than lt? t.left x
else if lt? t.payload x
then bbtree-concat3 lt? t.left t.payload (bbtree-splitLessThan lt? t.right x)
then bbtree-concat3 lt? t.left t.payload (bbtree-split-less-than lt? t.right x)
else t.left
end
val bbtree-splitGreaterThan lt? bt x =
val bbtree-split-greater-than lt? bt x =
case bt of
Lf: bt
| Br t:
if lt? t.payload x
then bbtree-splitGreaterThan lt? t.right x
then bbtree-split-greater-than lt? t.right x
else if lt? x t.payload
then bbtree-concat3 lt? (bbtree-splitGreaterThan lt? t.left x) t.payload t.right
then bbtree-concat3 lt? (bbtree-split-greater-than lt? t.left x) t.payload t.right
else t.right
end
......@@ -296,11 +297,11 @@ val bbtree-difference lt? btl btr =
bbtree-concat
(bbtree-difference
lt?
(bbtree-splitLessThan lt? btl r.payload)
(bbtree-split-less-than lt? btl r.payload)
r.left)
(bbtree-difference
lt?
(bbtree-splitGreaterThan lt? btl r.payload)
(bbtree-split-greater-than lt? btl r.payload)
r.right)
end
end
......@@ -316,7 +317,7 @@ val bbtree-concat btl btr =
then mkT r.payload (bbtree-concat btl r.left) r.right
else if r.size * 3 < l.size
then mkT l.payload l.left (bbtree-concat l.right btr)
else mkT (bbtree-min btr) btl (bbtree-removeMin btr)
else mkT (bbtree-min btr) btl (bbtree-remove-min btr)
end
end
......@@ -341,14 +342,14 @@ val bbtree-get lt? bt x =
else t.payload
end
val bbtree-getOrElse lt? bt x y =
val bbtree-get-orelse lt? bt x =
case bt of
Lf: y
Lf: x
| Br t:
if lt? x t.payload
then bbtree-getOrElse lt? t.left x y
then bbtree-get-orelse lt? t.left x
else if lt? t.payload x
then bbtree-getOrElse lt? t.right x y
then bbtree-get-orelse lt? t.right x
else t.payload
end
......@@ -365,27 +366,27 @@ val bbtree-intersection lt? btl btr =
lt?
(bbtree-intersection
lt?
(bbtree-splitLessThan lt? btl r.payload)
(bbtree-split-less-than lt? btl r.payload)
r.left)
r.payload
(bbtree-intersection
lt?
(bbtree-splitGreaterThan lt? btl r.payload)
(bbtree-split-greater-than lt? btl r.payload)
r.right)
else
bbtree-concat
(bbtree-intersection
lt?
(bbtree-splitLessThan lt? btl r.payload)
(bbtree-split-less-than lt? btl r.payload)
r.left)
(bbtree-intersection
lt?
(bbtree-splitGreaterThan lt? btl r.payload)
(bbtree-split-greater-than lt? btl r.payload)
r.right)
end
end
val bbtree-simpleUnion lt? btl btr =
val bbtree-simple-union lt? btl btr =
case btl of
Lf: btr
| Br l:
......@@ -394,19 +395,19 @@ val bbtree-simpleUnion lt? btl btr =
| Br r:
bbtree-concat3
lt?
(bbtree-simpleUnion
(bbtree-simple-union
lt?
l.left
(bbtree-splitLessThan lt? btr l.payload))
(bbtree-split-less-than lt? btr l.payload))
l.payload
(bbtree-simpleUnion
(bbtree-simple-union
lt?
l.right
(bbtree-splitGreaterThan lt? btr l.payload))
(bbtree-split-greater-than lt? btr l.payload))
end
end
val bbtree-union lt? btl btr = bbtree-simpleUnion lt? btl btr
val bbtree-union lt? btl btr = bbtree-simple-union lt? btl btr
val bbtree-fold f s bt =
case bt of
......@@ -426,7 +427,7 @@ val bbtree-pretty f bt =
val intset-lt? a b = a < b
val intset-add s x = bbtree-add intset-lt? s x
val intset-remove s x = bbtree-remove intset-lt? s x
val intset-removeMin s = bbtree-removeMin s
val intset-remove-min s = bbtree-remove-min s
val intset-union a b = bbtree-union intset-lt? a b
val intset-intersection a b = bbtree-intersection intset-lt? a b
val intset-difference a b = bbtree-difference intset-lt? a b
......@@ -445,10 +446,93 @@ val fitree-lt? a b =
then '0'
else a.hi < b.hi
val interval-overlaps? x y = x.lo <= y.hi and y.lo <= x.hi
val interval-contains? x y = x.lo <= y.lo and y.hi <= x.hi
val fitree-search p? it x =
let
val maybe-search-left it acc =
case it of
Lf: acc
| _ :
if x.lo <= (bbtree-max it).hi
then search it acc
else acc
end
val maybe-search-right it acc =
case it of
Lf: acc
| _ :
if x.hi >= (bbtree-min it).lo
then search it acc
else acc
end
val search it acc =
case it of
Lf: acc
| Br t:
maybe-search-left
t.left
(maybe-search-right
t.right
(if p? x t.payload
then fitree-add acc t.payload
else acc))
end
in
search it (fitree-empty {})
end
val fitree-any p? it x =
let
val maybe-search-left it =
case it of
Lf: '0'
| _ :
if x.lo <= (bbtree-max it).hi
then search it
else '0'
end
val maybe-search-right it =
case it of
Lf: '0'
| _ :
if x.hi >= (bbtree-min it).lo
then search it
else '0'
end
val search it =
case it of
Lf: '0'
| Br t:
if p? x t.payload
then '1'
else
maybe-search-left t.left
or maybe-search-right t.right
end
in
search it
end
val fitree-any-overlapping? t x = fitree-any interval-overlaps? t x
val fitree-search-contained t x = fitree-search interval-contains? t x
val fitree-search-overlapping t x = fitree-search interval-overlaps? t x
# TODO:
# Real interval difference supporting interval splitting, cutting and
# full interval containing
val fitree-interval-difference a b =
let
val remove-contained it x = fitree-difference it (fitree-search-contained it x)
in
fitree-fold remove-contained a b
end
val fitree-mk l h = {lo=l, hi=h}
val fitree-add s x = bbtree-add fitree-lt? s x
val fitree-remove s x = bbtree-remove fitree-lt? s x
val fitree-removeMin s = bbtree-removeMin s
#val fitree-remove s x = bbtree-remove fitree-lt? s x
val fitree-remove-min s = bbtree-remove-min s
val fitree-union a b = bbtree-union fitree-lt? a b
val fitree-intersection a b = bbtree-intersection fitree-lt? a b
val fitree-difference a b = bbtree-difference fitree-lt? a b
......
specifications/rreil/rreil-pretty.ml
View file @ 891c3d2d
# vim:filetype=sml:ts=3:sw=3:expandtab
# The following functions need to be defined elsewhere:
# - show/arch
# - arch-show-id
export = prettyrreil
export = rreil-pretty
val prettyrreil ss = showrreil/stmts ss
val rreil-pretty ss = rreil-show-stmts ss
val showrreil/stmts ss =
val rreil-show-stmts ss =
case ss of
SEM_NIL: ""
| SEM_CONS x: showrreil/stmt x.hd +++ "\n" +++ showrreil/stmts x.tl
| SEM_CONS x: rreil-show-stmt x.hd +++ "\n" +++ rreil-show-stmts x.tl
end
val showrreil/stmt s =
val rreil-show-stmt s =
case s of
SEM_ASSIGN x: showrreil/var x.lhs +++ " = " +++ showrreil/op x.rhs
| SEM_LOAD x: showrreil/var x.lhs +++ " = " showrreil/ptrderef x.size x.address
| SEM_STORE x: "*" +++ showrreil/address x.address +++ " = " +++ showrreil/op x.rhs
| SEM_LABEL x: showrreil/label x.id
| SEM_IF_GOTO_LABEL x: "if (" +++ showrreil/linear x.cond +++ ") goto label " +++ showrreil/label x.label
| SEM_IF_GOTO x: "if (" +++ showrreil/linear x.cond +++ ") goto " +++ showrreil/address x.target
| SEM_CALL x: "if (" +++ showrreil/linear x.cond +++ ") call " +++ showrreil/address x.target
| SEM_RETURN x: "if (" +++ showrreil/linear x.cond +++ ") return " +++ showrreil/address x.target
SEM_ASSIGN x: rreil-show-var x.lhs +++ " = " +++ rreil-show-op x.rhs
| SEM_LOAD x: rreil-show-var x.lhs +++ " = " rreil-show-ptrderef x.size x.address
| SEM_STORE x: "*" +++ rreil-show-address x.address +++ " = " +++ rreil-show-op x.rhs
| SEM_LABEL x: rreil-show-label x.id
| SEM_IF_GOTO_LABEL x: "if (" +++ rreil-show-linear x.cond +++ ") goto label " +++ rreil-show-label x.label
| SEM_IF_GOTO x: "if (" +++ rreil-show-linear x.cond +++ ") goto " +++ rreil-show-linear x.target
| SEM_CALL x: "if (" +++ rreil-show-linear x.cond +++ ") call " +++ rreil-show-address x.target
| SEM_RETURN x: "if (" +++ rreil-show-linear x.cond +++ ") return " +++ rreil-show-address x.target
end
val showrreil/label l = "l" +++ showint l +++ ":"
val rreil-show-label l = "l" +++ showint l +++ ":"
val showrreil/op op =
val rreil-show-op op =
case op of
SEM_LIN x: showrreil/arity1 x
| SEM_BSWAP x: "bswap" +++ showrreil/arity1 x
| SEM_MUL x: "mul" +++ showrreil/arity2 x
| SEM_DIV x: "div" +++ showrreil/arity2 x
| SEM_DIVS x: "divs" +++ showrreil/arity2 x
| SEM_MOD x: "mod" +++ showrreil/arity2 x
| SEM_SHL x: "shl" +++ showrreil/arity2 x
| SEM_SHR x: "shr" +++ showrreil/arity2 x
| SEM_SHRS x: "shrs" +++ showrreil/arity2 x
| SEM_AND x: "and" +++ showrreil/arity2 x
| SEM_OR x: "or" +++ showrreil/arity2 x
| SEM_XOR x: "xor" +++ showrreil/arity2 x
| SEM_SX x: "sx[" +++ showint x.fromsize +++ "." +++ showint x.size +++ "](" +++ showrreil/linear x.opnd1 +++ ")"
| SEM_ZX x: "zx[" +++ showint x.fromsize +++ "." +++ showint x.size +++ "](" +++ showrreil/linear x.opnd1 +++ ")"
| SEM_CMPEQ x: "==" +++ showrreil/cmp x
| SEM_CMPNEQ x: "/=" +++ showrreil/cmp x
| SEM_CMPLES x: "<=s" +++ showrreil/cmp x
| SEM_CMPLEU x: "<=u" +++ showrreil/cmp x
| SEM_CMPLTS x: "<s" +++ showrreil/cmp x
| SEM_CMPLTU x: "<u" +++ showrreil/cmp x
SEM_LIN x: rreil-show-arity1 x
| SEM_BSWAP x: "bswap" +++ rreil-show-arity1 x
| SEM_MUL x: "mul" +++ rreil-show-arity2 x
| SEM_DIV x: "div" +++ rreil-show-arity2 x
| SEM_DIVS x: "divs" +++ rreil-show-arity2 x
| SEM_MOD x: "mod" +++ rreil-show-arity2 x
| SEM_SHL x: "shl" +++ rreil-show-arity2 x
| SEM_SHR x: "shr" +++ rreil-show-arity2 x
| SEM_SHRS x: "shrs" +++ rreil-show-arity2 x
| SEM_AND x: "and" +++ rreil-show-arity2 x
| SEM_OR x: "or" +++ rreil-show-arity2 x
| SEM_XOR x: "xor" +++ rreil-show-arity2 x
| SEM_SX x: "sx[" +++ showint x.fromsize +++ "." +++ showint x.size +++ "](" +++ rreil-show-linear x.opnd1 +++ ")"
| SEM_ZX x: "zx[" +++ showint x.fromsize +++ "." +++ showint x.size +++ "](" +++ rreil-show-linear x.opnd1 +++ ")"
| SEM_CMPEQ x: "==" +++ rreil-show-cmp x
| SEM_CMPNEQ x: "/=" +++ rreil-show-cmp x
| SEM_CMPLES x: "<=s" +++ rreil-show-cmp x
| SEM_CMPLEU x: "<=u" +++ rreil-show-cmp x
| SEM_CMPLTS x: "<s" +++ rreil-show-cmp x
| SEM_CMPLTU x: "<u" +++ rreil-show-cmp x
| SEM_ARB x: "arbitrary[" +++ showint x +++ "]"
end
val showrreil/arity1 x = "[" +++ showint x.size +++ "](" +++ showrreil/linear x.opnd1 +++ ")"
val showrreil/arity2 x = "[" +++ showint x.size +++ "](" +++ showrreil/linear x.opnd1 +++ "," +++ showrreil/linear x.opnd2 +++ ")"
val showrreil/cmp x = "[" +++ showint x.size +++ ".1](" +++ showrreil/linear x.opnd1 +++ "," +++ showrreil/linear x.opnd2 +++ ")"
val showrreil/ptrderef sz addr = "*[" +++ showint addr.size +++ "." +++ showint sz +++ "](" +++ showrreil/linear addr.address +++ ")"
val showrreil/address addr = "[" +++ showint addr.size +++ "](" +++ showrreil/linear addr.address +++ ")"
val showrreil/var x =
val rreil-show-arity1 x = "[" +++ showint x.size +++ "](" +++ rreil-show-linear x.opnd1 +++ ")"
val rreil-show-arity2 x = "[" +++ showint x.size +++ "](" +++ rreil-show-linear x.opnd1 +++ "," +++ rreil-show-linear x.opnd2 +++ ")"
val rreil-show-cmp x = "[" +++ showint x.size +++ ".1](" +++ rreil-show-linear x.opnd1 +++ "," +++ rreil-show-linear x.opnd2 +++ ")"
val rreil-show-ptrderef sz addr = "*[" +++ showint addr.size +++ "." +++ showint sz +++ "](" +++ rreil-show-linear addr.address +++ ")"
val rreil-show-address addr = "[" +++ showint addr.size +++ "](" +++ rreil-show-linear addr.address +++ ")"
val rreil-show-var x =
case x.offset of
0: showrreil/id x.id
| o: showrreil/id x.id +++ "/" +++ showint o
0: rreil-show-id x.id
| o: rreil-show-id x.id +++ "/" +++ showint o
end
val showrreil/linear lin =
val rreil-show-linear lin =
case lin of
SEM_LIN_VAR x: showrreil/var x
SEM_LIN_VAR x: rreil-show-var x
| SEM_LIN_IMM x: showint x.imm
| SEM_LIN_ADD x: showrreil/linear x.opnd1 +++ "+" +++ showrreil/linear x.opnd2
| SEM_LIN_SUB x: showrreil/linear x.opnd1 +++ "-" +++ showrreil/linear x.opnd2
| SEM_LIN_ADD x: rreil-show-linear x.opnd1 +++ "+" +++ rreil-show-linear x.opnd2
| SEM_LIN_SUB x: rreil-show-linear x.opnd1 +++ "-" +++ rreil-show-linear x.opnd2
| SEM_LIN_SCALE x:
case x.imm of
0: ""
| 1: showrreil/linear x.opnd
| s: showint s +++ "*" +++ showrreil/linear x.opnd
| 1: rreil-show-linear x.opnd
| s: showint s +++ "*" +++ rreil-show-linear x.opnd
end
end
val showrreil/id id =
val rreil-show-id id =
case id of
ARCH_R x: show/arch x
ARCH_R x: arch-show-id x
| VIRT_EQ: "EQ"
| VIRT_NEQ: "NEQ"
| VIRT_LES: "LES"
......
specifications/rreil/rreil.ml
View file @ 891c3d2d
......@@ -53,7 +53,7 @@ type sem_stmt =
| SEM_STORE of {address: sem_address, rhs: sem_op}
| SEM_LABEL of {id: int}
| SEM_IF_GOTO_LABEL of {cond:sem_linear, label: int}
| SEM_IF_GOTO of {cond: sem_linear, size:int, target: sem_address}
| SEM_IF_GOTO of {cond: sem_linear, size:int, target: sem_linear}
| SEM_CALL of {cond: sem_linear, size:int, target: sem_address}
| SEM_RETURN of {cond: sem_linear, size:int, target: sem_address}
......@@ -90,7 +90,7 @@ val rreil-sizeOf op =
| SEM_ARB x: x.size
end
val revSeq stmts =
val rreil-stmts-rev stmts =
let
val lp stmt acc =
case stmt of
......@@ -101,18 +101,6 @@ val revSeq stmts =
lp stmts SEM_NIL
end
val resultSize op =
case op of
SEM_CMPLES x : 1
| SEM_MUL x : x.size
end
val operandSize op =
case op of
SEM_CMPLES x : x.size
| x : resultSize op
end
val var//0 x = {id=x,offset=0}
val var x = SEM_LIN_VAR x
......@@ -127,7 +115,7 @@ val mklabel = do
l <- query $lab;
l' <- return (l + 1);
update @{lab=l'};
return (l)
return l
end
val /ASSIGN a b = SEM_ASSIGN{lhs=a,rhs=b}
......@@ -137,6 +125,7 @@ val /ADD a b = SEM_LIN_ADD{opnd1=a,opnd2=b}
val /SUB a b = SEM_LIN_SUB{opnd1=a,opnd2=b}
val /LABEL l = SEM_LABEL{id=l}
val /IFGOTOLABEL c l = SEM_IF_GOTO_LABEL{cond=c,label=l}
val /IFGOTO c sz t = SEM_IF_GOTO{cond=c,size=sz,target=t}
val /GOTOLABEL l = SEM_IF_GOTO_LABEL{cond=SEM_LIN_IMM{imm=1},label=l}
val push insn = do
......@@ -172,6 +161,7 @@ val cmpltu sz f a b = push (/ASSIGN f (SEM_CMPLTU{size=sz,opnd1=a,opnd2=b}))
val label l = push (/LABEL l)
val ifgotolabel c l = push (/IFGOTOLABEL c l)
val gotolabel l = push (/GOTOLABEL l)
val ifgoto c sz addr = push (/IFGOTO c sz addr)
val const i = return (SEM_LIN_IMM{imm=i})
......
specifications/x86/x86-pretty.ml
View file @ 891c3d2d
# vim:ts=3:sw=3:expandtab
# vim:filetype=sml:ts=3:sw=3:expandtab
export = pretty
......
specifications/x86/x86-rreil-registermapping.ml
View file @ 891c3d2d
val semanticRegisterOf r =
val semantic-register-of r =
case r of
RAX: {id=ARCH_R 0,offset=0,size=64}
| RBX: {id=ARCH_R 1,offset=0,size=64}
| RBP: {id=ARCH_R 2,offset=0,size=64}
| RSP: {id=ARCH_R 3,offset=0,size=