Lower a fall-through-free switch as a chain of conditionals - #234
Draft
nikswamy wants to merge 2 commits into
Draft
Lower a fall-through-free switch as a chain of conditionals#234nikswamy wants to merge 2 commits into
nikswamy wants to merge 2 commits into
Conversation
Consecutive labels nest in clang: `case 2: case 3: default: r = 30;` arrives as CaseStmt(2, CaseStmt(3, DefaultStmt(r = 30))), not as three siblings. The group builder peeled only the CaseStmt chain, so the DefaultStmt was pushed into the arm's body, where statement translation rejected it as unsupported. Peel the whole label chain, in either order, and mark the group default. Its explicit case values are then dropped, because an arm reached by anything gains nothing from also testing for 2 or 3, and emitting the test would leave a redundant condition in the generated Pulse. Both emitters already keyed off the group's default flag, so the terminal-break match encoding and the general fall-through encoding both follow. The regression covers a default written after the cases it shares an arm with, the same without a terminal break, one written before them, and the annotated form that reaches the match encoding. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit 12f46ba)
The general switch encoding threads `hit` and `brk` flags to model fall-through, so every arm executes under `!brk && (hit || scrut == v)` -- a compound condition over mutable state. When the arms differ in what they own, which is the shape of any dispatch that writes an output, the join is phrased in terms of the scrutinee while the guards are phrased in terms of the flags, and the two never meet. Binding a guard to a `let` fixes the first test but not the chained one, because `brk` becomes `match cond_a with true -> true | false -> false`. A switch with no fall-through and a `default` is an if/else chain, so say so: test the scrutinee directly and each branch condition is the one the join is phrased in. The emitted Pulse is legible besides. An explicit switch postcondition still takes the existing match form, which needs one -- Pulse cannot infer a postcondition for a non-tail conditional. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit 59600ae)
Contributor
|
!diff |
Generated F* output diffEffect of this pull request on the F* code SummaryFull diff: full diff artifact Diffdiff --git base/switch_stmt/Func_accumulate_with_fallthrough.fst head/switch_stmt/Func_accumulate_with_fallthrough.fst
index 383d025..704317b 100644
--- base/switch_stmt/Func_accumulate_with_fallthrough.fst
+++ head/switch_stmt/Func_accumulate_with_fallthrough.fst
@@ -15,21 +15,21 @@ divergent fn func_accumulate_with_fallthrough (var_x: Typedef_int32_t.ty_int32_t
let mut var_x = var_x;
let mut var_result : Typedef_int32_t.ty_int32_t;
var_result := 0l;
- let var___switch_scrut_2 : Typedef_int32_t.ty_int32_t = (!var_x);
- let mut var___switch_hit_2 : bool;
- var___switch_hit_2 := false;
- let mut var___switch_brk_2 : bool;
- var___switch_brk_2 := false;
- if (((not (!var___switch_brk_2)) &&
- ((!var___switch_hit_2) || (false || (var___switch_scrut_2 = 0l))))) {
- var___switch_hit_2 := true;
+ let var___switch_scrut_6 : Typedef_int32_t.ty_int32_t = (!var_x);
+ let mut var___switch_hit_6 : bool;
+ var___switch_hit_6 := false;
+ let mut var___switch_brk_6 : bool;
+ var___switch_brk_6 := false;
+ if (((not (!var___switch_brk_6)) &&
+ ((!var___switch_hit_6) || (false || (var___switch_scrut_6 = 0l))))) {
+ var___switch_hit_6 := true;
var_result := 10l;
} else {};
- if (((not (!var___switch_brk_2)) &&
- ((!var___switch_hit_2) || (false || (var___switch_scrut_2 = 1l))))) {
- var___switch_hit_2 := true;
+ if (((not (!var___switch_brk_6)) &&
+ ((!var___switch_hit_6) || (false || (var___switch_scrut_6 = 1l))))) {
+ var___switch_hit_6 := true;
var_result := ((!var_result) `Int32.add` 1l);
- var___switch_brk_2 := true;
+ var___switch_brk_6 := true;
} else {};
return (!var_result);
}
\ No newline at end of file
diff --git base/switch_stmt/Func_call_in_case.fst head/switch_stmt/Func_call_in_case.fst
index 45bbb9a..1e9c82a 100644
--- base/switch_stmt/Func_call_in_case.fst
+++ head/switch_stmt/Func_call_in_case.fst
@@ -12,9 +12,9 @@ divergent fn func_call_in_case (var_x: Typedef_int32_t.ty_int32_t)
let mut var_x = var_x;
let mut var_result : Typedef_int32_t.ty_int32_t;
var_result := 0l;
- let var___switch_scrut_3 : Typedef_int32_t.ty_int32_t = (!var_x);
+ let var___switch_scrut_7 : Typedef_int32_t.ty_int32_t = (!var_x);
{
- match (var___switch_scrut_3) {
+ match (var___switch_scrut_7) {
0l -> {
var_result := 1l;
}
@@ -24,6 +24,6 @@ divergent fn func_call_in_case (var_x: Typedef_int32_t.ty_int32_t)
};
}
ensures ((live var_x) ** (live var_result))
- label __pal_match_join_0:;
+ label __pal_match_join_1:;
return (!var_result);
}
\ No newline at end of file
diff --git base/switch_stmt/Func_classify.fst head/switch_stmt/Func_classify.fst
index 8d12994..a947174 100644
--- base/switch_stmt/Func_classify.fst
+++ head/switch_stmt/Func_classify.fst
@@ -20,27 +20,14 @@ divergent fn func_classify (var_x: Typedef_int32_t.ty_int32_t)
let mut var_r : Typedef_int32_t.ty_int32_t;
var_r := 0l;
let var___switch_scrut_1 : Typedef_int32_t.ty_int32_t = (!var_x);
- let mut var___switch_hit_1 : bool;
- var___switch_hit_1 := false;
- let mut var___switch_brk_1 : bool;
- var___switch_brk_1 := false;
- if (((not (!var___switch_brk_1)) &&
- ((!var___switch_hit_1) || (false || (var___switch_scrut_1 = 0l))))) {
- var___switch_hit_1 := true;
+ if ((var___switch_scrut_1 = 0l)) {
var_r := 10l;
- var___switch_brk_1 := true;
- } else {};
- if (((not (!var___switch_brk_1)) &&
- ((!var___switch_hit_1) ||
- ((false || (var___switch_scrut_1 = 1l)) || (var___switch_scrut_1 = 2l))))) {
- var___switch_hit_1 := true;
- var_r := 20l;
- var___switch_brk_1 := true;
- } else {};
- if ((not (!var___switch_brk_1))) {
- var___switch_hit_1 := true;
- var_r := 30l;
- var___switch_brk_1 := true;
- } else {};
+ } else {
+ if (((var___switch_scrut_1 = 1l) || (var___switch_scrut_1 = 2l))) {
+ var_r := 20l;
+ } else {
+ var_r := 30l;
+ };
+ };
return (!var_r);
}
\ No newline at end of file
diff --git base/switch_stmt/Func_classify_with_returns.fst head/switch_stmt/Func_classify_with_returns.fst
index 3b1567d..dbeccba 100644
--- base/switch_stmt/Func_classify_with_returns.fst
+++ head/switch_stmt/Func_classify_with_returns.fst
@@ -10,16 +10,16 @@ divergent fn func_classify_with_returns (var_x: Typedef_int32_t.ty_int32_t)
ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
{
let mut var_x = var_x;
- let var___switch_scrut_4 : Typedef_int32_t.ty_int32_t = (!var_x);
- let mut var___switch_hit_4 : bool;
- var___switch_hit_4 := false;
- let mut var___switch_brk_4 : bool;
- var___switch_brk_4 := false;
- if (((not (!var___switch_brk_4)) &&
- ((!var___switch_hit_4) || (false || (var___switch_scrut_4 = 0l))))) {
- var___switch_hit_4 := true;
+ let var___switch_scrut_8 : Typedef_int32_t.ty_int32_t = (!var_x);
+ let mut var___switch_hit_8 : bool;
+ var___switch_hit_8 := false;
+ let mut var___switch_brk_8 : bool;
+ var___switch_brk_8 := false;
+ if (((not (!var___switch_brk_8)) &&
+ ((!var___switch_hit_8) || (false || (var___switch_scrut_8 = 0l))))) {
+ var___switch_hit_8 := true;
return 10l;
} else {};
- var___switch_hit_4 := true;
+ var___switch_hit_8 := true;
return 20l;
}
\ No newline at end of file
diff --git base/switch_stmt/Func_day_type.fst head/switch_stmt/Func_day_type.fst
index 3a0abdb..8c55998 100644
--- base/switch_stmt/Func_day_type.fst
+++ head/switch_stmt/Func_day_type.fst
@@ -22,26 +22,15 @@ divergent fn func_day_type (var_day: Typedef_int32_t.ty_int32_t)
let mut var_result : Typedef_int32_t.ty_int32_t;
var_result := 0l;
let var___switch_scrut_0 : Typedef_int32_t.ty_int32_t = (!var_day);
- let mut var___switch_hit_0 : bool;
- var___switch_hit_0 := false;
- let mut var___switch_brk_0 : bool;
- var___switch_brk_0 := false;
- if (((not (!var___switch_brk_0)) &&
- ((!var___switch_hit_0) ||
- (((((false || (var___switch_scrut_0 = 1l)) || (var___switch_scrut_0 = 2l)) ||
- (var___switch_scrut_0 = 3l))
- ||
- (var___switch_scrut_0 = 4l))
- ||
- (var___switch_scrut_0 = 5l))))) {
- var___switch_hit_0 := true;
+ if ((((((var___switch_scrut_0 = 1l) || (var___switch_scrut_0 = 2l)) ||
+ (var___switch_scrut_0 = 3l))
+ ||
+ (var___switch_scrut_0 = 4l))
+ ||
+ (var___switch_scrut_0 = 5l))) {
var_result := 1l;
- var___switch_brk_0 := true;
- } else {};
- if ((not (!var___switch_brk_0))) {
- var___switch_hit_0 := true;
+ } else {
var_result := 0l;
- var___switch_brk_0 := true;
- } else {};
+ };
return (!var_result);
}
\ No newline at end of file
diff --git head/switch_stmt/Func_default_after_cases.fst head/switch_stmt/Func_default_after_cases.fst
new file mode 100644
index 0000000..399e3b5
--- /dev/null
+++ head/switch_stmt/Func_default_after_cases.fst
@@ -0,0 +1,32 @@
+module Func_default_after_cases
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_default_after_cases (var_x: Typedef_int32_t.ty_int32_t)
+ requires ((Typedef_int32_t.ty_int32_t__pred var_x 1.0R))
+ returns return_1 : Typedef_int32_t.ty_int32_t
+ ensures ((Typedef_int32_t.ty_int32_t__pred var_x 1.0R))
+ ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
+ ensures (with_pure (((id #int (Int32.v var_x)) = 0) ==> ((id #int (Int32.v return_1)) = 10)))
+ ensures (with_pure (((id #int (Int32.v var_x)) = 1) ==> ((id #int (Int32.v return_1)) = 20)))
+ ensures
+ (with_pure
+ (((not ((id #int (Int32.v var_x)) = 0)) && (not ((id #int (Int32.v var_x)) = 1))) ==>
+ ((id #int (Int32.v return_1)) = 30)))
+{
+ let mut var_x = var_x;
+ let mut var_r : Typedef_int32_t.ty_int32_t;
+ var_r := 0l;
+ let var___switch_scrut_2 : Typedef_int32_t.ty_int32_t = (!var_x);
+ if ((var___switch_scrut_2 = 0l)) {
+ var_r := 10l;
+ } else {
+ if ((var___switch_scrut_2 = 1l)) {
+ var_r := 20l;
+ } else {
+ var_r := 30l;
+ };
+ };
+ return (!var_r);
+}
\ No newline at end of file
diff --git head/switch_stmt/Func_default_after_cases.fsti head/switch_stmt/Func_default_after_cases.fsti
new file mode 100644
index 0000000..45131d7
--- /dev/null
+++ head/switch_stmt/Func_default_after_cases.fsti
@@ -0,0 +1,16 @@
+module Func_default_after_cases
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_default_after_cases (var_x: Typedef_int32_t.ty_int32_t)
+requires ((Typedef_int32_t.ty_int32_t__pred var_x 1.0R))
+returns return_1 : Typedef_int32_t.ty_int32_t
+ensures ((Typedef_int32_t.ty_int32_t__pred var_x 1.0R))
+ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
+ensures (with_pure (((id #int (Int32.v var_x)) = 0) ==> ((id #int (Int32.v return_1)) = 10)))
+ensures (with_pure (((id #int (Int32.v var_x)) = 1) ==> ((id #int (Int32.v return_1)) = 20)))
+ensures
+ (with_pure
+ (((not ((id #int (Int32.v var_x)) = 0)) && (not ((id #int (Int32.v var_x)) = 1))) ==>
+ ((id #int (Int32.v return_1)) = 30)))
\ No newline at end of file
diff --git head/switch_stmt/Func_default_after_cases_annotated.fst head/switch_stmt/Func_default_after_cases_annotated.fst
new file mode 100644
index 0000000..62fc7d8
--- /dev/null
+++ head/switch_stmt/Func_default_after_cases_annotated.fst
@@ -0,0 +1,31 @@
+module Func_default_after_cases_annotated
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_default_after_cases_annotated (var_x: Typedef_int32_t.ty_int32_t)
+ requires ((Typedef_int32_t.ty_int32_t__pred var_x 1.0R))
+ returns return_1 : Typedef_int32_t.ty_int32_t
+ ensures ((Typedef_int32_t.ty_int32_t__pred var_x 1.0R))
+ ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
+ ensures (with_pure (((id #int (Int32.v return_1)) = 10) || ((id #int (Int32.v return_1)) = 30)))
+{
+ let mut var_x = var_x;
+ let mut var_r : Typedef_int32_t.ty_int32_t;
+ var_r := 0l;
+ let var___switch_scrut_5 : Typedef_int32_t.ty_int32_t = (!var_x);
+ {
+ match (var___switch_scrut_5) {
+ 0l -> {
+ var_r := 10l;
+ }
+ _ -> {
+ var_r := 30l;
+ }
+ };
+ }
+ ensures (((live var_x) ** (live var_r)) **
+ (with_pure (((id #int (Int32.v (!var_r))) = 10) || ((id #int (Int32.v (!var_r))) = 30))))
+ label __pal_match_join_0:;
+ return (!var_r);
+}
\ No newline at end of file
diff --git head/switch_stmt/Func_default_after_cases_annotated.fsti head/switch_stmt/Func_default_after_cases_annotated.fsti
new file mode 100644
index 0000000..f310941
--- /dev/null
+++ head/switch_stmt/Func_default_after_cases_annotated.fsti
@@ -0,0 +1,11 @@
+module Func_default_after_cases_annotated
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_default_after_cases_annotated (var_x: Typedef_int32_t.ty_int32_t)
+requires ((Typedef_int32_t.ty_int32_t__pred var_x 1.0R))
+returns return_1 : Typedef_int32_t.ty_int32_t
+ensures ((Typedef_int32_t.ty_int32_t__pred var_x 1.0R))
+ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
+ensures (with_pure (((id #int (Int32.v return_1)) = 10) || ((id #int (Int32.v return_1)) = 30)))
\ No newline at end of file
diff --git head/switch_stmt/Func_default_after_cases_no_break.fst head/switch_stmt/Func_default_after_cases_no_break.fst
new file mode 100644
index 0000000..6042e2f
--- /dev/null
+++ head/switch_stmt/Func_default_after_cases_no_break.fst
@@ -0,0 +1,34 @@
+module Func_default_after_cases_no_break
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_default_after_cases_no_break (var_x: Typedef_int32_t.ty_int32_t)
+ requires ((Typedef_int32_t.ty_int32_t__pred var_x 1.0R))
+ returns return_1 : Typedef_int32_t.ty_int32_t
+ ensures ((Typedef_int32_t.ty_int32_t__pred var_x 1.0R))
+ ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
+ ensures (with_pure (((id #int (Int32.v var_x)) = 0) ==> ((id #int (Int32.v return_1)) = 10)))
+ ensures
+ (with_pure ((not ((id #int (Int32.v var_x)) = 0)) ==> ((id #int (Int32.v return_1)) = 30)))
+{
+ let mut var_x = var_x;
+ let mut var_r : Typedef_int32_t.ty_int32_t;
+ var_r := 0l;
+ let var___switch_scrut_3 : Typedef_int32_t.ty_int32_t = (!var_x);
+ let mut var___switch_hit_3 : bool;
+ var___switch_hit_3 := false;
+ let mut var___switch_brk_3 : bool;
+ var___switch_brk_3 := false;
+ if (((not (!var___switch_brk_3)) &&
+ ((!var___switch_hit_3) || (false || (var___switch_scrut_3 = 0l))))) {
+ var___switch_hit_3 := true;
+ var_r := 10l;
+ var___switch_brk_3 := true;
+ } else {};
+ if ((not (!var___switch_brk_3))) {
+ var___switch_hit_3 := true;
+ var_r := 30l;
+ } else {};
+ return (!var_r);
+}
\ No newline at end of file
diff --git head/switch_stmt/Func_default_after_cases_no_break.fsti head/switch_stmt/Func_default_after_cases_no_break.fsti
new file mode 100644
index 0000000..243bb00
--- /dev/null
+++ head/switch_stmt/Func_default_after_cases_no_break.fsti
@@ -0,0 +1,12 @@
+module Func_default_after_cases_no_break
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_default_after_cases_no_break (var_x: Typedef_int32_t.ty_int32_t)
+requires ((Typedef_int32_t.ty_int32_t__pred var_x 1.0R))
+returns return_1 : Typedef_int32_t.ty_int32_t
+ensures ((Typedef_int32_t.ty_int32_t__pred var_x 1.0R))
+ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
+ensures (with_pure (((id #int (Int32.v var_x)) = 0) ==> ((id #int (Int32.v return_1)) = 10)))
+ensures (with_pure ((not ((id #int (Int32.v var_x)) = 0)) ==> ((id #int (Int32.v return_1)) = 30)))
\ No newline at end of file
diff --git head/switch_stmt/Func_default_before_cases.fst head/switch_stmt/Func_default_before_cases.fst
new file mode 100644
index 0000000..78e1d96
--- /dev/null
+++ head/switch_stmt/Func_default_before_cases.fst
@@ -0,0 +1,25 @@
+module Func_default_before_cases
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_default_before_cases (var_x: Typedef_int32_t.ty_int32_t)
+ requires ((Typedef_int32_t.ty_int32_t__pred var_x 1.0R))
+ returns return_1 : Typedef_int32_t.ty_int32_t
+ ensures ((Typedef_int32_t.ty_int32_t__pred var_x 1.0R))
+ ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
+ ensures (with_pure (((id #int (Int32.v var_x)) = 1) ==> ((id #int (Int32.v return_1)) = 20)))
+ ensures
+ (with_pure ((not ((id #int (Int32.v var_x)) = 1)) ==> ((id #int (Int32.v return_1)) = 30)))
+{
+ let mut var_x = var_x;
+ let mut var_r : Typedef_int32_t.ty_int32_t;
+ var_r := 0l;
+ let var___switch_scrut_4 : Typedef_int32_t.ty_int32_t = (!var_x);
+ if ((var___switch_scrut_4 = 1l)) {
+ var_r := 20l;
+ } else {
+ var_r := 30l;
+ };
+ return (!var_r);
+}
\ No newline at end of file
diff --git head/switch_stmt/Func_default_before_cases.fsti head/switch_stmt/Func_default_before_cases.fsti
new file mode 100644
index 0000000..5578d49
--- /dev/null
+++ head/switch_stmt/Func_default_before_cases.fsti
@@ -0,0 +1,12 @@
+module Func_default_before_cases
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_default_before_cases (var_x: Typedef_int32_t.ty_int32_t)
+requires ((Typedef_int32_t.ty_int32_t__pred var_x 1.0R))
+returns return_1 : Typedef_int32_t.ty_int32_t
+ensures ((Typedef_int32_t.ty_int32_t__pred var_x 1.0R))
+ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
+ensures (with_pure (((id #int (Int32.v var_x)) = 1) ==> ((id #int (Int32.v return_1)) = 20)))
+ensures (with_pure ((not ((id #int (Int32.v var_x)) = 1)) ==> ((id #int (Int32.v return_1)) = 30)))
\ No newline at end of file
diff --git base/switch_stmt/Func_sparse_string_name.fst head/switch_stmt/Func_sparse_string_name.fst
index 486a4f1..2b365bd 100644
--- base/switch_stmt/Func_sparse_string_name.fst
+++ head/switch_stmt/Func_sparse_string_name.fst
@@ -14,14 +14,14 @@ divergent fn func_sparse_string_name
let mut var_fallback = var_fallback;
let mut var_name : (ref Int8.t);
var_name := (!var_fallback);
- let var___switch_scrut_11 : Typedef_int32_t.ty_int32_t = (!var_x);
- let mut var___switch_hit_11 : bool;
- var___switch_hit_11 := false;
- let mut var___switch_brk_11 : bool;
- var___switch_brk_11 := false;
- if (((not (!var___switch_brk_11)) &&
- ((!var___switch_hit_11) || (false || (var___switch_scrut_11 = 100l))))) {
- var___switch_hit_11 := true;
+ let var___switch_scrut_15 : Typedef_int32_t.ty_int32_t = (!var_x);
+ let mut var___switch_hit_15 : bool;
+ var___switch_hit_15 := false;
+ let mut var___switch_brk_15 : bool;
+ var___switch_brk_15 := false;
+ if (((not (!var___switch_brk_15)) &&
+ ((!var___switch_hit_15) || (false || (var___switch_scrut_15 = 100l))))) {
+ var___switch_hit_15 := true;
var_name :=
(Pulse.Lib.C.Array.array_literal_to_ref
(array_spec_of_list_with_len
@@ -36,12 +36,12 @@ divergent fn func_sparse_string_name
(Cons #Int8.t (Int8.int_to_t 0)
(Nil #Int8.t)))))))))
8));
- var___switch_brk_11 := true;
+ var___switch_brk_15 := true;
} else {};
- if (((not (!var___switch_brk_11)) &&
- ((!var___switch_hit_11) ||
- (false || (var___switch_scrut_11 = (Int32.sub Int32.zero 10l)))))) {
- var___switch_hit_11 := true;
+ if (((not (!var___switch_brk_15)) &&
+ ((!var___switch_hit_15) ||
+ (false || (var___switch_scrut_15 = (Int32.sub Int32.zero 10l)))))) {
+ var___switch_hit_15 := true;
var_name :=
(Pulse.Lib.C.Array.array_literal_to_ref
(array_spec_of_list_with_len
@@ -61,11 +61,11 @@ divergent fn func_sparse_string_name
(Cons #Int8.t (Int8.int_to_t 0)
(Nil #Int8.t))))))))))))))
13));
- var___switch_brk_11 := true;
+ var___switch_brk_15 := true;
} else {};
- if (((not (!var___switch_brk_11)) &&
- ((!var___switch_hit_11) || (false || (var___switch_scrut_11 = 7l))))) {
- var___switch_hit_11 := true;
+ if (((not (!var___switch_brk_15)) &&
+ ((!var___switch_hit_15) || (false || (var___switch_scrut_15 = 7l))))) {
+ var___switch_hit_15 := true;
var_name :=
(Pulse.Lib.C.Array.array_literal_to_ref
(array_spec_of_list_with_len
@@ -78,7 +78,7 @@ divergent fn func_sparse_string_name
(Cons #Int8.t (Int8.int_to_t 0)
(Nil #Int8.t)))))))
6));
- var___switch_brk_11 := true;
+ var___switch_brk_15 := true;
} else {};
return (!var_name);
}
\ No newline at end of file
diff --git base/switch_stmt/Func_sparse_unsorted.fst head/switch_stmt/Func_sparse_unsorted.fst
index 439e10e..627ac92 100644
--- base/switch_stmt/Func_sparse_unsorted.fst
+++ head/switch_stmt/Func_sparse_unsorted.fst
@@ -25,29 +25,29 @@ divergent fn func_sparse_unsorted (var_x: Typedef_int32_t.ty_int32_t)
let mut var_x = var_x;
let mut var_result : Typedef_int32_t.ty_int32_t;
var_result := 0l;
- let var___switch_scrut_5 : Typedef_int32_t.ty_int32_t = (!var_x);
- let mut var___switch_hit_5 : bool;
- var___switch_hit_5 := false;
- let mut var___switch_brk_5 : bool;
- var___switch_brk_5 := false;
- if (((not (!var___switch_brk_5)) &&
- ((!var___switch_hit_5) || (false || (var___switch_scrut_5 = 100l))))) {
- var___switch_hit_5 := true;
+ let var___switch_scrut_9 : Typedef_int32_t.ty_int32_t = (!var_x);
+ let mut var___switch_hit_9 : bool;
+ var___switch_hit_9 := false;
+ let mut var___switch_brk_9 : bool;
+ var___switch_brk_9 := false;
+ if (((not (!var___switch_brk_9)) &&
+ ((!var___switch_hit_9) || (false || (var___switch_scrut_9 = 100l))))) {
+ var___switch_hit_9 := true;
var_result := 3l;
- var___switch_brk_5 := true;
+ var___switch_brk_9 := true;
} else {};
- if (((not (!var___switch_brk_5)) &&
- ((!var___switch_hit_5) ||
- (false || (var___switch_scrut_5 = (Int32.sub Int32.zero 10l)))))) {
- var___switch_hit_5 := true;
+ if (((not (!var___switch_brk_9)) &&
+ ((!var___switch_hit_9) ||
+ (false || (var___switch_scrut_9 = (Int32.sub Int32.zero 10l)))))) {
+ var___switch_hit_9 := true;
var_result := 1l;
- var___switch_brk_5 := true;
+ var___switch_brk_9 := true;
} else {};
- if (((not (!var___switch_brk_5)) &&
- ((!var___switch_hit_5) || (false || (var___switch_scrut_5 = 7l))))) {
- var___switch_hit_5 := true;
+ if (((not (!var___switch_brk_9)) &&
+ ((!var___switch_hit_9) || (false || (var___switch_scrut_9 = 7l))))) {
+ var___switch_hit_9 := true;
var_result := 2l;
- var___switch_brk_5 := true;
+ var___switch_brk_9 := true;
} else {};
return (!var_result);
}
\ No newline at end of file
diff --git base/switch_stmt/Func_terminal_break_i32.fst head/switch_stmt/Func_terminal_break_i32.fst
index 1365a2f..c0a48ec 100644
--- base/switch_stmt/Func_terminal_break_i32.fst
+++ head/switch_stmt/Func_terminal_break_i32.fst
@@ -13,9 +13,9 @@ divergent fn func_terminal_break_i32 (var_x: Typedef_int32_t.ty_int32_t)
let mut var_x = var_x;
let mut var_result : Typedef_int32_t.ty_int32_t;
var_result := 0l;
- let var___switch_scrut_6 : Typedef_int32_t.ty_int32_t = (!var_x);
+ let var___switch_scrut_10 : Typedef_int32_t.ty_int32_t = (!var_x);
{
- match (var___switch_scrut_6) {
+ match (var___switch_scrut_10) {
-10l -> {
var_result := 1l;
}
@@ -28,6 +28,6 @@ divergent fn func_terminal_break_i32 (var_x: Typedef_int32_t.ty_int32_t)
ensures (((live var_x) ** (live var_result)) **
(with_pure
(((id #int (Int32.v (!var_result))) = 0) || ((id #int (Int32.v (!var_result))) = 1))))
- label __pal_match_join_1:;
+ label __pal_match_join_2:;
return (!var_result);
}
\ No newline at end of file
diff --git base/switch_stmt/Func_terminal_break_i64.fst head/switch_stmt/Func_terminal_break_i64.fst
index 07fa590..4736d42 100644
--- base/switch_stmt/Func_terminal_break_i64.fst
+++ head/switch_stmt/Func_terminal_break_i64.fst
@@ -13,9 +13,9 @@ divergent fn func_terminal_break_i64 (var_x: Typedef_int64_t.ty_int64_t)
let mut var_x = var_x;
let mut var_result : Typedef_int32_t.ty_int32_t;
var_result := 0l;
- let var___switch_scrut_9 : Typedef_int64_t.ty_int64_t = (!var_x);
+ let var___switch_scrut_13 : Typedef_int64_t.ty_int64_t = (!var_x);
{
- match (var___switch_scrut_9) {
+ match (var___switch_scrut_13) {
-1L -> {
var_result := 1l;
}
@@ -25,6 +25,6 @@ divergent fn func_terminal_break_i64 (var_x: Typedef_int64_t.ty_int64_t)
ensures (((live var_x) ** (live var_result)) **
(with_pure
(((id #int (Int32.v (!var_result))) = 0) || ((id #int (Int32.v (!var_result))) = 1))))
- label __pal_match_join_4:;
+ label __pal_match_join_5:;
return (!var_result);
}
\ No newline at end of file
diff --git base/switch_stmt/Func_terminal_break_promoted_u8.fst head/switch_stmt/Func_terminal_break_promoted_u8.fst
index 0d6d313..08b74d5 100644
--- base/switch_stmt/Func_terminal_break_promoted_u8.fst
+++ head/switch_stmt/Func_terminal_break_promoted_u8.fst
@@ -13,9 +13,9 @@ divergent fn func_terminal_break_promoted_u8 (var_x: Typedef_uint8_t.ty_uint8_t)
let mut var_x = var_x;
let mut var_result : Typedef_int32_t.ty_int32_t;
var_result := 0l;
- let var___switch_scrut_8 : Int32.t = (id #Int32.t (Int.Cast.uint8_to_int32 (!var_x)));
+ let var___switch_scrut_12 : Int32.t = (id #Int32.t (Int.Cast.uint8_to_int32 (!var_x)));
{
- match (var___switch_scrut_8) {
+ match (var___switch_scrut_12) {
255l -> {
var_result := 1l;
}
@@ -25,6 +25,6 @@ divergent fn func_terminal_break_promoted_u8 (var_x: Typedef_uint8_t.ty_uint8_t)
ensures (((live var_x) ** (live var_result)) **
(with_pure
(((id #int (Int32.v (!var_result))) = 0) || ((id #int (Int32.v (!var_result))) = 1))))
- label __pal_match_join_3:;
+ label __pal_match_join_4:;
return (!var_result);
}
\ No newline at end of file
diff --git base/switch_stmt/Func_terminal_break_scale.fst head/switch_stmt/Func_terminal_break_scale.fst
index a206cf6..c908d53 100644
--- base/switch_stmt/Func_terminal_break_scale.fst
+++ head/switch_stmt/Func_terminal_break_scale.fst
@@ -13,55 +13,55 @@ divergent fn func_terminal_break_scale (var_x: Typedef_int32_t.ty_int32_t)
let mut var_x = var_x;
let mut var_result : Typedef_int32_t.ty_int32_t;
var_result := 0l;
- let var___switch_scrut_12 : Typedef_int32_t.ty_int32_t = (!var_x);
+ let var___switch_scrut_16 : Typedef_int32_t.ty_int32_t = (!var_x);
{
- match (var___switch_scrut_12) {
- 33l -> {
+ match (var___switch_scrut_16) {
+ 43l -> {
var_result := 1l;
}
- 34l -> {
+ 44l -> {
var_result := 1l;
}
- 35l -> {
+ 45l -> {
var_result := 1l;
}
- 36l -> {
+ 46l -> {
var_result := 1l;
}
- 37l -> {
+ 47l -> {
var_result := 1l;
}
- 38l -> {
+ 48l -> {
var_result := 1l;
}
- 39l -> {
+ 49l -> {
var_result := 1l;
}
- 40l -> {
+ 50l -> {
var_result := 1l;
}
- 41l -> {
+ 51l -> {
var_result := 1l;
}
- 42l -> {
+ 52l -> {
var_result := 1l;
}
- 43l -> {
+ 53l -> {
var_result := 1l;
}
- 44l -> {
+ 54l -> {
var_result := 1l;
}
- 45l -> {
+ 55l -> {
var_result := 1l;
}
- 46l -> {
+ 56l -> {
var_result := 1l;
}
- 47l -> {
+ 57l -> {
var_result := 1l;
}
- 48l -> {
+ 58l -> {
var_result := 1l;
}
_ -> {}
@@ -70,6 +70,6 @@ divergent fn func_terminal_break_scale (var_x: Typedef_int32_t.ty_int32_t)
ensures (((live var_x) ** (live var_result)) **
(with_pure
(((id #int (Int32.v (!var_result))) = 0) || ((id #int (Int32.v (!var_result))) = 1))))
- label __pal_match_join_6:;
+ label __pal_match_join_7:;
return (!var_result);
}
\ No newline at end of file
diff --git base/switch_stmt/Func_terminal_break_u32.fst head/switch_stmt/Func_terminal_break_u32.fst
index cdf9530..8450d1b 100644
--- base/switch_stmt/Func_terminal_break_u32.fst
+++ head/switch_stmt/Func_terminal_break_u32.fst
@@ -13,9 +13,9 @@ divergent fn func_terminal_break_u32 (var_x: Typedef_uint32_t.ty_uint32_t)
let mut var_x = var_x;
let mut var_result : Typedef_int32_t.ty_int32_t;
var_result := 0l;
- let var___switch_scrut_7 : Typedef_uint32_t.ty_uint32_t = (!var_x);
+ let var___switch_scrut_11 : Typedef_uint32_t.ty_uint32_t = (!var_x);
{
- match (var___switch_scrut_7) {
+ match (var___switch_scrut_11) {
0ul -> {
var_result := 1l;
}
@@ -28,6 +28,6 @@ divergent fn func_terminal_break_u32 (var_x: Typedef_uint32_t.ty_uint32_t)
ensures (((live var_x) ** (live var_result)) **
(with_pure
(((id #int (Int32.v (!var_result))) = 0) || ((id #int (Int32.v (!var_result))) = 1))))
- label __pal_match_join_2:;
+ label __pal_match_join_3:;
return (!var_result);
}
\ No newline at end of file
diff --git base/switch_stmt/Func_terminal_break_u64.fst head/switch_stmt/Func_terminal_break_u64.fst
index f5e9ec7..48b2106 100644
--- base/switch_stmt/Func_terminal_break_u64.fst
+++ head/switch_stmt/Func_terminal_break_u64.fst
@@ -13,9 +13,9 @@ divergent fn func_terminal_break_u64 (var_x: Typedef_uint64_t.ty_uint64_t)
let mut var_x = var_x;
let mut var_result : Typedef_int32_t.ty_int32_t;
var_result := 0l;
- let var___switch_scrut_10 : Typedef_uint64_t.ty_uint64_t = (!var_x);
+ let var___switch_scrut_14 : Typedef_uint64_t.ty_uint64_t = (!var_x);
{
- match (var___switch_scrut_10) {
+ match (var___switch_scrut_14) {
0uL -> {
var_result := 1l;
}
@@ -28,6 +28,6 @@ divergent fn func_terminal_break_u64 (var_x: Typedef_uint64_t.ty_uint64_t)
ensures (((live var_x) ** (live var_result)) **
(with_pure
(((id #int (Int32.v (!var_result))) = 0) || ((id #int (Int32.v (!var_result))) = 1))))
- label __pal_match_join_5:;
+ label __pal_match_join_6:;
return (!var_result);
}
\ No newline at end of file
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Part of the upstreaming of
nswamy/pal-c-project-integration(PR20 of 35 PRs) — seePR_PLAN.mdon that branch for the whole plan and the dependency graph.Base:
main. Depends on nothing; reviewable on its own.Consecutive labels nest in clang, so
case 2: case 3: default:arrives asCaseStmt(2, CaseStmt(3, DefaultStmt(..))); the group builder peeled only theCaseStmtchain and statement translation then rejected the stray
DefaultStmt. Peels the wholechain in either order and marks the group default, dropping its explicit case values —
an arm reached by anything gains nothing from also testing for 2 or 3. The second commit
lowers a fall-through-free switch with a
defaultas an if/else chain: the generalencoding threads
hit/brkflags, so every arm executes under a compound condition overmutable state, and the join — phrased in terms of the scrutinee — never meets the guards.
An explicit switch postcondition still takes the match form, which needs one.
Commits
Testing
Verified:
make rust lib,test/check-template.sh,cargo fmt --check,clang-format --dry-run --Werror, and F* verification oftest/switch_stmt.