diff options
| -rw-r--r-- | cfrontend/C2C.ml | 11 | ||||
| -rw-r--r-- | common/Switchaux.ml | 35 |
2 files changed, 42 insertions, 4 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 702fcf2..b8586e0 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -771,7 +771,8 @@ let rec convertStmt ploc env s = if init.sdesc <> C.Sskip then warning "ignored code at beginning of 'switch'"; let te = convertExpr env e in - add_lineno ploc s.sloc (Sswitch(te, convertSwitch s.sloc env cases)) + add_lineno ploc s.sloc + (Sswitch(te, convertSwitch s.sloc env (is_longlong env e.etyp) cases)) | C.Slabeled(C.Slabel lbl, s1) -> add_lineno ploc s.sloc (Slabel(intern_string lbl, convertStmt s.sloc env s1)) @@ -795,7 +796,7 @@ let rec convertStmt ploc env s = add_lineno ploc s.sloc (Sdo (Ebuiltin (EF_inline_asm (intern_string txt), Tnil, Enil, Tvoid))) -and convertSwitch ploc env = function +and convertSwitch ploc env is_64 = function | [] -> LSnil | (lbl, s) :: rem -> @@ -808,9 +809,11 @@ and convertSwitch ploc env = function match Ceval.integer_expr env e with | None -> unsupported "'case' label is not a compile-time integer"; None - | Some v -> Some (Z.of_uint64 v) + | Some v -> Some (if is_64 + then Z.of_uint64 v + else Z.of_uint32 (Int64.to_int32 v)) in - LScons(lbl', convertStmt ploc env s, convertSwitch s.sloc env rem) + LScons(lbl', convertStmt ploc env s, convertSwitch s.sloc env is_64 rem) (** Function definitions *) diff --git a/common/Switchaux.ml b/common/Switchaux.ml index 15480ae..39b484c 100644 --- a/common/Switchaux.ml +++ b/common/Switchaux.ml @@ -96,4 +96,39 @@ let compile_switch modulus default table = else compile_switch_as_tree modulus default tbl end +(* For debugging *) +(** +open Format +let print_table p (tbl, dfl) = + fprintf p "@[<v 0>"; + List.iter + (fun (key, act) -> fprintf p "%s -> %d@ " (Z.to_string key) (Nat.to_int act)) + tbl; + fprintf p "_ -> %d@]" (Nat.to_int dfl) + +let rec print_jumptable p = function + | [] -> fprintf p "<empty>" + | [n] -> fprintf p "%d" (Nat.to_int n) + | n::ns -> fprintf p "%d %a" (Nat.to_int n) print_jumptable ns + +let rec print_tree p = function + | CTaction n -> fprintf p "action %d" (Nat.to_int n) + | CTifeq(key, act, t) -> + fprintf p "@[<v 2>if (x == %s)@ action %d@;<0 -2>else@ %a@]" + (Z.to_string key) (Nat.to_int act) print_tree t + | CTiflt(key, t1, t2) -> + fprintf p "@[<v 2>if (x <u %s)@ %a@;<0 -2>else@ %a@]" + (Z.to_string key) print_tree t1 print_tree t2 + | CTjumptable(ofs, sz, acts,t) -> + fprintf p "@[<v 2>if (x - %s <u %s)@ jumptable %a@;<0 -2>else@ %a@]" + (Z.to_string ofs) (Z.to_string sz) + print_jumptable acts print_tree t + +let compile_switch modulus default table = + let t = compile_switch modulus default table in + printf "@[<v 0>-------------@ "; + printf "Initial problem:@ %a@ " print_table (table, default); + printf "Decision tree:@ %a@ @]@." print_tree t; + t +**) |