fix inlogic explorer (#1266)

* fix inlogic explorer

* change default of reg_alloc (absence case)

* make eror syntactically obvious

Author: tanyongkiam

compiler/backend/cv_compute/backend_asmScript.sml

@@ -573,7 +573,8 @@ Definition to_bvl_all_def:
            call_state := (g,aux)|> in
     let init_stubs = toAList (init_code c1.max_app) in
     let init_globs =
-            [(num_stubs c1.max_app − 1,0,
+            [(num_stubs c1.max_app − 2, 2, force_thunk_code);
+             (num_stubs c1.max_app − 1, 0,
               init_globals c1.max_app (num_stubs c1.max_app + c1.start))] in
     let comp_progs = clos_to_bvl$compile_prog c1.max_app prog in
     let prog' = init_stubs ++ init_globs ++ comp_progs in
@@ -651,7 +652,7 @@ Definition to_word_all_def:
               ((name_num,arg_count,
                remove_must_terminate
                  (case word_alloc_inlogic asm_conf prog col_opt of
-                  | NONE => Skip
+                  | NONE => FFI "reg alloc fail" 0 0 0 0 (LN,LN)
                   | SOME x => x)))) (ZIP (p,n_oracles)) in
     let ps = ps ++ [(strlit "after word_alloc (and remove_must_terminate)",Word p names)] in
     let c = c with inc_word_to_word_conf updated_by (λc. c with col_oracle := col) in

compiler/backend/reg_alloc/reg_allocScript.sml

@@ -1220,7 +1220,7 @@ End
 
 Definition sp_default_def:
   sp_default t i =
-  (case lookup i t of NONE => if is_phy_var i then i DIV 2 else i | SOME x => x)
+  (case lookup i t of NONE => if is_phy_var i then i DIV 2 else 0 | SOME x => x)
 End
 
 Definition extend_graph_def:

compiler/backend/word_allocScript.sml

@@ -1417,7 +1417,7 @@ End
 (*Extract a colouring function from the generated sptree*)
 Definition total_colour_def:
   total_colour col x =
-    dtcase lookup x col of NONE => if is_phy_var x then x else 2*x | SOME x => 2*x
+    dtcase lookup x col of NONE => if is_phy_var x then x else 0 | SOME x => 2*x
 End
 
 Theorem total_colour_alt:

unverified/reg_alloc/reg_alloc.sml

@@ -234,7 +234,7 @@ structure reg_alloc = struct
       case  (lookup_1 v2 v3)
       of  NONE =>  (if  (is_phy_var v2)
       then  (v2 div 2)
-      else  v2)
+      else  0)
       |   SOME(v1) =>  v1);
   fun  extract_tag v2 =
     case  v2