Fix errors around ARM not being able to decode due to instruction_extractor being very power-specific.

Note: slight interface change to instruction_extractor

10 files changed, 139 insertions, 60 deletions

diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem
index 5cf1115b..f78e2d29 100644
--- a/src/lem_interp/instruction_extractor.lem
+++ b/src/lem_interp/instruction_extractor.lem
@@ -4,27 +4,32 @@ open import Pervasives
 
 type instr_parm_typ = 
 | IBit
-| IBitvector of maybe integer
-| IRange of maybe integer
+| IBitvector of maybe nat
+| IRange of maybe nat
+| IEnum of string * nat
 | IOther
 
 type instruction_form = 
 |  Instr_form of string * list (string * instr_parm_typ) * list base_effect
 |  Skipped 
 
-val extract_instructions : string -> string -> defs tannot -> list instruction_form
+val extract_instructions : 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
+let rec extract_ityp t tag = match (t,tag) with
+  | (T_abbrev _ t,_) -> extract_ityp t tag
+  | (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 (natFromInteger 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 (natFromInteger num))
+  | (T_app "atom" _,_) -> IRange Nothing
+  | (T_app "range" (T_args [_;T_arg_nexp (Ne_const max)]),_) -> 
+    IRange (Just (natFromInteger max))
+  | (T_app "range" _,_) -> IRange Nothing
+  | (T_app i (T_args []),Tag_enum max) ->
+    IEnum i (natFromInteger max)
   | _ -> IOther
 end 
 
@@ -32,17 +37,15 @@ let extract_parm (E_aux e (_,tannot)) =
   match e with
     | E_id (Id_aux (Id i) _) ->
       match tannot with
-	| Just(t,_,_,_) -> (i,(extract_ityp t))
+	| Just(t,tag,_,_) -> (i,(extract_ityp t tag))
 	| _ -> (i,IOther) end
     | _ -> 
       let i = "Unnamed" in
       match tannot with
-	| Just(t,_,_,_) -> (i,(extract_ityp t))
+	| Just(t,tag,_,_) -> (i,(extract_ityp t tag))
 	| _ -> (i,IOther) end
 end
 
-let rec extract_from_ast ast = []
-
 let rec extract_from_decode decoder = 
   match decoder with
     | [] -> []
@@ -62,6 +65,25 @@ let rec extract_effects_of_fcl id execute = match execute with
   | _::executes -> extract_effects_of_fcl id executes
 end
 
+let rec extract_patt_parm (P_aux p (_,tannot)) = 
+  let t = match tannot with
+    | Just(t,tag,_,_) -> extract_ityp t tag
+    | _ -> IOther end in
+  match p with
+    | P_lit lit -> ("",t)
+    | P_wild -> ("Unnamed",t)
+    | P_as _ (Id_aux (Id id) _) -> (id,t)
+    | P_typ typ p -> extract_patt_parm p
+    | P_id (Id_aux (Id id) _) -> (id,t)
+    | P_app (Id_aux (Id id) _) [] -> (id,t)
+    | _ -> ("",t) end
+
+let rec extract_from_execute fcls = match fcls with
+  | [] -> []
+  | FCL_aux (FCL_Funcl _ (P_aux (P_app (Id_aux (Id i) _) parms) _) _) (_,Just(_,_,_,Effect_aux(Effect_set efs) _))::fcls ->
+    (Instr_form i (List.map extract_patt_parm parms) efs)::extract_from_execute fcls
+end
+
 let rec extract_effects instrs execute = 
   match instrs with
     | [] -> []
@@ -70,10 +92,14 @@ let rec extract_effects instrs execute =
       (Instr_form id parms (extract_effects_of_fcl id execute))::(extract_effects instrs execute)
 end
 
-let extract_instructions decode_name execute_name defs = 
+let extract_instructions_old decode_name execute_name defs = 
   let (Just decoder) = find_function defs (Id_aux (Id decode_name) Unknown) in
   let (Just executer) = find_function defs (Id_aux (Id execute_name) Unknown) in
   let instr_no_effects = extract_from_decode decoder in
   let instructions = extract_effects instr_no_effects executer in
   instructions
-  
+
+let extract_instructions execute_name defs =
+  let (Just executer) = find_function defs (Id_aux (Id execute_name) Unknown) in
+  let instructions = extract_from_execute executer in
+  instructions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 0b7916e0..b61f724a 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -25,7 +25,7 @@ let val_annot typ = Just(typ,Tag_empty,[],pure)
 
 let ctor_annot typ = Just(typ,Tag_ctor,[],pure)
 
-let enum_annot typ = Just(typ,Tag_enum,[],pure)
+let enum_annot typ max = Just(typ,Tag_enum max,[],pure)
 
 (* This is different from OCaml: it will drop elements from the longest list. *)
 let foldr2 f x l l' = List.foldr (Tuple.uncurry f) x (List.zip l l')
@@ -781,7 +781,7 @@ let rec to_exp mode env v : (exp tannot * lenv) =
     (Interp_ast.Unknown, 
      if is_ctor 
      then match ctor_kind with
-       | Just(C_Enum _) -> (enum_annot (val_typ v))
+       | Just(C_Enum i) -> (enum_annot (val_typ v) (integerFromNat i))
        | _ -> (ctor_annot (val_typ v)) end
      else (val_annot (val_typ v))) in
   let annot = mk_annot false Nothing in
@@ -951,7 +951,7 @@ let rec match_pattern t_level (P_aux p (_, annot)) value_whole =
      else (false,false,eenv)
    | V_lit (L_aux (L_num i) _) ->
      match tag with 
-       | Tag_enum -> 
+       | Tag_enum _ -> 
 	 match Map.lookup (get_id (Id_aux id Unknown)) lets with
 	   | Just(V_ctor _ t (C_Enum j) _) -> 
 	     if i = (integerFromNat j) then (true,false,eenv)
@@ -1274,7 +1274,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 	      (match in_env regs name with
 		| Just(value) -> (Value value, l_mem,l_env)
 		| Nothing -> (Error l ("Internal error: " ^ name ^ " unbound on Tag_global"),l_mem,l_env) end) end
-        | Tag_enum ->
+        | Tag_enum _ ->
           match in_env lets name with
             | Just(value) -> (Value value,l_mem,l_env)
 	    | Nothing -> (Error l ("Internal error: " ^ name ^ " unbound on Tag_enum "), l_mem,l_env)
@@ -2544,11 +2544,11 @@ let rec extract_default_direction (Defs defs) = match defs with
       | 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*)
+(*TODO Contemplate making execute environment variable instead of constant*)
 let to_top_env external_functions defs = 
   let direction = (extract_default_direction defs) in
   let t_level = Env (to_fdefs defs) 
-                    (extract_instructions "decode" "execute" defs) 
+                    (extract_instructions "execute" defs) 
                     direction
                     Map.empty (* empty letbind and enum values, call below will fill in any *) 
 		    (to_registers direction defs) 
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 2af90d6f..aa802641 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -194,15 +194,21 @@ let rec extern_mem_value mode v = match v with
   | _ -> Assert_extra.failwith ("extern_mem_value received non-externable value " ^ (Interp.string_of_value v))
 end 
 
-let rec extern_ifield_value v = match v with
-  | Interp.V_track v regs -> extern_ifield_value v 
-  | Interp.V_vector fst inc bits -> bits_from_ibits bits
-  | Interp.V_vector_sparse fst stop inc bits default ->
-    extern_ifield_value (Interp_lib.fill_in_sparse v)
-  | Interp.V_lit (L_aux L_zero _) -> [Bitc_zero]
-  | Interp.V_lit (L_aux L_false _) -> [Bitc_zero]
-  | Interp.V_lit (L_aux L_one _) ->  [Bitc_one]
-  | Interp.V_lit (L_aux L_true _) -> [Bitc_one]
+let rec extern_ifield_value v ftyp = match (v,ftyp) with
+  | (Interp.V_track v regs,_) -> extern_ifield_value v ftyp
+  | (Interp.V_vector fst inc bits,_) -> bits_from_ibits bits
+  | (Interp.V_vector_sparse fst stop inc bits default,_) ->
+    extern_ifield_value (Interp_lib.fill_in_sparse v) ftyp
+  | (Interp.V_lit (L_aux L_zero _),_) -> [Bitc_zero]
+  | (Interp.V_lit (L_aux L_false _),_) -> [Bitc_zero]
+  | (Interp.V_lit (L_aux L_one _),_) ->  [Bitc_one]
+  | (Interp.V_lit (L_aux L_true _),_) -> [Bitc_one]
+  | (Interp.V_lit (L_aux (L_num i) _),Range (Just n)) -> bit_list_of_integer n i
+  | (Interp.V_lit (L_aux (L_num i) _),Enum _ n) -> bit_list_of_integer n i
+  | (Interp.V_lit (L_aux (L_num i) _),_) -> bit_list_of_integer 64 i
+  | (Interp.V_ctor _ _ (Interp.C_Enum i) _,Enum _ n) -> bit_list_of_integer n (integerFromNat i)
+  | (Interp.V_ctor _ _ (Interp.C_Enum i) _,_) -> bit_list_of_integer 64 (integerFromNat i)
+  | _ -> Assert_extra.failwith ("extern_ifield_value given non-externable " ^ (Interp.string_of_value v) ^ " ftyp is " ^ show ftyp)
 end 
 
 let rec slice_reg_value v start stop = 
@@ -317,8 +323,9 @@ end
 
 let migrate_typ = function
   | Instruction_extractor.IBit -> Bit
-  | Instruction_extractor.IBitvector len ->
-    Bvector (match len with Nothing -> Nothing | Just i -> Just (natFromInteger i) end) 
+  | Instruction_extractor.IBitvector len -> Bvector len  
+  | Instruction_extractor.IRange len -> Range len
+  | Instruction_extractor.IEnum s max -> Enum s max
   | Instruction_extractor.IOther -> Other
 end
 
@@ -342,11 +349,13 @@ let decode_to_istate top_level value =
 	      match (parm,parms) with
 		| (Interp.V_lit (L_aux L_unit _),[]) -> (name, [], effects)
 		| (value,[(p_name,ie_typ)]) -> 
-		  (name, [(p_name,(migrate_typ ie_typ), (extern_ifield_value value))], effects)
+		  let t = migrate_typ ie_typ in
+		  (name, [(p_name,t, (extern_ifield_value value t))], effects)
 		| (Interp.V_tuple vals,parms) -> 
 		  (name, 
 		   (Interp.map2 (fun value (p_name,ie_typ) -> 
-		     (p_name,(migrate_typ ie_typ),(extern_ifield_value value))) vals parms), effects)
+		     let t = migrate_typ ie_typ in
+		     (p_name,t,(extern_ifield_value value t))) vals parms), effects)
           end end end in 
       let (arg,_) = Interp.to_exp mode Interp.eenv instr in
       let (instr_decoded,error) = interp_to_value_helper value instr_external internal_direction
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index e0c656eb..adf46803 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -378,15 +378,17 @@ val initial_instruction_state : context -> string -> list register_value -> inst
 (*Type representint the constructor parameters in instruction, other is a type not representable externally*)
 type instr_parm_typ = 
   | Bit (*A single bit, represented as a one element Bitvector as a value*)
-  | Range of maybe nat (*Internall represented as a number, externally as a bitvector of length int *)
-  | Other (*An unrepresentable type, will be represented as Unknown in instruciton form *)
   | Bvector of maybe nat (* A bitvector type, with length when statically known *)
+  | Range of maybe nat (*Internally represented as a number, externally as a bitvector of length nat *)
+  | Enum of string * nat (*Internally represented as either a number or constructor, externally as a bitvector*)
+  | Other (*An unrepresentable type, will be represented as Unknown in instruciton form *)
 
 let instr_parm_typEqual ip1 ip2 = match (ip1,ip2) with
   | (Bit,Bit) -> true
-  | (Other,Other) -> true
-  | (Range i1,Range i2) -> i1 = i2
   | (Bvector i1,Bvector i2) -> i1 = i2
+  | (Range i1,Range i2) -> i1 = i2
+  | (Enum s1 i1,Enum s2 i2) -> s1 = s2 && i1 = i2
+  | (Other,Other) -> true
   | _ -> false
 end 
 
@@ -395,6 +397,18 @@ instance (Eq instr_parm_typ)
   let (<>) ip1 ip2 = not (instr_parm_typEqual ip1 ip2)
 end 
 
+let instr_parm_typShow ip = match ip with
+  | Bit -> "Bit"
+  | Bvector i -> "Bvector " ^ show i
+  | Range i -> "Range " ^ show i
+  | Enum s i -> "Enum " ^ s ^ " " ^ show i
+  | Other -> "Other"
+ end
+
+instance (Show instr_parm_typ)
+let show = instr_parm_typShow
+end
+
 (*A representation of the AST node for each instruction in the spec, with concrete values from this call,
   and the potential static effects from the funcl clause for this instruction 
   Follows the form of the instruction in instruction_extractor, but populates the parameters with actual values
@@ -768,4 +782,32 @@ val byte_list_of_opcode : opcode -> list byte
 let byte_list_of_opcode (opc:opcode) : list byte = 
   match opc with
   | Opcode bs -> bs
+ end
+
+(** ****************************************** *)
+(** show type class instantiations             *)
+(** ****************************************** *)
+
+let stringFromAddress (Address bs i) = 
+  let i' = integer_of_byte_list bs in
+  if i=i' then
+    show i (*TODO: should be made to match the src/pp.ml pp_address*)
+  else
+    "stringFromAddress bytes and integer mismatch"
+
+instance (Show address)
+  let show = stringFromAddress
+end
+
+let stringFromByte_lifted bl =
+  match byte_of_byte_lifted bl with
+  | Nothing -> "u?"  
+  | Just (Byte bits) -> 
+      let i = integer_of_bit_list bits in
+      show i
   end
+
+instance (Show byte_lifted)
+  let show = stringFromByte_lifted
+end
+
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index c7f42e02..c5c550da 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -1,4 +1,5 @@
 open import Pervasives
+open import Interp_utilities
 open import Interp
 open import Interp_ast
 import Assert_extra Maybe_extra (* For failwith for error reporting while debugging; and for fromJust when we know it's not Nothing *)
@@ -10,11 +11,6 @@ open import Bool
 
 type signed = Unsigned | Signed
 
-let rec power (a: integer) (b: integer) : integer =
- if b <= 0 
- then 1
- else a * (power a (b-1))
-
 let hardware_mod (a: integer) (b:integer) : integer = 
  if a < 0 && b < 0
  then (abs a) mod (abs b)
diff --git a/src/lem_interp/interp_utilities.lem b/src/lem_interp/interp_utilities.lem
index 196655e2..7a667478 100644
--- a/src/lem_interp/interp_utilities.lem
+++ b/src/lem_interp/interp_utilities.lem
@@ -1,6 +1,11 @@
 open import Interp_ast
 open import Pervasives
 
+let rec power (a: integer) (b: integer) : integer =
+ if b <= 0 
+ then 1
+ else a * (power a (b-1))
+
 type tannot = maybe (t * tag * list nec * effect)
 
 let get_exp_l (E_aux e (l,annot)) = l
@@ -88,7 +93,7 @@ let string_of_tag tag = match tag with
   | Tag_extern _ -> "extern"
   | Tag_default -> "default"
   | Tag_spec -> "spec"
-  | Tag_enum -> "enum"
+  | Tag_enum i -> "enum"
   | Tag_alias -> "alias"
 end      
 
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 3f167ffc..25a9f41b 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -289,7 +289,7 @@ let pp_format_tag = function
   | External None -> "(Tag_extern Nothing)"
   | Default -> "Tag_default"
   | Constructor -> "Tag_ctor"
-  | Enum -> "Tag_enum"
+  | Enum i -> "(Tag_enum " ^ (lemnum string_of_int i) ^ ")"
   | Alias -> "Tag_alias"
   | Spec -> "Tag_spec"
 
diff --git a/src/type_check.ml b/src/type_check.ml
index 5b5a0864..e76f40be 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -265,12 +265,12 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
 	      then typ_error l ("Constructor " ^ i ^ " expects arguments of type " ^ (t_to_string t) ^ ", found none")
 	      else default
             | _ -> raise (Reporting_basic.err_unreachable l "Constructor tannot does not have function type"))
-	| Some(Base((params,t),Enum,cs,ef,bounds)) ->
+	| Some(Base((params,t),Enum max,cs,ef,bounds)) ->
 	  let t,cs,ef,_ = subst params false t cs ef in
 	  if conforms_to_t d_env false false t expect_t
 	  then 
 	    let tp,cp = type_consistent (Expr l) d_env Guarantee false t expect_t in
-	    (P_aux(P_app(id,[]),(l,tag_annot t Enum)),Envmap.empty,cs@cp,bounds,tp)
+	    (P_aux(P_app(id,[]),(l,tag_annot t (Enum max))),Envmap.empty,cs@cp,bounds,tp)
 	  else default
 	| _ -> default)
     | P_app(id,pats) -> 
@@ -476,10 +476,10 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
         | Tfn(t1,t',IP_none,e) -> 
           typ_error l ("Constructor " ^ i ^ " expects arguments of type " ^ (t_to_string t) ^ ", found none")
         | _ -> raise (Reporting_basic.err_unreachable l "Constructor tannot does not have function type"))
-      | Some(Base((params,t),Enum,cs,ef,bounds)) ->
+      | Some(Base((params,t),(Enum max),cs,ef,bounds)) ->
         let t',cs,_,_ = subst params false t cs ef in
         let t',cs',ef',e' = 
-	  type_coerce (Expr l) d_env Require false false t' (rebuild (cons_tag_annot t' Enum cs)) expect_t in
+	  type_coerce (Expr l) d_env Require false false t' (rebuild (cons_tag_annot t' (Enum max) cs)) expect_t in
         (e',t',t_env,cs@cs',nob,ef')
       | Some(Base(tp,Default,cs,ef,_)) | Some(Base(tp,Spec,cs,ef,_)) ->
         typ_error l ("Identifier " ^ i ^ " must be defined, not just specified, before use")
@@ -641,7 +641,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	      (E_aux (E_app(id, parms),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t
       in
       (match Envmap.apply t_env i with
-      | Some(Base(tp,Enum,_,_,_)) ->
+      | Some(Base(tp,Enum _,_,_,_)) ->
         typ_error l ("Expected function with name " ^ i ^ " but found an enumeration identifier")
       | Some(Base(tp,Default,_,_,_)) ->
         typ_error l ("Function " ^ i ^ " must be specified, not just declared as a default, before use")
@@ -715,7 +715,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	      (E_aux (E_app_infix(lft,op,rht),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t 
       in
       (match Envmap.apply t_env i with
-      | Some(Base(tp,Enum,cs,ef,b)) -> 
+      | Some(Base(tp,Enum _,cs,ef,b)) -> 
 	typ_error l ("Expected function with name " ^ i ^ " but found an enumeration identifier")
       | Some(Base(tp,Default,cs,ef,b)) -> 
 	typ_error l ("Function " ^ i ^ " must be defined, not just declared as default, before use")
@@ -1651,7 +1651,8 @@ let check_type_def envs (TD_aux(td,(l,annot))) =
     | TD_enum(id,nmscm,ids,_) -> 
       let id' = id_to_string id in
       let ids' = List.map id_to_string ids in
-      let ty = Base (([],{t = Tid id' }),Enum,[],pure_e,nob) in
+      let max = (List.length ids') -1 in
+      let ty = Base (([],{t = Tid id' }),Enum max,[],pure_e,nob) in
       let t_env = List.fold_right (fun id t_env -> Envmap.insert t_env (id,ty)) ids' t_env in
       let enum_env = Envmap.insert d_env.enum_env (id',ids') in
       (TD_aux(td,(l,ty)),Env({d_env with enum_env = enum_env;},t_env,b_env,tp_env))
diff --git a/src/type_internal.ml b/src/type_internal.ml
index f46b5409..a459c78e 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -78,7 +78,7 @@ type tag =
   | External of string option
   | Default
   | Constructor
-  | Enum
+  | Enum of int
   | Alias
   | Spec
 
@@ -223,7 +223,7 @@ let tag_to_string = function
   | External (Some s) -> "External " ^ s
   | Default -> "Default"
   | Constructor -> "Constructor"
-  | Enum -> "Enum"
+  | Enum _ -> "Enum"
   | Alias -> "Alias"
   | Spec -> "Spec"
 
diff --git a/src/type_internal.mli b/src/type_internal.mli
index d0740ecf..0cfa5089 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -78,7 +78,7 @@ type tag =
   | External of string option (* External function or register name *)
   | Default (* Variable has default type, has not been bound *)
   | Constructor (* Variable is a data constructor *)
-  | Enum (* Variable came from an enumeration *)
+  | Enum of int (* Variable came from an enumeration, int tells me the highest possible numeric value *)
   | Alias (* Variable came from a register alias *)
   | Spec (* Variable came from a val specification *)