Commit 199d41a5 authored by Julian Kranz's avatar Julian Kranz

Merge branch 'experimental'

parents 38e3d848 2f1f5587
......@@ -99,7 +99,7 @@ libs/x86/src/libx86_la-x86_features.lo
libs/x86/src/libx86_la-x86_features.o
tools/.dirstamp
tools/decoder_cli-decoder-cli.o
tools/liveness_sweep-liveness-sweep.o
tools/optimization_sweep-optimization-sweep.o
tools/semantics_cif_cli-semantics-cif-cli.o
tools/semantics_cli-semantics-cli.o
tools/semantics_cli_dynamic-semantics-cli-dynamic.o
......@@ -132,8 +132,8 @@ tools/x86-test-stats-runner/src/x86_test_stats_runner-main.o
/libs/x86/x86_features.o
/tools/decoder-cli
/tools/decoder-cli.o
/tools/liveness-sweep
/tools/liveness-sweep.o
/tools/optimization-sweep
/tools/optimization-sweep.o
/tools/semantics-cif-cli
/tools/semantics-cif-cli.o
/tools/semantics-cli
......
......@@ -179,6 +179,7 @@ GDSL_ASM = \
GDSL_X86 = \
$(srcdir)/specifications/x86/x86.ml \
$(srcdir)/specifications/x86/x86-equals.ml \
$(srcdir)/specifications/x86/x86-traverse.ml \
$(srcdir)/specifications/x86/x86-pretty.ml \
$(srcdir)/specifications/x86/x86-asm.ml \
......@@ -239,7 +240,7 @@ GDSL_RREIL = \
$(srcdir)/specifications/rreil/rreil-translator.ml \
$(srcdir)/specifications/rreil/forward-subst/inline.ml \
$(srcdir)/specifications/rreil/forward-subst/substitute.ml \
$(srcdir)/specifications/rreil/forward-subst/substmap.ml \
$(srcdir)/specifications/rreil/forward-subst/substmap.ml \
$(srcdir)/specifications/rreil/forward-subst/simplify-expressions.ml
if X86_RREIL
......
......@@ -21,7 +21,7 @@ GDSL_BASIS_HL=specifications/basis/prelude.ml specifications/basis/bbtree.ml spe
GDSL_RREIL_HL=specifications/rreil/rreil.ml specifications/rreil/rreil-examples.ml specifications/rreil/rreil-cif.ml specifications/rreil/rreil-pretty.ml specifications/rreil/fmap.ml specifications/rreil/rreil-opt.ml specifications/rreil/rreil-translator.ml
GDSL_OPT_HL=specifications/rreil/rreil-liveness.ml specifications/rreil/rreil-forward-subst.ml specifications/rreil/forward-subst/inline.ml specifications/rreil/rreil-cleanup.ml specifications/rreil/forward-subst/substitute.ml specifications/rreil/forward-subst/substmap.ml specifications/rreil/forward-subst/simplify-expressions.ml
GDSL_X86_HL=specifications/x86/x86.ml specifications/x86/x86-traverse.ml specifications/x86/x86-pretty.ml specifications/x86/x86-asm.ml specifications/x86/x86-semantics-mapping.ml specifications/x86/x86-semantics-mapping-pretty.ml
GDSL_X86_HL=specifications/x86/x86.ml specifications/x86/x86-equals.ml specifications/x86/x86-traverse.ml specifications/x86/x86-pretty.ml specifications/x86/x86-asm.ml specifications/x86/x86-semantics-mapping.ml specifications/x86/x86-semantics-mapping-pretty.ml
GDSL_X86_TRANS_HL=specifications/x86/x86-rreil-translator.ml specifications/x86/x86-rreil-translator-a-l.ml specifications/x86/x86-rreil-translator-m-z.ml
GDSL_X86_OPT_HL=specifications/x86/x86-liveness.ml
GDSL_X86_TEST_HL=specifications/x86-tester/x86-pretty-simple.ml
......
......@@ -935,6 +935,7 @@ structure C1 = struct
and emitPrim s (GETSTATEprim, [],_) = str "s->mon_state"
| emitPrim s (SETSTATEprim, [e],_) = seq [str "s->mon_state = ", emitExp s e]
| emitPrim s (SEEKprim, [e],_) = seq [str "gdsl_seek(s, (size_t) (", emitExp s e, str "))"]
| emitPrim s (SEEKFprim, [e],_) = seq [str "gdsl_seekf(s, (size_t) (", emitExp s e, str "))"]
| emitPrim s (DIVprim, [e1, e2],_) = seq [str "(", emitExp s e1, str ")/(", emitExp s e2, str ")"]
| emitPrim s (IPGETprim, [],_) = str "gdsl_get_ip(s)"
| emitPrim s (CONSUME8prim, [],_) = (addConsume s 8; str "consume(s, 1)")
......@@ -1334,6 +1335,7 @@ structure C1 = struct
C1Templates.mkHook ("set_code", str (prefix ^ "set_code")),
C1Templates.mkHook ("get_ip", str (prefix ^ "get_ip")),
C1Templates.mkHook ("seek", str (prefix ^ "seek")),
C1Templates.mkHook ("seekf", str (prefix ^ "seekf")),
(*C1Templates.mkHook ("rseek", str (prefix ^ "rseek")),*)
C1Templates.mkHook ("err_tgt", str (prefix ^ "err_tgt")),
C1Templates.mkHook ("get_error_message", str (prefix ^ "get_error_message")),
......@@ -1352,6 +1354,7 @@ structure C1 = struct
C1Templates.mkHook ("set_code", str (prefix ^ "set_code")),
C1Templates.mkHook ("get_ip", str (prefix ^ "get_ip")),
C1Templates.mkHook ("seek", str (prefix ^ "seek")),
C1Templates.mkHook ("seekf", str (prefix ^ "seekf")),
(*C1Templates.mkHook ("rseek", str (prefix ^ "rseek")),*)
C1Templates.mkHook ("err_tgt", str (prefix ^ "err_tgt")),
C1Templates.mkHook ("get_error_message", str (prefix ^ "get_error_message")),
......
......@@ -346,6 +346,13 @@ int_t
return 0;
}
void
@seekf@
(state_t s, size_t i) {
size_t start_offset = i - s->ip_base;
s->ip = s->ip_start + start_offset;
}
string_t
@merge_rope@
(state_t s, obj_t rope) {
......
......@@ -50,6 +50,7 @@ end = struct
val get_ip = get "get-ip"
(* val rseek = get "rseek"*)
val seek = get "seek"
val seekf = get "seekf"
val index = get "index"
val puts = get "puts"
val return = get "return"
......@@ -304,6 +305,16 @@ end = struct
(seek, [x], body)
end
val seekf =
let
val x = fresh "x"
val s = fresh "s"
val primseekf = get "%seekf"
val body = FN (s, PRI (primseekf, [s,x]))
in
(seekf, [x], body)
end
(* val index s = %index(s) *)
val index =
let
......@@ -414,6 +425,7 @@ end = struct
raisee,
get_ip,
seek,
seekf,
index,
puts,
add,
......
......@@ -2512,6 +2512,7 @@ structure DeadVariables = struct
and hasSidePrim SETSTATEprim = true
| hasSidePrim SEEKprim = true
| hasSidePrim SEEKFprim = true
| hasSidePrim CONSUME8prim = true
| hasSidePrim CONSUME16prim = true
| hasSidePrim CONSUME32prim = true
......
......@@ -61,6 +61,7 @@ structure Imp = struct
| SETSTATEprim
| IPGETprim
| SEEKprim
| SEEKFprim
(*| RSEEKprim*)
| DIVprim
| CONSUME8prim
......@@ -100,6 +101,7 @@ structure Imp = struct
| prim_info SETSTATEprim = { name = "__set_state", prio = 0 }
| prim_info IPGETprim = { name = "get-ip", prio = 0 }
| prim_info SEEKprim = { name = "seek", prio = 0 }
| prim_info SEEKFprim = { name = "seekf", prio = 0 }
(*| prim_info RSEEKprim = { name = "rseek", prio = 0 }*)
| prim_info DIVprim = { name = "/z", prio = 5 }
| prim_info CONSUME8prim = { name = "__consume8", prio = 0 }
......
......@@ -136,6 +136,8 @@ structure Primitives = struct
flow = BD.meetVarImpliesVar (bvar stateN', bvar stateN)},
{name="seek", ty=func (ZENO, MONAD (ZENO, stateO, stateO')),
flow = BD.meetVarImpliesVar (bvar stateO', bvar stateO)},
{name="seekf", ty=func (ZENO, MONAD (UNIT, stateO, stateO')),
flow = BD.meetVarImpliesVar (bvar stateO', bvar stateO)},
{name="/z", ty=FUN([ZENO, ZENO],ZENO),flow=noFlow},
{name="index", ty=func (h, ZENO), flow = noFlow},
{name="puts", ty=func (i, MONAD (UNIT, stateP, stateP')),
......@@ -236,6 +238,7 @@ structure Primitives = struct
{name="%slice", ty=UNIT, flow = noFlow},
{name="%get-ip", ty=UNIT, flow = noFlow},
{name="%seek", ty=UNIT, flow = noFlow},
{name="%seekf", ty=UNIT, flow = noFlow},
{name="%invoke", ty=UNIT, flow = noFlow},
{name="%invoke_int", ty=UNIT, flow = noFlow},
{name="%index", ty=UNIT, flow = noFlow},
......@@ -310,6 +313,7 @@ structure Primitives = struct
val iiib = ftype [INTvtype, INTvtype, INTvtype] VECvtype
val ov = ftype [OBJvtype] VOIDvtype
val ii = ftype [INTvtype] INTvtype
val iv = ftype [INTvtype] VOIDvtype
val oi = ftype [OBJvtype] INTvtype
val oio = ftype [OBJvtype, INTvtype] OBJvtype
val oo = ftype [OBJvtype] OBJvtype
......@@ -364,6 +368,7 @@ structure Primitives = struct
| _ => raise ImpPrimTranslationBug))),
("get-ip", (t 0, fn args => action (boxI (PRIexp (IPGETprim,i,args))))),
("seek", (t 0, fn args => action (boxI (PRIexp (SEEKprim,ii,unboxI args))))),
("seekf", (t 0, fn args => action (PRIexp (SEEKFprim,iv,unboxI args)))),
(*("rseek", (t 0, fn args => action (boxI (PRIexp (RSEEKprim,ii,unboxI args))))),*)
("/z", (t 2, fn args => boxI (pr (DIVprim,iii,unboxI args)))),
("consume8", (t 0, fn args => action (boxV8 (PRIexp (CONSUME8prim,i,args))))),
......
......@@ -30,3 +30,9 @@ std::ostream& operator<<(std::ostream &out, expr &_this);
}
}
#include "binop_op.h"
#include "expr_binop.h"
#include "expr_ext.h"
#include "expr_sexpr.h"
#include "expr_visitor.h"
......@@ -9,6 +9,9 @@
#include "id_visitor.h"
#include <iosfwd>
#include <string>
extern "C" {
#include <gdsl_generic.h>
}
namespace gdsl {
namespace rreil {
......@@ -31,3 +34,7 @@ std::ostream &operator<<(std::ostream &out, id &_this);
}
}
#include "arch_id.h"
#include "shared_id.h"
#include "virtual.h"
......@@ -29,7 +29,7 @@ public:
virtual void visit(arch_id *a);
virtual void visit(shared_id *a);
virtual void visit(_virtual *a);
virtual void _default(id *s);;
virtual void _default(id *s);
void _(std::function<void(arch_id*)> c) {
this->arch_id_callback = c;
......
......@@ -8,9 +8,6 @@
#pragma once
#include "id.h"
#include <string>
extern "C" {
#include <gdsl_generic.h>
}
namespace gdsl {
namespace rreil {
......
......@@ -31,3 +31,10 @@ std::ostream& operator<<(std::ostream &out, linear &_this);
}
}
#include "linear_visitor.h"
#include "lin_var.h"
#include "lin_scale.h"
#include "lin_imm.h"
#include "lin_binop.h"
#include "binop_lin_op.h"
......@@ -30,3 +30,8 @@ std::ostream &operator<<(std::ostream &out, sexpr &_this);
}
}
#include "arbitrary.h"
#include "sexpr_cmp.h"
#include "sexpr_lin.h"
#include "sexpr_visitor.h"
......@@ -19,7 +19,6 @@ namespace rreil {
class sexpr_cmp : public sexpr {
private:
int_t size;
expr_cmp *inner;
void put(std::ostream &out);
......
......@@ -33,3 +33,14 @@ std::ostream& operator<<(std::ostream &out, statement &_this);
}
}
#include "assign.h"
#include "branch.h"
#include "cbranch.h"
#include "floating.h"
#include "ite.h"
#include "load.h"
#include "prim.h"
#include "store.h"
#include "throw.h"
#include "while.h"
MLTK=../..
JDK=/usr/lib/jvm/java-7-openjdk
JDK=/usr/lib/jvm/default-java
CC=gcc
#CC=clang
LIBDS=-L$(MLTK)/lib
......
......@@ -65,11 +65,11 @@ public class Program {
// buffer.put((byte) 0xc8);
// buffer.put((byte) 0xc3);
ByteBuffer buffer = ByteBuffer.allocateDirect(5);
buffer.put((byte) 0x3b);
buffer.put((byte) 0xfe);
buffer.put((byte) 0x78);
buffer.put((byte) 0x05);
buffer.put((byte) 0xc3);
buffer.put((byte) 0xe8);
buffer.put((byte) 0xae);
buffer.put((byte) 0xff);
buffer.put((byte) 0xff);
buffer.put((byte) 0xff);
sub(buffer);
//
......
......@@ -20,8 +20,6 @@ public class X86Binder extends ArchBinder {
*/
public X86Binder (Frontend[] frontends) {
super(specific(frontends, ArchId.X86));
setConfigFlag(X86ConfigFlag.DefaultOpndSz32);
}
/**
......@@ -35,7 +33,5 @@ public class X86Binder extends ArchBinder {
if (!checkFrontend(ArchId.X86, getFrontend()))
throw new IllegalArgumentException();
setConfigFlag(X86ConfigFlag.DefaultOpndSz32);
}
}
......@@ -8,7 +8,7 @@ package gdsl.arch;
*/
public enum X86ConfigFlag implements IConfigFlag {
MODE32(1),
DefaultOpndSz32(2);
DefaultOpndSz16(2);
private long flag;
......
......@@ -34,10 +34,9 @@ val subst-stmt-list-initial stmts = do
export subst-stmt-list-m : (subst-map, sem_stmt_list) -> S sem_stmt_list <{} => {}>
val subst-stmt-list-m state stmts = case stmts of
SEM_CONS s : let
val new-stmt = subst-stmt state s.hd
val new-state = update-with-stmt state new-stmt
in do
SEM_CONS s : do
new-stmt <- subst-stmt-m state s.hd;
new-state <- update-with-stmt state new-stmt;
#println "old stmt:";
#println (rreil-show-stmt s.hd);
#println "new stmt:";
......@@ -46,54 +45,71 @@ val subst-stmt-list-m state stmts = case stmts of
#println (show-substmap new-state);
#println ".";
continued <- subst-stmt-list-m new-state s.tl;
return (SEM_CONS {hd=new-stmt, tl=continued}) end end
return (SEM_CONS {hd=new-stmt, tl=continued})
end
| SEM_NIL : return SEM_NIL
end
export subst-stmt-list : (subst-map, sem_stmt_list) -> sem_stmt_list
val subst-stmt-list state stmts = case stmts of
SEM_CONS s : let val new-stmt = subst-stmt state s.hd
val new-state = update-with-stmt state new-stmt
in SEM_CONS {hd=new-stmt, tl=subst-stmt-list new-state s.tl}
end
| SEM_NIL : SEM_NIL
end
export update-with-stmt: (subst-map, sem_stmt) -> subst-map
export update-with-stmt: (subst-map, sem_stmt) -> S subst-map <{} => {}>
val update-with-stmt state stmt = case stmt of
SEM_ASSIGN s : update-bind-expr state s.size s.lhs s.rhs
| SEM_LOAD s : update-mark-var-overwritten state s.lhs.offset s.size s.lhs.id
| SEM_STORE s : state
| SEM_ITE s : substmap-initial # no join of branches, so we "approximate"
| SEM_WHILE s : substmap-initial # no fixpoint calculation, so we "approximate"
| SEM_CBRANCH s : state
| SEM_BRANCH s : state
| SEM_FLOP s : update-mark-varl-overwritten state s.lhs
| SEM_PRIM s : update-mark-varl-list-overwritten state s.lhs
| SEM_THROW s : state
end
| SEM_LOAD s : return (update-mark-var-overwritten state s.lhs.offset s.size s.lhs.id)
| SEM_STORE s : return state
| SEM_ITE s : return substmap-initial # no join of branches, so we "approximate"
| SEM_WHILE s : return substmap-initial # no fixpoint calculation, so we "approximate"
| SEM_CBRANCH s : return state
| SEM_BRANCH s : return state
| SEM_FLOP s : return (update-mark-varl-overwritten state s.lhs)
| SEM_PRIM s : return (update-mark-varl-list-overwritten state s.lhs)
| SEM_THROW s : return state
end
# only bind linear expressions
export update-bind-expr : (subst-map, int, sem_var, sem_expr) -> subst-map
export update-bind-expr : (subst-map, int, sem_var, sem_expr) -> S subst-map <{} => {}>
val update-bind-expr state size var expr = case expr of
SEM_SEXPR sexpr : update-bind-sexpr state size var sexpr
| x : update-mark-var-overwritten state var.offset size var.id
SEM_SEXPR sexpr : return (update-bind-sexpr state size var sexpr)
| SEM_XOR a2 : do #println ("checking "+++rreil-show-expr expr);
if size === 1 and is-inverting-xor a2.opnd1 a2.opnd2
then do #println ("checking inv "+++rreil-show-expr expr);
case subst-linear-to-cond state a2.opnd1 of
Nothing-sexpr :
return (update-bind-sexpr-inverted state size var (SEM_SEXPR_LIN a2.opnd1))
| Just-sexpr o1 :
return (update-bind-sexpr-inverted state size var o1)
| Just-sexpr-inverted o1 :
return (update-bind-sexpr state size var o1)
#TODO
end
end
else return (update-mark-var-overwritten state var.offset size var.id)
end
| x : return (update-mark-var-overwritten state var.offset size var.id)
end
val is-inverting-xor opnd1 opnd2 = case opnd2 of
SEM_LIN_IMM l : l.const === 1
| x : '0'
end
export update-bind-sexpr : (subst-map, int, sem_var, sem_sexpr) -> subst-map
val update-bind-sexpr state size var sexpr
= if sexpr-does-not-ref-to-var sexpr size var
then update-bind-linear state var.offset size var.id sexpr
else update-mark-var-overwritten state var.offset size var.id
export update-bind-sexpr-inverted : (subst-map, int, sem_var, sem_sexpr) -> subst-map
val update-bind-sexpr-inverted state size var sexpr
= if sexpr-does-not-ref-to-var sexpr size var
then update-bind-linear-inverted state var.offset size var.id sexpr
else update-mark-var-overwritten state var.offset size var.id
export sexpr-does-not-ref-to-var : (sem_sexpr, int, sem_var) -> |1|
val sexpr-does-not-ref-to-var linear size var = case linear of
SEM_SEXPR_LIN l : linear-does-not-ref-to-var l size var
| SEM_SEXPR_CMP x : expr-cmp-does-not-ref-to-var x.cmp x.size var
| SEM_SEXPR_ARB : '1'
| SEM_SEXPR_ARB : '0' # quick hack to avoid the insertion of 'arbitrary'
end
export expr-cmp-does-not-ref-to-var : (sem_expr_cmp, int, sem_var) -> |1|
......@@ -152,6 +168,9 @@ val update-mark-varl-overwritten state varl = update-mark-var-overwritten state
export update-bind-linear : (subst-map, int, int, sem_id, sem_sexpr) -> subst-map
val update-bind-linear state offset size var linear = substmap-bind-sexpr state offset size var linear
export update-bind-linear-inverted : (subst-map, int, int, sem_id, sem_sexpr) -> subst-map
val update-bind-linear-inverted state offset size var linear = substmap-bind-sexpr-inverted state offset size var linear
export update-mark-var-overwritten : (subst-map, int, int, sem_id) -> subst-map
val update-mark-var-overwritten state offset size var = substmap-mark-overwritten state offset size var
......
......@@ -4,20 +4,90 @@
#
# SEM_WHILE and SEM_ITE use the top-level function for a rough approximation
#
export subst-stmt : (subst-map, sem_stmt) -> sem_stmt
val subst-stmt state stmt = case stmt of
SEM_ASSIGN s : SEM_ASSIGN{lhs=s.lhs, size=s.size, rhs = subst-expr state s.size s.rhs}
| SEM_LOAD s : SEM_LOAD {size=s.size, lhs=s.lhs, address= subst-address state s.address}
| SEM_STORE s : SEM_STORE {size=s.size, address= subst-address state s.address, rhs=subst-linear state s.size s.rhs}
| SEM_ITE s : SEM_ITE {cond= subst-sexpr state 1 s.cond, then_branch= subst-stmt-list state s.then_branch, else_branch= subst-stmt-list state s.else_branch}
| SEM_WHILE s : SEM_WHILE {cond= subst-sexpr state 1 s.cond, body= subst-stmt-list substmap-initial s.body}
| SEM_CBRANCH s : SEM_CBRANCH {cond= subst-sexpr state 1 s.cond, target-true= subst-address state s.target-true, target-false= subst-address state s.target-false}
| SEM_BRANCH s : SEM_BRANCH {hint=s.hint, target= subst-address state s.target}
| SEM_FLOP s : SEM_FLOP {op=s.op, flags= s.flags, lhs=s.lhs, rhs= subst-varl-list state s.rhs}
| SEM_PRIM s : SEM_PRIM {op=s.op, lhs = s.lhs, rhs= subst-varl-list state s.rhs}
| SEM_THROW e : SEM_THROW e
export subst-stmt-m : (subst-map, sem_stmt) -> S sem_stmt <{} => {}>
val subst-stmt-m state stmt = case stmt of
SEM_ASSIGN s : return (SEM_ASSIGN{lhs=s.lhs, size=s.size, rhs = subst-expr state s.size s.rhs})
| SEM_LOAD s : return (SEM_LOAD {size=s.size, lhs=s.lhs, address= subst-address state s.address})
| SEM_STORE s : return (SEM_STORE {size=s.size, address= subst-address state s.address, rhs=subst-linear state s.size s.rhs})
| SEM_ITE s : do
tb <- subst-stmt-list-m state s.then_branch;
eb <- subst-stmt-list-m state s.else_branch;
newCond <- subst-cond state s.cond;
case newCond of
Nothing-sexpr : do
#println "subst-cond-ite-nothing";
return (SEM_ITE {cond= s.cond, then_branch= tb, else_branch= eb})
end
| Just-sexpr se : do
#println "subst-cond-ite-insert";
return (SEM_ITE {cond= se, then_branch= tb, else_branch= eb})
end
| Just-sexpr-inverted se : do
#println "subst-cond-ite-insert-inverted";
return (SEM_ITE {cond= se, then_branch= eb, else_branch= tb})
end
end
end
| SEM_WHILE s : do
newBody <- subst-stmt-list-m substmap-initial s.body;
return (SEM_WHILE {cond= s.cond, body= newBody})
end
| SEM_CBRANCH s : do
newCond <- subst-cond state s.cond;
case newCond of
Nothing-sexpr : do
#println "subst-cond-cbranch-nothing";
return (SEM_CBRANCH {cond= s.cond, target-true= subst-address state s.target-true, target-false= subst-address state s.target-false})
end
| Just-sexpr se : do
#println "subst-cond-cbranch-insert";
return (SEM_CBRANCH {cond= se, target-true= subst-address state s.target-true, target-false= subst-address state s.target-false})
end
| Just-sexpr-inverted se : do
#println "subst-cond-cbranch-insert-inverted";
return (SEM_CBRANCH {cond= se, target-true= subst-address state s.target-false, target-false= subst-address state s.target-true})
end
end
end
| SEM_BRANCH s : return (SEM_BRANCH {hint=s.hint, target= subst-address state s.target})
| SEM_FLOP s : return (SEM_FLOP {op=s.op, flags= s.flags, lhs=s.lhs, rhs= subst-varl-list state s.rhs})
| SEM_PRIM s : return (SEM_PRIM {op=s.op, lhs = s.lhs, rhs= subst-varl-list state s.rhs})
| SEM_THROW e : return (SEM_THROW e)
end
export subst-cond : (subst-map, sem_sexpr) -> S maybe-sexpr <{} => {}>
val subst-cond state c = case c of
SEM_SEXPR_LIN linear : return (subst-linear-to-cond state linear)
| SEM_SEXPR_CMP s : return (Just-sexpr (SEM_SEXPR_CMP {size=s.size, cmp=subst-expr-cmp state s.size s.cmp}))
| SEM_SEXPR_ARB : return (Just-sexpr c)
end
export subst-linear-to-cond: (subst-map, sem_linear) -> maybe-sexpr
val subst-linear-to-cond state linear =
case linear of
SEM_LIN_VAR var : 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 (simplify-lin-add (subst-linear state 1 s.opnd1) (subst-linear state 1 s.opnd2)))
| SEM_LIN_SUB s : Just-sexpr (SEM_SEXPR_LIN (SEM_LIN_SUB (subst-arity2 state 1 s)))
| SEM_LIN_SCALE s : Just-sexpr (SEM_SEXPR_LIN (SEM_LIN_SCALE {const=s.const, opnd=subst-linear state 1 s.opnd}))
end
#do
# case of
# Nothing-sexpr : do
# println "subst-cond-keep-var";
# return (SEM_SEXPR_LIN (SEM_LIN_VAR {id=var, offset=offset}))
# end
# | Just-sexpr linear : do
# println "subst-cond-inline-expression";
# return linear
# end
# | Just-sexpr-inverted linear : do
# println "subst-cond-inline-inverted";
# return (SEM_SEXPR_LIN (SEM_LIN_VAR {id=var, offset=offset}))
# end
# end
# end
export subst-expr : (subst-map, int, sem_expr) -> sem_expr
val subst-expr state size expr = case expr of
......@@ -38,6 +108,7 @@ val subst-expr state size expr = case expr of
end
export subst-sexpr: (subst-map, int, sem_sexpr) -> sem_sexpr
val subst-sexpr state size sexpr = case sexpr of
SEM_SEXPR_LIN linear : subst-linear-to-sexpr state size linear
......
......@@ -22,7 +22,7 @@
#
type subst-map =
Substmap-empty
| Substmap-bind-linear of {offset:int, size:int, id:sem_id, rhs:sem_sexpr, cont:subst-map}
| Substmap-bind-linear of {offset:int, size:int, id:sem_id, rhs:sem_sexpr, cont:subst-map, inverted:int}
| Substmap-mark-overwritten of {offset:int, size:int, id:sem_id, cont:subst-map}
val substmap-initial = Substmap-empty
......@@ -39,7 +39,18 @@ val substmap-initial = Substmap-empty
# subst map with right hand side bound to write location
#
export substmap-bind-sexpr : (subst-map, int, int, sem_id, sem_sexpr) -> subst-map
val substmap-bind-sexpr state offset size var linear = Substmap-bind-linear {offset=offset, size=rreil-size-by-sexpr-type size linear , id=var, rhs=linear, cont=state}
val substmap-bind-sexpr state offset size var linear
= let val newSize = rreil-size-by-sexpr-type size linear
val isInverted = 0
in Substmap-bind-linear {offset=offset, size=newSize, id=var, rhs=linear, cont=state, inverted=isInverted}
end
export substmap-bind-sexpr-inverted : (subst-map, int, int, sem_id, sem_sexpr) -> subst-map
val substmap-bind-sexpr-inverted state offset size var linear
= let val newSize = rreil-size-by-sexpr-type size linear
val isInverted = 1
in Substmap-bind-linear {offset=offset, size=newSize, id=var, rhs=linear, cont=state, inverted=isInverted}
end
......@@ -63,7 +74,7 @@ type maybe-linear = Nothing-linear | Just-linear of sem_linear
type maybe-sexpr = Nothing-sexpr | Just-sexpr of sem_sexpr
type maybe-sexpr = Nothing-sexpr | Just-sexpr of sem_sexpr | Just-sexpr-inverted of sem_sexpr
# lookup binding for location
......@@ -77,17 +88,23 @@ type maybe-sexpr = Nothing-sexpr | Just-sexpr of sem_sexpr
#
export substmap-var-to-lin: (subst-map, int, int, sem_id) -> sem_linear
val substmap-var-to-lin state offset size var = case substmap-lookup-var-to-linear state offset size var of
Nothing-linear : SEM_LIN_VAR {id=var, offset=offset}
| Just-linear linear : linear
Nothing-linear : SEM_LIN_VAR {id=var, offset=offset}
| Just-linear linear : linear
end
export substmap-var-to-sexpr: (subst-map, int, int, sem_id) -> sem_sexpr
val substmap-var-to-sexpr state offset size var = case 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
Nothing-sexpr : SEM_SEXPR_LIN (SEM_LIN_VAR {id=var, offset=offset})
| Just-sexpr linear : linear
| Just-sexpr-inverted linear : SEM_SEXPR_LIN (SEM_LIN_VAR {id=var, offset=offset})
end
export substmap-lookup-var-to-cond: (subst-map, int, sem_id) -> maybe-sexpr
val substmap-lookup-var-to-cond state offset var = substmap-lookup-var-to-sexpr state offset 1 var
# lookup binding for location, recursive worker function
#
# Parameters:
......@@ -108,7 +125,9 @@ val substmap-lookup-var-to-sexpr state offset size var = #Nothing-linear
then checkOverwritten-sexpr s.offset s.size s.id size (substmap-lookup-var-to-sexpr s.cont offset size var) # checkoverwrites
else (if size+offset <= s.offset+s.size
then (if offset===s.offset
then Just-sexpr s.rhs
then (if s.inverted === 0
then Just-sexpr s.rhs
else Just-sexpr-inverted s.rhs)
else Nothing-sexpr)
else Nothing-sexpr))
else checkOverwritten-sexpr s.offset s.size s.id size (substmap-lookup-var-to-sexpr s.cont offset size var)
......@@ -140,7 +159,7 @@ val substmap-lookup-var-to-linear state offset size var = #Nothing-linear
then (if size+offset <= s.offset or s.size+s.offset <= offset
then checkOverwritten-linear s.offset s.size s.id size (substmap-lookup-var-to-linear s.cont offset size var)
else (if size+offset <= s.offset+s.size
then (if offset===s.offset
then (if offset===s.offset and s.inverted === 0
then case s.rhs of
SEM_SEXPR_LIN l : Just-linear l
| _ : Nothing-linear
......@@ -205,6 +224,6 @@ val lin-uses-location o s v rs lin = case lin of
val show-substmap sm = case sm of
Substmap-empty : ""
| Substmap-bind-linear x : rreil-show-id x.id +++ "." +++ show-int x.offset +++ ":" +++ show-int x.size +++ " = " +++ rreil-show-sexpr x.rhs +++ "\n" +++ show-substmap x.cont
| Substmap-bind-linear x : rreil-show-id x.id +++ "." +++ show-int x.offset +++ ":" +++ show-int x.size +++ " = " +++ rreil-show-sexpr x.rhs +++ " inv="+++show-int x.inverted+++ "\n" +++ show-substmap x.cont
| Substmap-mark-overwritten x : rreil-show-id x.id +++ "." +++ show-int x.offset +++ ":" +++ show-int x.size +++ " = <?>\n" +++ show-substmap x.cont
end
This diff is collapsed.
......@@ -2,6 +2,9 @@ export decode-translate-block-optimized: (decoder-configuration, int, optimizati
export traverse-insn-list: (insn_list, insn_list_obj, (insn_list_obj, insndata) -> insn_list_obj) -> insn_list_obj
export optimization-config : configuration[vec=optimization-configuration]
#for optimization-sweep
export propagate-contextful: (|1|, {insns:sem_stmt_list, succ_a:stmts_option, succ_b:stmts_option}) -> S {insns:sem_stmt_list, succ_a:stmts_option, succ_b:stmts_option} <{} => {}>
type optimization-configuration = |5|
val optimization-config =
......
......@@ -7,7 +7,7 @@ export succ-pretty: (stmts_option, string) -> rope
val decode-translate-block-headless config limit = do
insn <- decode config;
insns <- query $insns;
#Todo: Don't use state
#Todo: Don't use state