Correct directionality in interpreter. Now the interpreter shouldn't use inc unless that's the current default or there's no default set in the spec

5 files changed, 50 insertions, 31 deletions

diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem
index 9ff4dd49..5cf1115b 100644
--- a/src/lem_interp/instruction_extractor.lem
+++ b/src/lem_interp/instruction_extractor.lem
@@ -5,6 +5,7 @@ open import Pervasives
 type instr_parm_typ = 
 | IBit
 | IBitvector of maybe integer
+| IRange of maybe integer
 | IOther
 
 type instruction_form = 
@@ -13,29 +14,35 @@ type instruction_form =
 
 val extract_instructions : string -> string -> defs tannot -> list instruction_form
 
+let extract_ityp t = match t with
+  | T_id "bit" -> IBit
+  | T_id "bool" -> IBit
+  | T_app "vector" (T_args [_; T_arg_nexp (Ne_const len); _; T_arg_typ (T_id "bit")]) ->
+    IBitvector (Just len)
+  | T_app "vector" (T_args [_;_;_;T_arg_typ (T_id "bit")]) -> IBitvector Nothing
+  | T_app "atom" (T_args [T_arg_nexp (Ne_const num)]) ->
+    IRange (Just num)
+  | T_app "atom" _ -> IRange Nothing
+  | T_app "range" (T_args [_;T_arg_nexp (Ne_const max)]) -> IRange (Just max)
+  | T_app "range" _ -> IRange Nothing
+  | _ -> IOther
+end 
+
 let extract_parm (E_aux e (_,tannot)) =
   match e with
     | E_id (Id_aux (Id i) _) ->
       match tannot with
-	| Just(T_id "bit",_,_,_) -> (i,IBit)
-	| Just(T_id "bool",_,_,_) -> (i,IBit)
-	| Just(T_app "vector" (T_args [T_arg_nexp _; T_arg_nexp (Ne_const len); _; T_arg_typ (T_id "bit")]),_,_,_) ->
-	  (i,IBitvector (Just len))
-	| Just(T_app "vector" (T_args [T_arg_nexp _; T_arg_nexp _; _; T_arg_typ (T_id "bit")]),_,_,_) ->
-	  (i,IBitvector Nothing)
+	| Just(t,_,_,_) -> (i,(extract_ityp t))
 	| _ -> (i,IOther) end
     | _ -> 
       let i = "Unnamed" in
       match tannot with
-	| Just(T_id "bit",_,_,_) -> (i,IBit)
-	| Just(T_id "bool",_,_,_) -> (i,IBit)
-	| Just(T_app "vector" (T_args [T_arg_nexp _; T_arg_nexp (Ne_const len); _; T_arg_typ (T_id "bit")]),_,_,_) ->
-	  (i,IBitvector (Just len))
-	| Just(T_app "vector" (T_args [T_arg_nexp _; T_arg_nexp _; _; T_arg_typ (T_id "bit")]),_,_,_) ->
-	  (i,IBitvector Nothing)
+	| Just(t,_,_,_) -> (i,(extract_ityp t))
 	| _ -> (i,IOther) end
 end
 
+let rec extract_from_ast ast = []
+
 let rec extract_from_decode decoder = 
   match decoder with
     | [] -> []
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 0c30cca8..9106f7b6 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -2445,8 +2445,8 @@ let rec extract_default_direction (Defs defs) = match defs with
   | [] -> IInc (*When lack of a declared default, go for inc*)
   | def::defs ->
     match def with
-      | DEF_default (DT_aux (DT_order Oinc) _) -> IInc
-      | DEF_default (DT_aux (DT_order Odec) _) -> IDec
+      | DEF_default (DT_aux (DT_order (Ord_aux Ord_inc _)) _) -> IInc
+      | DEF_default (DT_aux (DT_order (Ord_aux Ord_dec _)) _) -> IDec
       | _ -> extract_default_direction (Defs defs) end end
 
 (*TODO Contemplate making decode and execute environment variables instead of these constants*)
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index f3dad5bf..459ec828 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -8,7 +8,7 @@ open import Assert_extra
 
 
 val intern_reg_value : register_value -> Interp.value
-val intern_mem_value : memory_value -> Interp.value
+val intern_mem_value : direction -> memory_value -> Interp.value
 val extern_reg_value : maybe nat -> Interp.value -> register_value
 val extern_mem_value : interp_mode -> Interp.value -> (memory_value * maybe (list reg_name))
 val extern_reg : Interp.reg_form -> maybe (nat * nat) -> reg_name
@@ -79,22 +79,30 @@ let bits_to_word8 b =
   then natFromInteger (integerFromBoolList (false,(List.reverse (List.map to_bool b))))
   else Assert_extra.failwith "bits_to_word8 given a non-8 list or one containing ? and u"
 
-(*!!! All but reg_value should take a mode to get direction and start correct*)
-let intern_opcode (Opcode v) =
-  Interp.V_vector 0 Interp.IInc
-    (List.concatMap (fun (Byte(bits)) -> (List.map bit_to_ibit bits)) v)
+let intern_direction = function
+  | D_increasing -> Interp.IInc
+  | D_decreasing -> Interp.IDec
+end
+
+let intern_opcode direction (Opcode v) =
+  let bits = List.concatMap (fun (Byte(bits)) -> (List.map bit_to_ibit bits)) v in
+  let direction = intern_direction direction in
+  Interp.V_vector (if Interp.is_inc(direction) then 0 else (List.length(bits) - 1)) direction bits
 		   
 let intern_reg_value v = match v with
   | <| rv_bits=[b] |> -> bitl_to_ibit b
-  | _ -> Interp.V_vector v.rv_start (if v.rv_dir = D_increasing then Interp.IInc else Interp.IDec) (bitls_to_ibits v.rv_bits)
+  | _ -> Interp.V_vector v.rv_start (intern_direction v.rv_dir) (bitls_to_ibits v.rv_bits)
 end
 
-(*!!! Another two that need the direction *)
-let intern_mem_value v = 
-  Interp.V_vector 0 Interp.IInc (List.concatMap (fun (Byte_lifted bits) -> bitls_to_ibits bits) v)
+let intern_mem_value direction v = 
+  let bits = (List.concatMap (fun (Byte_lifted bits) -> bitls_to_ibits bits) v) in
+  let direction = intern_direction direction in
+  Interp.V_vector (if Interp.is_inc(direction) then 0 else (List.length(bits) -1)) direction bits
 
-let intern_ifield_value v =
-  Interp.V_vector 0 Interp.IInc (bits_to_ibits v)
+let intern_ifield_value direction v =
+  let bits = bits_to_ibits v in
+  let direction = intern_direction direction in
+  Interp.V_vector (if Interp.is_inc direction then 0 else (List.length(bits) -1)) direction bits
 
 (*let byte_list_of_integer size num = 
   if (num < 0)
@@ -314,8 +322,8 @@ end
 
 let decode_to_istate top_level value = 
   let mode = make_mode true false in
-  let (arg,_) = Interp.to_exp mode Interp.eenv (intern_opcode value) in
   let (Context ((Interp.Env _ instructions _ _ _ _ _ _) as top_env) direction _ _ _ _) = top_level in
+  let (arg,_) = Interp.to_exp mode Interp.eenv (intern_opcode direction value) in
   let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
   let (instr_decoded,error) = interp_to_value_helper value ("",[],[]) internal_direction
     (fun _ -> Interp.resume 
@@ -369,9 +377,9 @@ let decode_to_instruction (top_level:context) (value:opcode) : instruction_or_de
 val instruction_to_istate : context -> instruction -> instruction_state 
 let instruction_to_istate (top_level:context) (((name, parms, _) as instr):instruction) : instruction_state  = 
   let mode = make_mode true false in
-  let (Context top_env _ _ _ _ _) = top_level in
+  let (Context top_env direction _ _ _ _) = top_level in
   let get_value (name,typ,v) = 
-    let vec = intern_ifield_value v in
+    let vec = intern_ifield_value direction v in
     let v = match vec with
       | Interp.V_vector start dir bits ->
 	match typ with
@@ -415,7 +423,7 @@ let rec interp_to_outcome mode context thunk =
         let (location, length, tracking) = (f mode value) in 
 	if (List.length location) = 8
         then Read_mem read_k (Address_lifted location) length tracking 
-	  (fun v -> IState (Interp.add_answer_to_stack next_state (intern_mem_value v)) context)
+	  (fun v -> IState (Interp.add_answer_to_stack next_state (intern_mem_value direction v)) context)
 	else Error ("Memory address on read is not 64 bits")
       | _ -> Error ("Memory " ^ i ^ " function with read kind not found")
       end
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index e4de0d71..1e97e061 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -127,7 +127,9 @@ let lt_range (V_tuple[v1;v2]) =
 
 let bit_to_bool b = match detaint b with
   | V_lit (L_aux L_zero _) -> false
+  | V_lit (L_aux L_false _) -> false
   | V_lit (L_aux L_one _) -> true
+  | V_lit (L_aux L_true _) -> true
   end ;;
 let bool_to_bit b = match b with
     false -> V_lit (L_aux L_zero Unknown)
@@ -137,7 +139,9 @@ let bool_to_bit b = match b with
 let bitwise_not_bit v = 
   let lit_not (L_aux l loc) = match l with
     | L_zero -> (V_lit (L_aux L_one loc))
-    | L_one  -> (V_lit (L_aux L_zero loc)) end in
+    | L_false -> (V_lit (L_aux L_one loc))
+    | L_one  -> (V_lit (L_aux L_zero loc))
+    | L_true -> (V_lit (L_aux L_zero loc)) end in
   retaint v (match detaint v with
   | V_lit lit -> lit_not lit
   | V_unknown -> V_unknown end)
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 0366bfa9..1764e46b 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -408,7 +408,7 @@ let instr_parm_to_string (name, typ, value) =
   name ^"="^
   match typ with
     | Other -> "Unrepresentable external value"
-    | _ -> let intern_v = (Interp_inter_imp.intern_ifield_value value) in
+    | _ -> let intern_v = (Interp_inter_imp.intern_ifield_value D_increasing value) in
 	      match Interp_lib.to_num Interp_lib.Unsigned intern_v with
 		| V_lit (L_aux(L_num n, _)) -> string_of_big_int n
 		| _ -> ifield_to_string value