type check

Cimp.ml

@@ -15,6 +15,8 @@ module Vm_Ex = Vm_ex__Vm_Ex
 module Imp_Ex = Imp_ex__Imp_Ex
 module State = State__State
 
+module Imp = Imp__Imp
+
 let () =
 
   cmd; (* parse command line options and put into opt *)
@@ -32,13 +34,17 @@ let () =
       let lexbuf = Lexing.from_channel inBuffer in
       lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = opt.infile };
       try
-        let prog = Parser.prog Lexer.lex lexbuf in
+        let p = Parser.prog Lexer.lex lexbuf in
+        (* p_stdout ("Decl:" ^ nl ^ T_Dump.of_prog p); *)
+
+        let com = T_Check.tc_prog inBuffer p in
+
         if opt.d_ast then
-          p_stderr ("Raw AST : \n" ^ of_com prog ^ nl);
+          p_stderr ("Raw AST:" ^ nl ^ Dump.of_com com ^ nl);
         if opt.d_past then
-          p_stderr ("Pretty AST: \n" ^ pretty_of_com 0 prog ^ nl);
+          p_stderr ("Pretty AST:" ^ nl ^ Dump.pretty_of_com 0 com ^ nl);
 
-        let code = Compile.compile_program prog in
+        let code = Compile.compile_program com in
         if opt.d_code then
           p_stderr ("Raw Code : \n" ^ of_code false code ^ nl);
         if opt.d_pcode then
@@ -50,7 +56,7 @@ let () =
         if opt.imp_ex then (
           try
             p_stdout ("Execute : imp_ex" );
-            let st_end = Imp_Ex.ceval_ex st_0 prog in
+            let st_end = Imp_Ex.ceval_ex st_0 com in
             p_stdout ("ceval_ex" ^ nl ^ Env.to_string st_end ^ nl);
           with
           | _ -> p_stdout "ceval : Exited with an error\n";
@@ -73,7 +79,9 @@ let () =
 
       with
       | Lexer.SyntaxError msg -> raise (CompilerError ("Syntax error. " ^ msg ^ parse_err_msg lexbuf));
-      | Parser.Error -> raise (CompilerError ("Parser error." ^ parse_err_msg lexbuf));
+      | Parser.Error -> 
+        raise (CompilerError ("Parser error." ^ parse_err_msg lexbuf)); 
+        (* raise (CompilerError ("Parser error.")); *)
   with
   | CompilerError msg -> p_stderr msg;
   | Failure msg -> p_stderr ("Failure (internal error): " ^ msg);

Common.ml

@@ -20,6 +20,7 @@ let ecit  = "\'"
 
 
 (* Error handling *)
+exception TypeError of string
 exception CompilerError of string
 exception UnMatched
 

Lexer.mll

@@ -26,6 +26,7 @@ let digits  = ['0'-'9']+
 
 (* lexing rules *)
 rule lex = parse
+
   | "IF"                 { IF }
   | "THEN"               { THEN }
   | "ELSE"               { ELSE }
@@ -41,8 +42,13 @@ rule lex = parse
   | "="                  { BEQ }
   | "<="                 { BLE }
 
+  | "SINT"               { SINT }
+  | "UINT32"             { UINT32 }
+
   | ';'                  { SC }
+  | ':'                  { C }
   | ":="                 { ASSIGN }
+  
   | '+'                  { PLUS }
   | "+u"                 { PLUSU }
   | '-'                  { MINUS }
@@ -56,6 +62,7 @@ rule lex = parse
   | "(*"                 { set_info lexbuf; comments 0 lexbuf } (* nested comment *)
   | '('                  { LP }                                 (* must come after comment *)
   | ')'                  { RP }
+  
   | eof                  { EOF }
   | _                    { raise (SyntaxError("Unknown Symbol.")) }
 

Parser.mly

@@ -7,11 +7,21 @@
 %token <int> INTVAL
 %token IF THEN ELSE END WHILE DO DONE
 %token TRUE FALSE AND NOT BEQ BLE
-%token SC LP RP ASSIGN PLUS PLUSU MINUS
+%token SINT UINT32
+
+%token SC C LP RP 
+%token ASSIGN
+%token PLUS PLUSU MINUS
 %token EOF
 
+(* precedence and associativity according to C/Java/Rust? *)
+%left SC
+%left AND
+%left MINUS, PLUS, PLUSU
+%left NOT
+
 %{
-  open Imp__Imp
+  open T_Imp
   open Common
   open Env
   open State__State
@@ -19,34 +29,51 @@
 
 %start prog
 
-%type <Imp__Imp.com> prog
+%type <T_Imp.prog> prog
 
 %%
-
 prog:
-  | com EOF                        { $1 }
+  | decl_span  SC com_span EOF        { Prog ($1, $3) } 
 
+decl_span:
+  | decl                              { ($1, ($startofs, $endofs)) }  
+decl:
+  | decl_span SC decl_span            { Dseq ($1, $3) } 
+  | ID C primtype                     { Ddecl ($1, $3) }
+
+primtype:
+  | SINT                              { Tsint }
+  | UINT32                            { Tuint32 }
+
+com_span:
+  | com                               { ($1, ($startofs, $endofs)) }
 com:
-  | com SC com                     { Cseq ($1, $3) }
-  | ID ASSIGN aexpr                { Cassign ($1, $3) }
-  | IF bexpr THEN com ELSE com END { Cif ($2, $4, $6) }
-  | IF bexpr THEN com END          { Cif ($2, $4, Cskip) }
-  | WHILE bexpr DO com DONE        { Cwhile ($2, $4) }
+  | com_span SC com_span              { Cseq ($1, $3) }
+  | ID ASSIGN aexpr_span              { Cassign ($1, $3) }
+  | IF bexpr_span THEN com_span 
+    ELSE com_span END                 { Cif ($2, $4, $6) }
+  | IF bexpr_span THEN com_span END   { Cif ($2, $4, (Cskip, (0, 0))) }
+  | WHILE bexpr_span DO com_span DONE { Cwhile ($2, $4) }
 
+bexpr_span:
+  | bexpr                             { ($1, ($startofs, $endofs)) }
 bexpr:
   | LP bexpr RP                       { $2 }
   | TRUE                              { Btrue }
   | FALSE                             { Bfalse }
-  | bexpr AND bexpr                { Band ($1, $3) }
-  | NOT bexpr                      { Bnot ($2) }
-  | aexpr BEQ aexpr                { Beq ($1, $3) }
-  | aexpr BLE aexpr                { Ble ($1, $3) }
+  | bexpr_span AND bexpr_span         { Band ($1, $3) }
+  | NOT bexpr_span                    { Bnot ($2) }
+  | aexpr_span BEQ aexpr_span         { Beq ($1, $3) }
+  | aexpr_span BLE aexpr_span         { Ble ($1, $3) }
+
+aexpr_span:                        
+  | aexpr                             { ($1, ($startofs, $endofs)) }
 
 aexpr:
   | LP aexpr RP                       { $2 } 
   | INTVAL                            { Anum (Z.of_int $1) }
   | ID                                { Avar $1 }
-  | aexpr PLUS aexpr               { Aadd ($1, $3) }
-  | aexpr PLUSU aexpr              { Aaddu ($1, $3) }
-  | aexpr MINUS aexpr              { Asub ($1, $3) }
+  | aexpr_span PLUS aexpr_span        { Aadd ($1, $3) }
+  | aexpr_span PLUSU aexpr_span       { Aaddu ($1, $3) }
+  | aexpr_span MINUS aexpr_span       { Asub ($1, $3) }
 

T_Check.ml

+(* Copyright Per Lindgren 2016-2018, see the file "LICENSE" *)
+(* for the full license governing this code.                *)
+
+(* type checker *)
+open T_Imp
+open T_Dump
+open Common
+open State__State
+
+
+module Imp = Imp__Imp
+
+let of_span inb (start, stop) = 
+  let _ = seek_in inb start in
+  let s = really_input_string inb (stop - start) in
+  "<" ^ string_of_int start ^ ".." ^ string_of_int stop ^ "> " ^ s
+
+let unique_id chan (id1, (t1, s1)) (id2, (t2, s2)) = 
+  if id1 = id2 then 
+    raise (CompilerError("Dupclicate variable definition: " ^
+                         of_span chan s1 ^ " already declared at " ^  of_span chan s2)) 
+  else ()
+
+let rec idt_acc ch sp acc = function 
+  | Dseq (d1, d2) ->  (idt_acc_span ch (idt_acc_span ch acc d1) d2) 
+  | Ddecl (id, t) -> List.iter (unique_id ch (id, (t, sp))) acc;
+    (id, (t, sp)) :: acc
+
+and idt_acc_span c acc (d, s) = idt_acc c s acc d
+
+let of_idt ch (id, (t,s)) =
+  of_id id ^ ":" ^ of_types t ^ of_span ch s
+
+
+let tc_unify ch t1 s1 t2 s2 : types =
+  match t1, t2 with
+  | Tsint,    Tsint     -> Tsint
+  | Tuint32,  Tuint32   -> Tuint32
+  | Tint,     t         -> t
+  | t,        Tint      -> t
+  | _,        _         ->
+    raise (TypeError(
+        "Type error: " ^ 
+        of_span ch s1 ^ " : " ^ of_types t1 ^ ", does not match " ^ 
+        of_span ch s2 ^ " : " ^ of_types t2 ))
+
+let get_id_type itl (id : id) : types * span =
+  try
+    List.assoc id itl
+  with 
+    _ -> raise (TypeError("Undeclared identifier: " ^ Dump.pretty_of_id id))
+
+let rec tc_aexpr ch itl (a, span) : Imp.aexpr * types =  
+  (* try *)
+  match a with
+  | Anum n -> (Imp.Anum n, Tint)
+  | Avar id -> 
+    let (t, _ ) = get_id_type itl id in
+    (Imp.Avar id, t)
+  | Aadd ((a1, a1_span), (a2, a2_span)) -> 
+
+    (* type check a1 against Tsint *)
+    let (ai1, t1) = tc_aexpr ch itl (a1, a1_span) in
+    let _ = tc_unify ch Tsint (0, 0) t1 a1_span in
+
+    (* type check a2 against Tsint *)
+    let (ai2, t2) = tc_aexpr ch itl (a2, a2_span) in
+    let _ = tc_unify ch Tsint (0, 0) t2 a2_span in
+
+    (Imp.Aadd(ai1, ai2), t1) 
+  | Aaddu ((a1, a1_span), (a2, a2_span)) -> 
+
+    (* type check a1 against Tuint32 *)
+    let (ai1, t1) = tc_aexpr ch itl (a1, a1_span) in
+    let _ = tc_unify ch Tuint32 (0, 0) t1 a1_span in
+
+    (* type check a2 against Tuint32 *)
+    let (ai2, t2) = tc_aexpr ch itl (a2, a2_span) in
+    let _ = tc_unify ch Tuint32 (0, 0) t2 a2_span in
+
+    (Imp.Aaddu(ai1, ai2), t1)
+
+  | Asub ((a1, a1_span), (a2, a2_span)) -> 
+
+    (* type check a1 against Tsint *)
+    let (ai1, t1) = tc_aexpr ch itl (a1, a1_span) in
+    let _ = tc_unify ch Tsint (0, 0) t1 a1_span in
+
+    (* type check a2 against Tsint *)
+    let (ai2, t2) = tc_aexpr ch itl (a2, a2_span) in
+    let _ = tc_unify ch Tsint (0, 0) t2 a2_span in
+
+    (Imp.Asub(ai1, ai2), t1)  
+(* with
+   | TypeError msg -> raise (TypeError (msg ^ nl ^ "in expression:" ^ of_span ch span )) *)
+
+let rec tc_bexpr ch itl (b, span) = 
+  try
+    match b with
+    | Btrue -> Imp.Btrue
+    | Bfalse -> Imp.Bfalse
+    | Band (b1, b2) -> Imp.Band(tc_bexpr ch itl b1,tc_bexpr ch itl b2)
+    | Bnot b -> Imp.Bnot(tc_bexpr ch itl b)
+    | Beq ((a1, a1_span),(a2, a2_span)) -> 
+      let (a1, t1) = tc_aexpr ch itl (a1, a1_span) in
+      let (a2, t2) = tc_aexpr ch itl (a2, a2_span) in
+      let _ = tc_unify ch t1 a1_span t2 a2_span in
+      Imp.Beq(a1, a2)
+    | Ble (a1, a2) -> Imp.Ble(imp_of_aexpr_span a1, imp_of_aexpr_span a2)
+  with
+  | TypeError msg -> raise (TypeError (msg ^ nl ^ "in expression:" ^ of_span ch span ))
+
+
+let rec tc_com ch itl span com = 
+  try 
+    match com with
+    | Cseq (c1, c2) -> Imp.Cseq(tc_com_span ch itl c1, tc_com_span ch itl c2)
+    | Cassign (id, a) ->
+      let (_, a_span) = a in
+      let (a, ta) = tc_aexpr ch itl a in
+      let (tid, tid_span) = get_id_type itl id in
+      let _ = tc_unify ch ta a_span tid tid_span in 
+      Imp.Cassign (id, a)
+    | Cif (b, c1, c2)  -> Imp.Cif(tc_bexpr ch itl b, tc_com_span ch itl c1, tc_com_span ch itl c2)
+    | Cwhile (b, c) -> Imp.Cwhile(tc_bexpr ch itl b, tc_com_span ch itl c)
+    | Cskip -> Imp.Cskip
+  with
+  | TypeError msg -> raise (CompilerError (msg ^ nl ^ "in command: " ^ of_span ch span ))
+and
+  tc_com_span ch itl (com, span)  = tc_com ch itl span com
+
+let tc_prog ch (Prog (decl, com)) = 
+  let itl = idt_acc_span ch [] decl in
+  tc_com_span ch itl com 
+

T_Dump.ml

+(* Copyright Per Lindgren 2016-2018, see the file "LICENSE" *)
+(* for the full license governing this code.                *)
+
+open State__State
+open Vm__Vm
+open Env
+open Common
+open T_Imp
+
+(* AST dump of T_Imp *)
+
+let of_types = function 
+  | Tsint   -> "SINT"
+  | Tuint32 -> "UINT32"
+  | Tint    -> "INT"
+
+let of_id = function
+  | Id i -> "Id #" ^ Z.to_string i
+
+let rec of_aexpr = function
+  | Anum v          -> "Anum " ^ Z.to_string v
+  | Avar id         -> "Avar " ^ of_id id
+  | Aadd (e1, e2)   -> "Aadd (" ^ of_aexpr_span e1 ^ ") (" ^ of_aexpr_span e2 ^ ")"
+  | Aaddu (e1, e2)  -> "Aaddu (" ^ of_aexpr_span e1 ^ ") (" ^ of_aexpr_span e2 ^")"
+  | Asub (e1, e2)   -> "Asub (" ^ of_aexpr_span e1 ^ ") (" ^ of_aexpr_span e2 ^")"
+and of_aexpr_span (e, (start, stop)) = 
+  "< (" ^ string_of_int start ^ ", " ^ string_of_int stop ^ 
+  ") " ^ of_aexpr e ^ ">"
+
+let rec of_bexpr = function
+  | Btrue           -> "Btrue"
+  | Bfalse          -> "Bfalse"
+  | Band (b1, b2)   -> "Band (" ^ of_bexpr_span b1 ^ ") (" ^ of_bexpr_span b2 ^ ")"
+  | Bnot b          -> "Bnot (" ^ of_bexpr_span b ^ ")"
+  | Beq (e1, e2)    -> "Beq (" ^ of_aexpr_span e1 ^ ") (" ^ of_aexpr_span e2 ^ ")"
+  | Ble (e1, e2)    -> "Ble (" ^ of_aexpr_span e1 ^ ") (" ^ of_aexpr_span e2 ^ ")"
+and of_bexpr_span (e, s) = of_bexpr e
+
+let rec of_com = function
+  | Cskip           -> "Cskip"
+  | Cassign (id, a) -> "Cassign " ^ of_id id ^ " " ^ of_aexpr_span a
+  | Cseq (c1, c2)   -> "Cseq (" ^ of_com_span c1 ^ ") (" ^ of_com_span c2 ^ ")"
+  | Cif (b, c1, c2) -> "Cif (" ^ of_bexpr_span b ^ ") (" ^ of_com_span c1 ^ " " ^ of_com_span c2 ^ ")"
+  | Cwhile (b, c)   -> "Cwhile (" ^ of_bexpr_span b ^ ") (" ^ of_com_span c ^ ")"
+and of_com_span (c, (start, stop)) = 
+  "< (" ^ string_of_int start ^ ", " ^ string_of_int stop ^ 
+  ") " ^ of_com c ^ ">"
+
+let rec of_decl = function
+  | Dseq (d1, d2) -> "Dseq (" ^ of_decl_span d1 ^ ", " ^ of_decl_span d2 ^ ")"
+  | Ddecl (id, t) -> "Ddecl (" ^ of_id id ^ ", " ^ of_types t ^ ")" 
+and of_decl_span (d,_) = of_decl d
+
+let of_prog = function
+  | Prog (d, c) -> of_decl_span d ^ of_com_span c
+

T_Imp.ml

+
+module Imp = Imp__Imp 
+
+type types =
+  | Tsint
+  | Tuint32
+  | Tint (* int litterals can be coersed to both Tsint and Tuint32 *)
+
+type span = int * int
+
+type aexpr =
+  | Anum of (Z.t)
+  | Avar of State__State.id
+  | Aadd of aexpr_span * aexpr_span
+  | Aaddu of aexpr_span * aexpr_span
+  | Asub of aexpr_span * aexpr_span
+and
+  aexpr_span = aexpr * span
+
+type bexpr =
+  | Btrue
+  | Bfalse
+  | Band of bexpr_span * bexpr_span
+  | Bnot of bexpr_span
+  | Beq of aexpr_span * aexpr_span
+  | Ble of aexpr_span * aexpr_span
+and bexpr_span = bexpr * span
+
+type com =
+  | Cskip
+  | Cseq of com_span * com_span
+  | Cassign of State__State.id * aexpr_span
+  | Cif of bexpr_span * com_span * com_span
+  | Cwhile of bexpr_span * com_span
+and com_span = com * span
+
+type decl =
+  | Dseq of decl_span * decl_span
+  | Ddecl of State__State.id * types 
+and decl_span = decl * span
+
+type prog = Prog of decl_span * com_span
+
+(* Convert to Imp *)
+let rec imp_of_aexpr = function
+  | Anum n -> Imp.Anum n
+  | Avar id -> Imp.Avar id
+  | Aadd (a1, a2) -> Imp.Aadd(imp_of_aexpr_span a1, imp_of_aexpr_span a2) 
+  | Aaddu (a1, a2) -> Imp.Aaddu(imp_of_aexpr_span a1, imp_of_aexpr_span a2) 
+  | Asub (a1, a2) -> Imp.Asub(imp_of_aexpr_span a1, imp_of_aexpr_span a2) 
+and
+  imp_of_aexpr_span (a, _) = imp_of_aexpr a
+
+let rec imp_of_bexpr = function
+  | Btrue -> Imp.Btrue
+  | Bfalse -> Imp.Bfalse
+  | Band (b1, b2) -> Imp.Band(imp_of_bexpr_span b1,imp_of_bexpr_span b2)
+  | Bnot b -> Imp.Bnot(imp_of_bexpr_span b)
+  | Beq (a1, a2) -> Imp.Beq(imp_of_aexpr_span a1, imp_of_aexpr_span a2)
+  | Ble (a1, a2) -> Imp.Ble(imp_of_aexpr_span a1, imp_of_aexpr_span a2)
+and
+  imp_of_bexpr_span (b, _) = imp_of_bexpr b
+
+let rec imp_of_com = function
+  | Cskip -> Imp.Cskip
+  | Cseq (c1, c2) -> Imp.Cseq(imp_of_com_span c1,imp_of_com_span c2)
+  | Cassign (id, a) -> Imp.Cassign (id, imp_of_aexpr_span a)
+  | Cif (b, c1, c2)  -> Imp.Cif(imp_of_bexpr_span b, imp_of_com_span c1, imp_of_com_span c2)
+  | Cwhile (b, c) -> Imp.Cwhile(imp_of_bexpr_span b, imp_of_com_span c)
+and
+  imp_of_com_span (c, _) = imp_of_com c
+
+
+
+
+