Adding undefined

Also interpreter now supports reading and writing of basic registers (i.e with no subranges yet)

8 files changed, 19 insertions, 2 deletions

diff --git a/src/ast.ml b/src/ast.ml
index d280f4b8..bf5ecf31 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -147,6 +147,7 @@ lit_aux =  (* Literal constant *)
  | L_num of int (* natural number constant *)
  | L_hex of string (* bit vector constant, C-style *)
  | L_bin of string (* bit vector constant, C-style *)
+ | L_undef (* constant representing undefined values *)
  | L_string of string (* string constant *)
 
 
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 3b27b840..90b2d240 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -273,6 +273,7 @@ let to_ast_lit (Parse_ast.L_aux(lit,l)) : lit =
     | Parse_ast.L_one -> L_one
     | Parse_ast.L_true -> L_true
     | Parse_ast.L_false -> L_false
+    | Parse_ast.L_undef -> L_undef
     | Parse_ast.L_num(i) -> L_num(i)
     | Parse_ast.L_hex(h) -> L_hex(h)
     | Parse_ast.L_bin(b) -> L_bin(b)
diff --git a/src/lem_interp/ast.lem b/src/lem_interp/ast.lem
index aebbebc6..51831898 100644
--- a/src/lem_interp/ast.lem
+++ b/src/lem_interp/ast.lem
@@ -8,7 +8,7 @@ type l =
   | Trans of string * option l
   | Range of num * num
 
- val disjoint : forall 'a . set 'a -> set 'a -> bool
+val disjoint : forall 'a . set 'a -> set 'a -> bool
 let disjoint s1 s2 = 
   let diff = s1 inter s2 in
   diff = Pervasives.empty
@@ -122,6 +122,7 @@ type lit =  (* Literal constant *)
  | L_num of num (* natural number constant *)
  | L_hex of string (* bit vector constant, C-style *)
  | L_bin of string (* bit vector constant, C-style *)
+ | L_undef (* constant representing undefined values *)
  | L_string of string (* string constant *)
 
 
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index face5e27..f7e473c1 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -396,6 +396,14 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level lexp =
     | (LEXP_id id,true) -> 
       match in_env l_env id with
       | Some (V_boxref n) -> (Value (V_lit L_unit), update_mem l_mem n value, l_env)
+      | None -> 
+	match in_reg regs id with
+	| Some regf -> (Action (Write_reg regf None value) (Frame (Id "0") (E_id (Id "0")) l_env l_mem Top),l_mem,l_env)
+	| None -> (*Should check memory here*)
+	  let (Mem c m) = l_mem in
+	  let l_mem = (Mem (c+1) m) in
+	  (Value (V_lit L_unit), update_mem l_mem c value, (id,(V_boxref c))::l_env)
+        end
       end 
    end
 	
diff --git a/src/lexer.mll b/src/lexer.mll
index 1aa5d18d..4a8058e5 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -92,6 +92,7 @@ let kw_table =
      ("true",                    (fun x -> True));
      ("Type",                    (fun x -> TYPE));
      ("typedef",		 (fun x -> Typedef));
+     ("undefined",               (fun x -> Undefined));
      ("union",			 (fun x -> Union));
      ("with",                    (fun x -> With));
      ("val",                     (fun x -> Val));
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 23957118..b12651c0 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -137,6 +137,7 @@ lit_aux =  (* Literal constant *)
  | L_num of int (* natural number constant *)
  | L_hex of string (* bit vector constant, C-style *)
  | L_bin of string (* bit vector constant, C-style *)
+ | L_undef (* undefined value *)
  | L_string of string (* string constant *)
 
 
diff --git a/src/parser.mly b/src/parser.mly
index 1d4b7a0e..e4bcfb05 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -122,7 +122,7 @@ let star = "*"
 
 %token And As Bits By Case Clause Const Default Dec Effect Effects End Enumerate Else False
 %token Forall Foreach Function_ If_ In IN Inc Let_ Member Nat Order Pure Rec Register
-%token Scattered Struct Switch Then True Type TYPE Typedef Union With Val
+%token Scattered Struct Switch Then True Type TYPE Typedef Undefined Union With Val
 
 /* Avoid shift/reduce conflict - see right_atomic_exp rule */
 %nonassoc Then
@@ -376,6 +376,8 @@ lit:
     { lloc (L_bin $1) }
   | Hex
     { lloc (L_hex $1) }
+  | Undefined
+    { lloc L_undef }
 
 
 atomic_pat:
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index bcc5961d..0612d78b 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -166,6 +166,7 @@ let pp_format_lit (L_aux(l,_)) =
   | L_false -> "false"
   | L_num(i) -> string_of_int i
   | L_hex(n) | L_bin(n) -> n
+  | L_undef -> "undefined"
   | L_string(s) -> "\"" ^ s ^ "\"" 
 
 let pp_lit ppf l = base ppf (pp_format_lit l)
@@ -456,6 +457,7 @@ let pp_format_lit_lem (L_aux(l,_)) =
   | L_num(i) -> "(L_num " ^ string_of_int i ^ ")"
   | L_hex(n) -> "(L_hex " ^ n ^ ")"
   | L_bin(n) -> "(L_bin " ^ n ^ ")"
+  | L_undef -> "L_undef"
   | L_string(s) -> "(L_string \"" ^ s ^ "\")" 
 
 let pp_lem_lit ppf l = base ppf (pp_format_lit_lem l)