summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--language/jib.ott2
-rw-r--r--lib/mapping.sail84
-rw-r--r--lib/real.sail4
-rw-r--r--lib/string.sail2
-rw-r--r--src/jib/jib_smt.ml39
-rw-r--r--src/jib/jib_ssa.ml20
-rw-r--r--src/jib/jib_util.ml4
-rw-r--r--src/property.mli2
-rw-r--r--src/sail.ml3
-rw-r--r--test/smt/encdec.sat.sail64
-rwxr-xr-xtest/smt/run_tests.py2
-rw-r--r--test/smt/rv_add_0.unsat.sail2
12 files changed, 216 insertions, 12 deletions
diff --git a/language/jib.ott b/language/jib.ott
index 447b25e3..dfda3bbc 100644
--- a/language/jib.ott
+++ b/language/jib.ott
@@ -58,6 +58,8 @@ name :: '' ::=
op :: '' ::=
| not :: :: bnot
+ | or :: :: bor
+ | and :: :: band
| hd :: :: list_hd
| tl :: :: list_tl
| bit_to_bool :: :: bit_to_bool
diff --git a/lib/mapping.sail b/lib/mapping.sail
new file mode 100644
index 00000000..6cbb7585
--- /dev/null
+++ b/lib/mapping.sail
@@ -0,0 +1,84 @@
+$ifndef _MAPPING
+$define _MAPPING
+
+$include <arith.sail>
+$include <option.sail>
+
+val string_take = "string_take" : (string, nat) -> string
+val string_drop = "string_drop" : (string, nat) -> string
+val string_length = "string_length" : string -> nat
+val string_append = {c: "concat_str", _: "string_append"} : (string, string) -> string
+val string_startswith = "string_startswith" : (string, string) -> bool
+
+val n_leading_spaces : string -> nat
+function n_leading_spaces s =
+ match s {
+ "" => 0,
+ _ => match string_take(s, 1) {
+ " " => 1 + n_leading_spaces(string_drop(s, 1)),
+ _ => 0
+ }
+ }
+
+val spc : unit <-> string
+val opt_spc : unit <-> string
+val def_spc : unit <-> string
+
+val spc_forwards : unit -> string
+function spc_forwards () = " "
+val spc_backwards : string -> unit
+function spc_backwards s = ()
+val spc_matches_prefix : string -> option((unit, nat))
+function spc_matches_prefix s = {
+ let n = n_leading_spaces(s);
+ match n {
+ 0 => None(),
+ _ => Some((), n)
+ }
+}
+
+val opt_spc_forwards : unit -> string
+function opt_spc_forwards () = ""
+val opt_spc_backwards : string -> unit
+function opt_spc_backwards s = ()
+val opt_spc_matches_prefix : string -> option((unit, nat))
+function opt_spc_matches_prefix s =
+ Some((), n_leading_spaces(s))
+
+val def_spc_forwards : unit -> string
+function def_spc_forwards () = " "
+val def_spc_backwards : string -> unit
+function def_spc_backwards s = ()
+val def_spc_matches_prefix : string -> option((unit, nat))
+function def_spc_matches_prefix s = opt_spc_matches_prefix(s)
+
+val sep : unit <-> string
+mapping sep : unit <-> string = {
+ () <-> opt_spc() ^ "," ^ def_spc()
+}
+
+$ifdef _DEFAULT_DEC
+$include <vector_dec.sail>
+
+val hex_bits_20 : bits(20) <-> string
+val hex_bits_20_forwards = "decimal_string_of_bits" : bits(20) -> string
+val hex_bits_20_forwards_matches : bits(20) -> bool
+function hex_bits_20_forwards_matches bv = true
+val "hex_bits_20_matches_prefix" : string -> option((bits(20), nat))
+val hex_bits_20_backwards_matches : string -> bool
+function hex_bits_20_backwards_matches s = match s {
+ s if match hex_bits_20_matches_prefix(s) {
+ Some (_, n) if n == string_length(s) => true,
+ _ => false
+ } => true,
+ _ => false
+}
+val hex_bits_20_backwards : string -> bits(20)
+function hex_bits_20_backwards s =
+ match hex_bits_20_matches_prefix(s) {
+ Some (bv, n) if n == string_length(s) => bv
+ }
+
+$endif
+
+$endif
diff --git a/lib/real.sail b/lib/real.sail
index 47d3f9bd..cd63a622 100644
--- a/lib/real.sail
+++ b/lib/real.sail
@@ -1,5 +1,5 @@
-$ifndef __REAL
-$define __REAL
+$ifndef _REAL
+$define _REAL
val "neg_real" : real -> real
diff --git a/lib/string.sail b/lib/string.sail
index 3fe74eb5..87e4da57 100644
--- a/lib/string.sail
+++ b/lib/string.sail
@@ -5,6 +5,8 @@ $include <arith.sail>
val eq_string = {lem: "eq", coq: "generic_eq", _: "eq_string"} : (string, string) -> bool
+overload operator == = {eq_string}
+
infixl 9 ^-^
val concat_str = {lem: "stringAppend", _: "concat_str"} : (string, string) -> string
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 086d4d11..350f50d9 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -67,6 +67,8 @@ let opt_ignore_overflow = ref false
let opt_auto = ref false
+let opt_debug_graphs = ref false
+
module EventMap = Map.Make(Event)
(* Note that we have to use x : ty ref rather than mutable x : ty, to
@@ -278,6 +280,10 @@ let rec smt_cval ctx cval =
Fn ("=", [smt_cval ctx cval; Bin "1"])
| V_call (Bnot, [cval]) ->
Fn ("not", [smt_cval ctx cval])
+ | V_call (Band, cvals) ->
+ Fn ("and", List.map (smt_cval ctx) cvals)
+ | V_call (Bor, cvals) ->
+ Fn ("or", List.map (smt_cval ctx) cvals)
| V_ctor_kind (union, ctor_id, unifiers, _) ->
Fn ("not", [Tester (zencode_ctor ctor_id unifiers, smt_cval ctx union)])
| V_ctor_unwrap (ctor_id, union, unifiers, _) ->
@@ -322,6 +328,9 @@ let add_event ctx ev smt =
let stack = event_stack ctx ev in
Stack.push (Fn ("=>", [ctx.pathcond; smt])) stack
+let add_pathcond_event ctx ev =
+ Stack.push ctx.pathcond (event_stack ctx ev)
+
let overflow_check ctx smt =
if not !opt_ignore_overflow then (
Util.warn "Adding overflow check in generated SMT";
@@ -903,6 +912,16 @@ let builtin_compare_bits fn ctx v1 v2 ret_ctyp =
| _ -> builtin_type_error ctx fn [v1; v2] (Some ret_ctyp)
+(* ***** String operations: lib/real.sail ***** *)
+
+let builtin_decimal_string_of_bits ctx v =
+ begin match cval_ctyp v with
+ | CT_fbits (n, _) ->
+ Fn ("int.to.str", [Fn ("bv2nat", [smt_cval ctx v])])
+
+ | _ -> builtin_type_error ctx "decimal_string_of_bits" [v] None
+ end
+
(* ***** Real number operations: lib/real.sail ***** *)
let builtin_sqrt_real ctx root v =
@@ -986,6 +1005,7 @@ let smt_builtin ctx name args ret_ctyp =
(* string builtins *)
| "concat_str", [v1; v2], CT_string -> ctx.use_string := true; Fn ("str.++", [smt_cval ctx v1; smt_cval ctx v2])
| "eq_string", [v1; v2], CT_bool -> ctx.use_string := true; Fn ("=", [smt_cval ctx v1; smt_cval ctx v2])
+ | "decimal_string_of_bits", [v], CT_string -> ctx.use_string := true; builtin_decimal_string_of_bits ctx v
(* lib/real.sail *)
(* Note that sqrt_real is special and is handled by smt_instr. *)
@@ -1408,7 +1428,7 @@ let smt_instr ctx =
| I_aux (I_clear _, _) -> []
| I_aux (I_match_failure, _) ->
- add_event ctx Match (Bool_lit false);
+ add_pathcond_event ctx Match;
[]
| I_aux (I_undefined ctyp, _) -> []
@@ -1606,6 +1626,12 @@ let rec smt_query ctx = function
| Q_or qs ->
Fn ("or", List.map (smt_query ctx) qs)
+let dump_graph function_id cfg =
+ let gv_file = string_of_id function_id ^ ".gv" in
+ let out_chan = open_out gv_file in
+ Jib_ssa.make_dot out_chan cfg;
+ close_out out_chan
+
let smt_cdef props lets name_file ctx all_cdefs = function
| CDEF_spec (function_id, arg_ctyps, ret_ctyp) when Bindings.mem function_id props ->
begin match find_function [] function_id all_cdefs with
@@ -1641,14 +1667,13 @@ let smt_cdef props lets name_file ctx all_cdefs = function
let visit_order =
try topsort cfg with
| Not_a_DAG n ->
- let gv_file = string_of_id function_id ^ ".gv" in
- let out_chan = open_out gv_file in
- make_dot out_chan cfg;
- close_out out_chan;
+ dump_graph function_id cfg;
raise (Reporting.err_general pragma_l
- (Printf.sprintf "$%s %s: control flow graph is not acyclic (node %d is in cycle)\nWrote graph to %s"
- prop_type (string_of_id function_id) n gv_file))
+ (Printf.sprintf "$%s %s: control flow graph is not acyclic (node %d is in cycle)\nWrote graph to %s.gv"
+ prop_type (string_of_id function_id) n (string_of_id function_id)))
in
+ if !opt_debug_graphs then
+ dump_graph function_id cfg;
List.iter (fun n ->
begin match get_vertex cfg n with
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index 9a9a3361..a4a77f9d 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -619,15 +619,33 @@ let place_pi_functions graph start idom children =
List.concat (List.map (function Pi guards -> guards | _ -> []) ssanodes)
in
+ let rec between_dom p n =
+ if n = p then
+ []
+ else
+ match graph.nodes.(n) with
+ | Some ((_, cfnode), preds, _) ->
+ let preds = List.concat (List.map (between_dom p) (IntSet.elements preds)) in
+ begin match get_guard cfnode, preds with
+ | [guard], [pred] -> [V_call (Band, [guard; pred])]
+ | [guard], [] -> [guard]
+ | [guard], _ -> [V_call (Band, [guard; V_call (Bor, preds)])]
+ | _, (_ :: _ :: _ as preds) -> [V_call (Bor, preds)]
+ | _, pred -> pred
+ end
+ | None -> assert false
+ in
+
let rec go n =
begin match graph.nodes.(n) with
| Some ((ssa, cfnode), preds, succs) ->
let p = idom.(n) in
+ let bd = between_dom p n in
if p <> -1 then
begin match graph.nodes.(p) with
| Some ((dom_ssa, _), _, _) ->
let args = get_guard cfnode @ get_pi_contents dom_ssa in
- graph.nodes.(n) <- Some ((Pi args :: ssa, cfnode), preds, succs)
+ graph.nodes.(n) <- Some ((Pi (bd @ args) :: ssa, cfnode), preds, succs)
| None -> assert false
end
| None -> assert false
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index 378f5fae..3326d4ad 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -278,6 +278,8 @@ let string_of_name ?deref_current_exception:(dce=true) ?zencode:(zencode=true) =
let string_of_op = function
| Bnot -> "@not"
+ | Band -> "@and"
+ | Bor -> "@or"
| List_hd -> "@hd"
| List_tl -> "@tl"
| Bit_to_bool -> "@bit_to_bool"
@@ -896,6 +898,8 @@ let rec infer_call op vs =
match op, vs with
| Bit_to_bool, _ -> CT_bool
| Bnot, _ -> CT_bool
+ | Band, _ -> CT_bool
+ | Bor, _ -> CT_bool
| List_hd, [v] ->
begin match cval_ctyp v with
| CT_list ctyp -> ctyp
diff --git a/src/property.mli b/src/property.mli
index 3789fa63..f84a85e3 100644
--- a/src/property.mli
+++ b/src/property.mli
@@ -90,6 +90,8 @@ val rewrite : tannot defs -> tannot defs
type event = Overflow | Assertion | Assumption | Match | Return
+val string_of_event : event -> string
+
module Event : sig
type t = event
val compare : event -> event -> int
diff --git a/src/sail.ml b/src/sail.ml
index c2b2ed65..daec1fdb 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -315,6 +315,9 @@ let options = Arg.align ([
( "-ddump_flow_graphs",
Arg.Set Jib_compile.opt_debug_flow_graphs,
" (debug) dump flow analysis for Sail functions when compiling to C");
+ ( "-ddump_smt_graphs",
+ Arg.Set Jib_smt.opt_debug_graphs,
+ " (debug) dump flow analysis for properties when generating SMT");
( "-dtc_verbose",
Arg.Int (fun verbosity -> Type_check.opt_tc_debug := verbosity),
"<verbosity> (debug) verbose typechecker output: 0 is silent");
diff --git a/test/smt/encdec.sat.sail b/test/smt/encdec.sat.sail
new file mode 100644
index 00000000..d34f3629
--- /dev/null
+++ b/test/smt/encdec.sat.sail
@@ -0,0 +1,64 @@
+default Order dec
+
+$include <prelude.sail>
+$include <string.sail>
+$include <mapping.sail>
+
+type regbits = bits(5)
+
+val reg_name : bits(5) <-> string
+mapping reg_name = {
+ 0b00000 <-> "zero",
+ 0b00001 <-> "ra",
+ 0b00010 <-> "sp",
+ 0b00011 <-> "gp",
+ 0b00100 <-> "tp",
+ 0b00101 <-> "t0",
+ 0b00110 <-> "t1",
+ 0b00111 <-> "t2",
+ 0b01000 <-> "fp",
+ 0b01001 <-> "s1",
+ 0b01010 <-> "a0",
+ 0b01011 <-> "a1",
+ 0b01100 <-> "a2",
+ 0b01101 <-> "a3",
+ 0b01110 <-> "a4",
+ 0b01111 <-> "a5",
+ 0b10000 <-> "a6",
+ 0b10001 <-> "a7",
+ 0b10010 <-> "s2",
+ 0b10011 <-> "s3",
+ 0b10100 <-> "s4",
+ 0b10101 <-> "s5",
+ 0b10110 <-> "s6",
+ 0b10111 <-> "s7",
+ 0b11000 <-> "s8",
+ 0b11001 <-> "s9",
+ 0b11010 <-> "s10",
+ 0b11011 <-> "s11",
+ 0b11100 <-> "t3",
+ 0b11101 <-> "t4",
+ 0b11110 <-> "t5",
+ 0b11111 <-> "t6"
+}
+
+enum uop = RISCV_LUI | RISCV_AUIPC
+
+mapping utype_mnemonic : uop <-> string = {
+ RISCV_LUI <-> "lui",
+ RISCV_AUIPC <-> "auipc"
+}
+
+val assembly : ast <-> string
+
+scattered union ast
+
+union clause ast = UTYPE : (bits(20), regbits, uop)
+
+mapping clause assembly = UTYPE(imm, rd, op)
+ <-> utype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_20(imm)
+
+$counterexample
+function prop(x: string) -> bool = {
+ not_bool(utype_mnemonic(RISCV_LUI) == x)
+}
diff --git a/test/smt/run_tests.py b/test/smt/run_tests.py
index c9cadec3..f59bdba9 100755
--- a/test/smt/run_tests.py
+++ b/test/smt/run_tests.py
@@ -23,7 +23,7 @@ def test_smt(name, solver, sail_opts):
tests[filename] = os.fork()
if tests[filename] == 0:
step('sail {} -smt {} -o {}'.format(sail_opts, filename, basename))
- step('timeout 20s {} {}_prop.smt2 1> {}.out'.format(solver, basename, basename))
+ step('timeout 300s {} {}_prop.smt2 1> {}.out'.format(solver, basename, basename))
if re.match('.+\.sat\.sail$', filename):
step('grep -q ^sat$ {}.out'.format(basename))
else:
diff --git a/test/smt/rv_add_0.unsat.sail b/test/smt/rv_add_0.unsat.sail
index 87c55487..ed45112e 100644
--- a/test/smt/rv_add_0.unsat.sail
+++ b/test/smt/rv_add_0.unsat.sail
@@ -145,7 +145,7 @@ function clause execute (ITYPE (imm, rs1, rd, RISCV_ADDI)) =
function clause decode _ = None()
-$counterexample
+$property
function prop(imm: bits(12), rs1: regbits, rd: regbits, v: xlenbits) -> bool = {
X(rs1) = v;
match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) {
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-11 04:10:25 +0000