Decoding a mips instruction :)

Not executing yet as some previous commit has broken the interpreter's local assignment

2 files changed, 21 insertions, 7 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index bf82010e..f4c19362 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -1008,6 +1008,9 @@ let fix_up_nondet typ branches annot =
       (fun e -> E_aux (E_assign (LEXP_aux (LEXP_id redex_id) annot) e) annot) branches), Just "0")
 end
 
+val debug_print : string -> unit
+declare ocaml target_rep function debug_print s = `Printf.eprintf` "%s" s
+
 (* match_pattern returns a tuple of (pattern_matches? , pattern_passed_due_to_unknown?, env_of_pattern *)
 val match_pattern : top_level -> pat tannot -> value -> bool * bool * lenv
 let rec match_pattern t_level (P_aux p (_, annot)) value_whole =
@@ -1018,7 +1021,7 @@ let rec match_pattern t_level (P_aux p (_, annot)) value_whole =
   let value = detaint value_whole in
   let taint_pat v = binary_taint (fun v _ -> v) v value_whole in
   match p with 
-  | P_lit(lit) -> 
+    | P_lit(lit) ->
     if is_lit_vector lit then
       let (V_vector n inc bits) = litV_to_vec lit default_dir in 
       match value with
@@ -1032,7 +1035,7 @@ let rec match_pattern t_level (P_aux p (_, annot)) value_whole =
         (foldr2 (fun l r rest -> (l=r) && rest) true bits bits',false,eenv)
       | V_unknown -> (true,true,eenv)
       | _ -> (false,false,eenv) end
-    else
+else
     match value with
     | V_lit(litv) -> (lit = litv, false,eenv)
     | V_vector _ _ [V_lit(litv)] -> (lit = litv,false,eenv)
@@ -1221,9 +1224,19 @@ and vec_concat_match_plev t_level pat r_vals dir l last_pat t =
 	    | #'0' -> P_lit (L_aux L_zero l') | #'1' -> P_lit (L_aux L_one l')end) (l',Nothing)) bin_chars in
 	vec_concat_match t_level binpats r_vals
       | P_vector pats -> vec_concat_match t_level pats r_vals
-      | P_id id -> (match t with
-	  | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp (Ne_const i);_;_]) ->
-	    let wilds = List.genlist (fun _ -> P_aux P_wild (l,Nothing)) (natFromInteger i) in
+      | P_id id ->
+      (match t with
+       | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp (Ne_const i);_;_]) ->
+	 let wilds = List.genlist (fun _ -> P_aux P_wild (l,Nothing)) (natFromInteger i) in
+	 let (matched_p,used_unknown,bounds,matcheds,r_vals) = vec_concat_match t_level wilds r_vals in
+	 if matched_p 
+         then (matched_p, used_unknown, 
+                   (add_to_env (id,(V_vector (if is_inc(dir) then 0 else (List.length matcheds)) dir matcheds))
+		              bounds),
+                  matcheds,r_vals)
+	 else (false,false,eenv,[],[])
+       | T_abbrev _ (T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp (Ne_const i);_;_])) ->
+ 	    let wilds = List.genlist (fun _ -> P_aux P_wild (l,Nothing)) (natFromInteger i) in
 	    let (matched_p,used_unknown,bounds,matcheds,r_vals) = vec_concat_match t_level wilds r_vals in
 	    if matched_p 
 	    then (matched_p, used_unknown, 
@@ -1272,7 +1285,7 @@ and vec_concat_match t_level pats r_vals =
     | [] -> (true,false,eenv,[],r_vals)
     | pat::pats -> match r_vals with
       | [] -> (false,false,eenv,[],[])
-      | r::r_vals -> 
+      | r::r_vals ->
 	let (matched_p,used_unknown,new_bounds) = match_pattern t_level pat r in
         if matched_p then 
           let (matched_p,used_unknown',bounds,matcheds,r_vals) = vec_concat_match  t_level pats r_vals in
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 714f4c4c..e9161382 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -324,6 +324,7 @@ let migrate_typ = function
   | Instruction_extractor.IOther -> Other
 end
 
+
 let decode_to_istate top_level value = 
   let mode = make_interp_mode true false in
   let (Context ((Interp.Env _ instructions _ _ _ _ _ _) as top_env) direction _ _ _ _ _ _) = top_level in
@@ -340,7 +341,7 @@ let decode_to_istate top_level value =
   match (instr_decoded,error) with
     | (Just instr, _) -> 
       let instr_external = match instr with
-	| Interp.V_ctor (Id_aux (Id "Some") _) _ _ (Interp.V_ctor (Id_aux (Id i) _) _ _ parm) ->
+	| Interp.V_ctor (Id_aux (Id i) _) _ _ parm ->
 	  match (find_instruction i instructions) with
 	    | Just(Instruction_extractor.Instr_form name parms effects) -> 
 	      match (parm,parms) with