Merge branch 'experimental' of versioncontrolseidl.in.tum.de:gdsl/gdsl-toolkit into experimental

detail/codegen/c1/c1.sml

@@ -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")),

detail/codegen/c1/runtime.c

@@ -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) {

detail/cps/from-core.sml

@@ -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,

detail/imp/imp-opt.sml

@@ -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

detail/imp/imp.sml

@@ -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 }

detail/semantic/primitives.sml

@@ -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))))),

specifications/rreil/rreil-translator.ml

@@ -91,7 +91,7 @@ val decode-translate-super-block config limit = let
     error <- seek (current + idx);
     result <- if error === 0 then do
       stmts <- decode-translate-block config int-max;
-      seek current;
+      seekf current;
       return (SO_SOME stmts)
     end else
       return SO_NONE

tools/semantics-opt.c

@@ -167,9 +167,8 @@ int main(int argc, char** argv) {
     string_t fmt = gdsl_merge_rope(state, gdsl_rreil_pretty(state, opt_result->rreil));
     puts(fmt);
 
-    gdsl_reset_heap(state);
-
     last_offset_ptr = gdsl_get_ip(state);
+    gdsl_reset_heap(state);
   }
 
   gdsl_destroy(state);