Commit d9bd71ed authored by Julian Kranz's avatar Julian Kranz
Browse files

Use expressions in state

parent 58865a54
......@@ -9,56 +9,60 @@ val substitute-stmt-with-state-definitions state stmt = case stmt of
| SEM_LOAD s : return (SEM_LOAD {size=s.size, lhs=s.lhs, address= df-subst-address state s.address})
| SEM_STORE s : return (SEM_STORE {size=s.size, address= df-subst-address state s.address, rhs=df-subst-linear state s.size s.rhs})
| SEM_ITE s : do
newCond <- df-subst-cond state s.cond;
case newCond of
NOTHING_SEXPR : do
#println "subst-cond-ite-nothing";
return (SEM_ITE {cond= s.cond, then_branch= s.then_branch, else_branch= s.else_branch})
end
| JUST_SEXPR se : do
#println "subst-cond-ite-insert";
return (SEM_ITE {cond= se, then_branch= s.then_branch, else_branch= s.else_branch})
end
end
end
newCond <- df-subst-cond state s.cond;
case newCond of
NOTHING_EXPR : do
#println "subst-cond-ite-nothing";
return (SEM_ITE {cond= s.cond, then_branch= s.then_branch, else_branch= s.else_branch})
end
| JUST_EXPR e : do
#println "subst-cond-ite-insert";
case e of
SEM_SEXPR se: return (SEM_ITE {cond= se, then_branch= s.then_branch, else_branch= s.else_branch})
end
end
end
end
| SEM_WHILE s : return stmt
| SEM_CBRANCH s : do
newCond <- df-subst-cond state s.cond;
case newCond of
NOTHING_SEXPR : do
#println "subst-cond-cbranch-nothing";
return (SEM_CBRANCH {cond= s.cond, target-true= df-subst-address state s.target-true, target-false= df-subst-address state s.target-false})
end
| JUST_SEXPR se : do
#println "subst-cond-cbranch-insert";
return (SEM_CBRANCH {cond= se, target-true= df-subst-address state s.target-true, target-false= df-subst-address state s.target-false})
end
end
end
newCond <- df-subst-cond state s.cond;
case newCond of
NOTHING_EXPR : do
#println "subst-cond-cbranch-nothing";
return (SEM_CBRANCH {cond= s.cond, target-true= df-subst-address state s.target-true, target-false= df-subst-address state s.target-false})
end
| JUST_EXPR e : do
#println "subst-cond-cbranch-insert";
case e of
SEM_SEXPR se: return (SEM_CBRANCH {cond= se, target-true= df-subst-address state s.target-true, target-false= df-subst-address state s.target-false})
end
end
end
end
| SEM_BRANCH s : return (SEM_BRANCH {hint=s.hint, target= df-subst-address state s.target})
| SEM_FLOP s : return (SEM_FLOP {op=s.op, flags= s.flags, lhs=s.lhs, rhs= df-subst-varl-list state s.rhs})
| SEM_PRIM s : return (SEM_PRIM {op=s.op, lhs = s.lhs, rhs= df-subst-varl-list state s.rhs})
| SEM_THROW e : return stmt
end
end
val df-subst-cond state c = case c of
SEM_SEXPR_LIN linear : return (df-subst-linear-to-cond state linear)
| SEM_SEXPR_CMP s : return (JUST_SEXPR (SEM_SEXPR_CMP {size=s.size, cmp=df-subst-expr-cmp state s.size s.cmp}))
| SEM_SEXPR_ARB : return (JUST_SEXPR c)
end
| SEM_SEXPR_CMP s : return (JUST_EXPR (SEM_SEXPR (SEM_SEXPR_CMP {size=s.size, cmp=df-subst-expr-cmp state s.size s.cmp})))
| SEM_SEXPR_ARB : return (JUST_EXPR (SEM_SEXPR c))
end
val df-subst-linear-to-cond state linear =
case linear of
case linear of
SEM_LIN_VAR var : df-substmap-lookup-var-to-cond state var.offset var.id
| SEM_LIN_IMM s : JUST_SEXPR (SEM_SEXPR_LIN linear)
| SEM_LIN_ADD s : JUST_SEXPR (SEM_SEXPR_LIN (df-simplify-lin-add (df-subst-linear state 1 s.opnd1) (df-subst-linear state 1 s.opnd2)))
| SEM_LIN_SUB s : JUST_SEXPR (SEM_SEXPR_LIN (SEM_LIN_SUB (df-subst-arity2 state 1 s)))
| SEM_LIN_SCALE s : JUST_SEXPR (SEM_SEXPR_LIN (SEM_LIN_SCALE {const=s.const, opnd=df-subst-linear state 1 s.opnd}))
end
| SEM_LIN_IMM s : JUST_EXPR (SEM_SEXPR (SEM_SEXPR_LIN linear))
| SEM_LIN_ADD s : JUST_EXPR (SEM_SEXPR (SEM_SEXPR_LIN (df-simplify-lin-add (df-subst-linear state 1 s.opnd1) (df-subst-linear state 1 s.opnd2))))
| SEM_LIN_SUB s : JUST_EXPR (SEM_SEXPR (SEM_SEXPR_LIN (SEM_LIN_SUB (df-subst-arity2 state 1 s))))
| SEM_LIN_SCALE s : JUST_EXPR (SEM_SEXPR (SEM_SEXPR_LIN (SEM_LIN_SCALE {const=s.const, opnd=df-subst-linear state 1 s.opnd})))
end
val df-subst-expr state size expr = case expr of
SEM_SEXPR sexpr : SEM_SEXPR (df-subst-sexpr state size sexpr)
SEM_SEXPR sexpr : df-subst-sexpr-to-expr state size sexpr
| SEM_MUL s : SEM_MUL (df-subst-arity2 state size s)
| SEM_DIV s : SEM_DIV (df-subst-arity2 state size s)
| SEM_DIVS s : SEM_DIVS (df-subst-arity2 state size s)
......@@ -76,11 +80,11 @@ val df-subst-expr state size expr = case expr of
val df-subst-sexpr state size sexpr = case sexpr of
SEM_SEXPR_LIN linear : df-subst-linear-to-sexpr state size linear
| SEM_SEXPR_CMP s : SEM_SEXPR_CMP {size=s.size, cmp=df-subst-expr-cmp state s.size s.cmp}
| SEM_SEXPR_ARB : sexpr
end
val df-subst-sexpr-to-expr state size sexpr = case sexpr of
SEM_SEXPR_LIN linear : df-subst-linear-to-expr state size linear
| SEM_SEXPR_CMP s : SEM_SEXPR (SEM_SEXPR_CMP {size=s.size, cmp=df-subst-expr-cmp state s.size s.cmp})
| SEM_SEXPR_ARB : SEM_SEXPR sexpr
end
val df-subst-address state s = {size=s.size, address= df-subst-linear state s.size s.address}
......@@ -93,19 +97,19 @@ val df-subst-expr-cmp state size cmp = case cmp of
| SEM_CMPLEU s : SEM_CMPLEU (df-subst-arity2 state size s)
| SEM_CMPLTS s : SEM_CMPLTS (df-subst-arity2 state size s)
| SEM_CMPLTU s : SEM_CMPLTU (df-subst-arity2 state size s)
end
end
val df-subst-arity2 state size s = {opnd1= df-subst-linear state size s.opnd1, opnd2= df-subst-linear state size s.opnd2 }
val df-subst-linear-to-sexpr state size linear = case linear of
SEM_LIN_VAR var : df-subst-var-to-sexpr state size var
| SEM_LIN_IMM s : SEM_SEXPR_LIN linear
| SEM_LIN_ADD s : SEM_SEXPR_LIN (df-simplify-lin-add (df-subst-linear state size s.opnd1) (df-subst-linear state size s.opnd2))
| SEM_LIN_SUB s : SEM_SEXPR_LIN (SEM_LIN_SUB (df-subst-arity2 state size s))
| SEM_LIN_SCALE s : SEM_SEXPR_LIN (SEM_LIN_SCALE {const=s.const, opnd=df-subst-linear state size s.opnd})
end
val df-subst-linear-to-expr state size linear = case linear of
SEM_LIN_VAR var : df-subst-var-to-expr state size var
| SEM_LIN_IMM s : SEM_SEXPR (SEM_SEXPR_LIN linear)
| SEM_LIN_ADD s : SEM_SEXPR (SEM_SEXPR_LIN (df-simplify-lin-add (df-subst-linear state size s.opnd1) (df-subst-linear state size s.opnd2)))
| SEM_LIN_SUB s : SEM_SEXPR (SEM_SEXPR_LIN (SEM_LIN_SUB (df-subst-arity2 state size s)))
| SEM_LIN_SCALE s : SEM_SEXPR (SEM_SEXPR_LIN (SEM_LIN_SCALE {const=s.const, opnd=df-subst-linear state size s.opnd}))
end
val df-subst-linear state size linear = case linear of
SEM_LIN_VAR var : df-subst-var-to-lin state size var
......@@ -113,7 +117,7 @@ val df-subst-linear state size linear = case linear of
| SEM_LIN_ADD s : df-simplify-lin-add (df-subst-linear state size s.opnd1) (df-subst-linear state size s.opnd2)
| SEM_LIN_SUB s : SEM_LIN_SUB (df-subst-arity2 state size s)
| SEM_LIN_SCALE s : SEM_LIN_SCALE {const=s.const, opnd=df-subst-linear state size s.opnd}
end
end
val df-subst-varl-list state varlist = case varlist of
......@@ -125,10 +129,10 @@ val df-subst-varl-list state varlist = case varlist of
val df-subst-varl-to-varl state varl = case df-substmap-var-to-lin state varl.offset varl.size varl.id of
SEM_LIN_VAR v : {id=v.id, offset=v.offset, size=varl.size}
| _ : varl
end
end
val df-subst-var-to-sexpr state size var = df-substmap-var-to-sexpr state var.offset size var.id
val df-subst-var-to-expr state size var = df-substmap-var-to-expr state var.offset size var.id
val df-subst-var-to-lin state size var = df-substmap-var-to-lin state var.offset size var.id
......@@ -136,26 +140,26 @@ val df-simplify-linear lin = case lin of
SEM_LIN_VAR v : lin
| SEM_LIN_IMM v : lin
| SEM_LIN_ADD v :
let val o1 = df-simplify-linear v.opnd1
val o2 = df-simplify-linear v.opnd2
in case o1 of
SEM_LIN_IMM v1 :
case o2 of
SEM_LIN_IMM v2 : SEM_LIN_IMM {const= v1.const + v2.const}
| _ : SEM_LIN_ADD {opnd1= o1, opnd2=o2}
end
| _ : SEM_LIN_ADD {opnd1= o1, opnd2=o2}
end
end
end
let val o1 = df-simplify-linear v.opnd1
val o2 = df-simplify-linear v.opnd2
in case o1 of
SEM_LIN_IMM v1 :
case o2 of
SEM_LIN_IMM v2 : SEM_LIN_IMM {const= v1.const + v2.const}
| _ : SEM_LIN_ADD {opnd1= o1, opnd2=o2}
end
| _ : SEM_LIN_ADD {opnd1= o1, opnd2=o2}
end
end
end
val df-simplify-lin-add o1 o2 =
case o1 of
SEM_LIN_IMM v1 :
case o2 of
SEM_LIN_IMM v2 : SEM_LIN_IMM {const= v1.const + v2.const}
| _ : SEM_LIN_ADD {opnd1= o1, opnd2=o2}
end
| _ : SEM_LIN_ADD {opnd1= o1, opnd2=o2}
end
case o1 of
SEM_LIN_IMM v1 :
case o2 of
SEM_LIN_IMM v2 : SEM_LIN_IMM {const= v1.const + v2.const}
| _ : SEM_LIN_ADD {opnd1= o1, opnd2=o2}
end
| _ : SEM_LIN_ADD {opnd1= o1, opnd2=o2}
end
......@@ -19,7 +19,7 @@ val df-substmap-initial = SUBSTMAP_EMPTY
type df-maybe-linear = NOTHING_LINEAR | JUST_LINEAR of sem_linear
type df-maybe-sexpr = NOTHING_SEXPR | JUST_SEXPR of sem_sexpr
type df-maybe-expr = NOTHING_EXPR | JUST_EXPR of sem_expr
# lookup binding for location
......@@ -36,14 +36,14 @@ val df-substmap-var-to-lin state offset size var = case df-substmap-lookup-var-t
| JUST_LINEAR linear : linear
end
val df-substmap-var-to-sexpr state offset size var = case df-substmap-lookup-var-to-sexpr state offset size var of
NOTHING_SEXPR : SEM_SEXPR_LIN (SEM_LIN_VAR {id=var, offset=offset})
| JUST_SEXPR linear : linear
val df-substmap-var-to-expr state offset size var = case df-substmap-lookup-var-to-expr state offset size var of
NOTHING_EXPR : SEM_SEXPR (SEM_SEXPR_LIN (SEM_LIN_VAR {id=var, offset=offset}))
| JUST_EXPR e : e
end
val df-substmap-lookup-var-to-cond state offset var = df-substmap-lookup-var-to-sexpr state offset 1 var
val df-substmap-lookup-var-to-cond state offset var = df-substmap-lookup-var-to-expr state offset 1 var
# lookup binding for location, recursive worker function
......@@ -57,19 +57,19 @@ val df-substmap-lookup-var-to-cond state offset var = df-substmap-lookup-var-to-
# or nothing (if binding is nonexisting or overwritten or if rhs
# of binding refers to variables that are invalidated since then)
#
val df-substmap-lookup-var-to-sexpr state offset size var =
val df-substmap-lookup-var-to-expr state offset size var =
case state of
SUBSTMAP_LINEAR s :
if id-eq? var s.id
then (if size+offset <= s.offset or s.size+s.offset <= offset
then df-substmap-lookup-var-to-sexpr s.cont offset size var
then df-substmap-lookup-var-to-expr s.cont offset size var
else (if size+offset <= s.offset+s.size
then (if offset===s.offset
then JUST_SEXPR s.rhs
else NOTHING_SEXPR)
else NOTHING_SEXPR))
else df-substmap-lookup-var-to-sexpr s.cont offset size var
| SUBSTMAP_EMPTY : NOTHING_SEXPR
then JUST_EXPR s.rhs
else NOTHING_EXPR)
else NOTHING_EXPR))
else df-substmap-lookup-var-to-expr s.cont offset size var
| SUBSTMAP_EMPTY : NOTHING_EXPR
end
# lookup binding for location, recursive worker function
......@@ -92,8 +92,11 @@ val df-substmap-lookup-var-to-linear state offset size var =
else (if size+offset <= s.offset+s.size
then (if offset===s.offset
then case s.rhs of
SEM_SEXPR_LIN l : JUST_LINEAR l
| _ : NOTHING_LINEAR
SEM_SEXPR sex: case sex of
SEM_SEXPR_LIN l : JUST_LINEAR l
| _ : NOTHING_LINEAR
| _: NOTHING_LINEAR
end
end
else NOTHING_LINEAR)
else NOTHING_LINEAR))
......@@ -101,10 +104,14 @@ val df-substmap-lookup-var-to-linear state offset size var =
| SUBSTMAP_EMPTY : NOTHING_LINEAR
end
val df-sexpr-uses-location o s v rs lin = case lin of
SEM_SEXPR_LIN l : df-lin-uses-location o s v rs l
| SEM_SEXPR_CMP e : df-cmp-uses-location o e.size v rs e.cmp
| SEM_SEXPR_ARB : '0'
val df-expr-uses-location o s v rs lin =
case lin of
SEM_SEXPR se:
case se of
SEM_SEXPR_LIN l : df-lin-uses-location o s v rs l
| SEM_SEXPR_CMP e : df-cmp-uses-location o e.size v rs e.cmp
| SEM_SEXPR_ARB : '0'
end
end
val df-cmp-uses-location o s v rs lin = case lin of
......@@ -132,10 +139,14 @@ val df-show-substmap sm = case sm of
end
val df-sexpr-uses-id v lin = case lin of
SEM_SEXPR_LIN l : df-lin-uses-id v l
| SEM_SEXPR_CMP e : df-cmp-uses-id v e.cmp
| SEM_SEXPR_ARB : '0'
val df-expr-uses-id v lin =
case lin of
SEM_SEXPR se:
case se of
SEM_SEXPR_LIN l : df-lin-uses-id v l
| SEM_SEXPR_CMP e : df-cmp-uses-id v e.cmp
| SEM_SEXPR_ARB : '0'
end
end
val df-cmp-uses-id v lin = case lin of
......@@ -184,11 +195,11 @@ val df-substmap-remove-linear state offset size var-id =
# Returns:
# subst map with the updated/new added linear
#
val df-substmap-update-linear state offset size var-id sexpr =
val df-substmap-update-linear state offset size var-id expr =
case state of
SUBSTMAP_EMPTY : SUBSTMAP_LINEAR {offset=offset, size=size, id=var-id, rhs=sexpr, cont=SUBSTMAP_EMPTY, inverted=0}
SUBSTMAP_EMPTY : SUBSTMAP_LINEAR {offset=offset, size=size, id=var-id, rhs=expr, cont=SUBSTMAP_EMPTY, inverted=0}
| SUBSTMAP_LINEAR l :
if l.offset === offset and l.size === size and (id-eq? l.id var-id)
then df-substmap-update-linear l.cont offset size var-id sexpr
else SUBSTMAP_LINEAR {offset=l.offset, size=l.size, id=l.id, rhs=l.rhs, cont=(df-substmap-update-linear l.cont offset size var-id sexpr)}
then df-substmap-update-linear l.cont offset size var-id expr
else SUBSTMAP_LINEAR {offset=l.offset, size=l.size, id=l.id, rhs=l.rhs, cont=(df-substmap-update-linear l.cont offset size var-id expr)}
end
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment