diff options
| -rw-r--r-- | language/l2.ott | 2 | ||||
| -rw-r--r-- | language/l2_parse.ott | 1 | ||||
| -rw-r--r-- | src/ast.ml | 1 | ||||
| -rw-r--r-- | src/initial_check.ml | 1 | ||||
| -rw-r--r-- | src/lem_interp/ast.lem | 3 | ||||
| -rw-r--r-- | src/lem_interp/interp.lem | 8 | ||||
| -rw-r--r-- | src/lexer.mll | 1 | ||||
| -rw-r--r-- | src/parse_ast.ml | 1 | ||||
| -rw-r--r-- | src/parser.mly | 4 | ||||
| -rw-r--r-- | src/pretty_print.ml | 2 |
10 files changed, 22 insertions, 2 deletions
diff --git a/language/l2.ott b/language/l2.ott index fdd1dadf..11a57856 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -471,6 +471,8 @@ lit :: 'L_' ::= | hex :: :: hex {{ com bit vector constant, C-style }} {{ com hex and bin are constant bit vectors, C-style }} | bin :: :: bin {{ com bit vector constant, C-style }} +% Should undefined be of type bit[alpha] or alpha[beta] or just alpha? + | undefined :: :: undef {{ com constant representing undefined values }} | string :: :: string {{ com string constant }} semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::= {{ phantom }} diff --git a/language/l2_parse.ott b/language/l2_parse.ott index e06752a0..ab8d5d80 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -337,6 +337,7 @@ lit :: 'L_' ::= | hex :: :: hex {{ com bit vector constant, C-style }} {{ com hex and bin are constant bit vectors, C-style }} | bin :: :: bin {{ com bit vector constant, C-style }} + | undefined :: :: undef {{ com undefined value }} | string :: :: string {{ com string constant }} semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::= {{ phantom }} @@ -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) |