uw-unsat / serval Goto Github PK

I am trying to use Serval and I checked that my program does not have any unbounded loops or locks.
But when the program execute to this line:
(check-asserts-only (interpret-objdump-program cpu instructions))
the program never ends.
Please tell me what do I miss, thank you.

I tried to use serval to verify a RISC-V system. The specification I wrote was similar to that in serval-sosp19.
When rosette executes to this procedure:
(interpret-objdump-program cpu instructions)
This error happened:
instruction (csrrw (bv #x340 12) (bv #b00000 5) (bv #b00000 5)) not implemented

The whole outputs are like this:

raco test --check-stderr --table --timeout 1200 --jobs 8 verif/riscv.rkt
raco test: 0 (submod "verif/riscv.rkt" test)
riscv ecall tests
[ RUN      ] "init riscv check"
--------------------
riscv ecall tests > init riscv check
ERROR

instruction (csrrw (bv #x340 12) (bv #b00000 5) (bv #b00000 5)) not implemented
--------------------
0 success(es) 0 failure(s) 1 error(s) 1 test(s) run
cpu time: 86445 real time: 86424 gc time: 377
1
riscv.rkt: raco test: non-empty stderr: #"--------------------\nriscv ecall tests > init riscv check\nERROR\n\ninstruction (csrrw (bv #x340 12) (bv #b00000 5) (bv #b00000 5)) not implemented\n--------------------\n0 success(es) 0 failure(s) 1 error(s) 1 test(s) run\n"
1 1 verif/riscv.rkt
1/1 test failures
verif/verif.mk:16: recipe for target 'verify-system-riscv' failed

It seems like the error happened when it tries to write zero to the mscratch register.
But instructions like csrrw zero,mscratch,zero are obviously implemented in serval.
As for csrrw (bv #x340 12) (bv #b00000 5) (bv #b00000 5), I don't see any assembly related to this in my assembly file.

Can you please help me out?
Thank you!

When trying to compile a Rust file to a .ll.rkt file (.rs -> .ll -> .ll.rkt), the LLVM-Rosette tool throws the following error: “llvm: unknown value: i8* null”.

In the .ll file the only "i8* null" appears in the compiled version of core::ptr::null. After further examination of the LLVM-Rosette tool, it seems like a case for [constant-pointer-null] could be missing where the tool maps libLLVM functionality to Rosette - in the "value-ref" function in serval/llvm/parse.rkt (line 240). I've tried the following (hard-coding 64 just for now) as the additional case statement:

[(constant-pointer-null)
(bv 0 (bitvector 64))]

However, this causes at least one downstream error of the kind: "LLVMTypeRef->C: argument is not non-null `LLVMTypeRef' pointer". Is there a different encoding for null values I can use that won't cause this error? And/or have I set this up wrong? Any insight about what is going on here would be much appreciated!

I am doing a simple experiment with arrays in c. The c code is:

`int vec0[5];

int vec_func(int num) {
vec0[0] = 1;
vec0[1] = 2;
vec0[2] = 3;
vec0[3] = 4;
vec0[4] = 5;

return vec0[num];
}`

And here is the partial code for checking:

`(define (check-vec)
(parameterize ([llvm:current-machine (llvm:make-machine cpp:symbols cpp:globals)])

; symbolic inputs
(define-symbolic num (bitvector 32))

; symbolic result
(define r (cpp:@vec_func num))

(define sol
  (solve
   (begin
     (assume (bvsle num 5))
     (assert (not equal? r 3))
    )
  )
)
sol

))

`
But when I ran the checking, an error is reported:

[assert] ~/serval/serval/lib/memory/mblock.rkt:254 mcell-path: block size (bv #x0000000000000001 64) must be a multiple of size (bv #x0000000000000004 64)

I am writing and reading int from the array, so the block size should be 4 byte. why the error says block size is #x0000000000000001?
It seems the "element-size" in mblock.rkt has some problem: it always returns 1 for the integer array, even though its element type is int.

Update: I just find the same error happens for provided array.c in the test folder.

I'm trying to run the tests as a way to learn how to use serval and I'm having trouble.

I tried running make all from test/ and I ran into the following issue:

Am I missing a dependency? Am I using the wrong program to generate llvm?

When I am parsing some LLVM IR code which was generated by JLang from Java code to ll.rkt, something error happens.

llvm: error: invalid field 'variables'
!4 = distinct !DISubprogram(name: "Jni_trampoline_(L)L", 
linkageName: "Jni_trampoline_(L)L", scope: !1, file: !1, 
line: 52, type: !5, isLocal: false, isDefinition: true, 
scopeLine: 52, flags: DIFlagPrototyped, isOptimized: false,
unit: !0, variables: !2)
            ^

context...:
/serval/serval/serval/llvm/capi/irreader.rkt:11:2
/usr/share/racket/collects/ffi/unsafe/alloc.rkt:77:11
/usr/share/racket/collects/racket/private/more-scheme.rkt:265:2: call-with-exception-handler
/serval/serval/serval/llvm/parse.rkt:26:0: bytes->module
"/serval/serval/serval/bin/serval-llvm.rkt": [running body]
temp37_0
for-loop
run-module-instance!125
perform-require!78
make: *** [racket/racket.mk:21: my/ClientChannel.ll.rkt] Error 1

I don't know how to solve this problem.Could you help me?

Currently, the dwarf interpreter find global variables only at level <1> of the hierarchy, which works fine for C programs. However, in Rust (as well as C++ presumably), globals often appear inside namespaces which are nested in the dwarf info. For example:

pub static mut FOOBAR: u64 = 0;

#[no_mangle]
pub extern "C" fn _start() {
...
}

Results in a dwarf info containing the variable FOOBAR at level <2> nested under the namespace of the Rust crate. Globals inside public modules are further nested in the dwarf, so:

pub mod barbaz {
pub static mut FOOBAR: u64 = 0;
}

appears at level <3> in the dwarf under the barbaz namespace, which is under the crate namespace, and so on...

Moreover, the name in the .map.rkt (the output from nm) appears as a mangled name which includes the modules/namspaces leading to the variable, e.g. _ZN7toyrust6FOOBAR17h46bb1dae670b94b8E.

I think it's easy enough to change the dwarf parser to recurse down the all namespaces, and use the DWARF_AT_linkage_name as the variable name instead of DW_AT_name, if it is available (so it can be correctly correlated with the variable name in the map file inside create-mregions).

Does this seem reasonable? This isn't a PR simply because I'm very slowly learning Racket's macro language to be able to correctly modify the parser...