May 2018 - Devel - lists.sel4.systems

Help with Isabelle/AutoCorres
by Burkhart Wolff 18 May '18

18 May '18

Dear all, I stumbled into some problems with AutoCorres and would be grateful if someone could help me. I used the recent version autocorres1.4 under Isabelle2017. A) Running under MacOS, cpp is apparently not running inside install_C_file (yes, I installed the cpp wrapper: >>>>>>>>>>>>>>>>>>>>>> !/bin/bash # Wrapper for clang C preprocessor on MacOS export L4CPP="-DTARGET=ARM -DTARGET_ARM -DPLATFORM=Sabre -DPLATFORM_Sabre" llvm-gcc -Wno-invalid-pp-token -E -x c $@ <<<<<<<<<<<<<<<<<<<<<< and made sure that it is in the path of the shell in which I started Isabelle.) Does anyone know a cause for this behaviour or a feasible workaround ? (besides doing the expansions by hand) Is there an explicit Isabelle shell variable where the path to cpp must be set ? B) I get a weird crash of AutoCorres without a clue what might cause it: I have a T4.h file with >>>>>>>>>>>>>>>>>>>>>>> #define N_TEETH ( 100 * MODULO ) // shaft encoder's number of teeth per turn #define SIZE_OF_SPEED_FIFO 10 // number of samples to compute average speed extern const char *InputField[]; enum State { S1=1, S2, S3, S4, S5, S6, SFail=0 }; enum Status { FAIL, SUCCESS }; enum InputPatterns { Ph1 = 1, Ph2 = 5, Ph3 = 4, Ph4 = 6, Ph5 = 2, Ph6 = 3 }; struct OBits { int C1 ; int C2 ; int C3 ; } Obits; /********* Output data *****************/ extern enum Status O_Position_Valid; extern unsigned int O_Position_Count; extern unsigned int Relative_Position; extern int Instantaneous_Speed; extern int Mean_Speed; <<<<<<<<<<<<<<<<<<<<<<<<<<<<< and a T4.c file with: >>>>>>>>>>>>>>>>>>>>>>>>>>>>> #include "T4_AlgoODO.h" enum Status O_P_V = SUCCESS; unsigned int O_P_C = 0; unsigned int Relative_Position = 0; int I_Speed = 0; int Mean_Speed = 0; int Acceleration = 0; int scale = 1000; int PI_approx = 3141; struct OBits Input; enum State OState; const unsigned int Radius = 500; const unsigned int Sampling_Rate = 400; unsigned int F_O_P_C = 0; int Speed_FIFO[10 /*SIZE_OF_SPEED_FIFO*/]; int FIFO_pointer = 0; <<<<<<<<<<<<<<<<<<<<<<<<<<<<<<< Loading this in Isabelle/AutoCorres with: >>>>>>>>>>>>>>>>>>>>>>>>> install_C_file "code/c/T4.c” <<<<<<<<<<<<<<<<<<<<<<<<< results in the following AutoCorres crash: … exception Fail raised (line 175 of "~/codebox/odo_new/odo/autocorres-1.4/c-parser/calculate_state.ML"): translate_inttype: incomplete array! Can anybody tell me what this means and propose a workaround ? Best regards B. Wolff

2 1

Untyped Retype destination not empty?
by Richard Clark 18 May '18

18 May '18

Hi! I could use a clue as to the cause of this problem. The program has its free slots start index set correctly. It is trying to allocate a dma buffer. (4k with a known physical address). The vspace has been properly set up and knows the phys addresses of its free memory. This used to work fine in a different process, but I can't find anything I've done different/wrong in this one... I've added some extra printfs, and some debug code (in kernel/src/object/untyped.c). /* Ensure that the destination slots are all empty. */ slots.cnode = CTE_PTR(cap_cnode_cap_get_capCNodePtr(nodeCap)); slots.offset = nodeOffset; slots.length = nodeWindow; for (i = nodeOffset; i < nodeOffset + nodeWindow; i++) { status = ensureEmptySlot(slots.cnode + i); if (status != EXCEPTION_NONE) { userError("Untyped Retype: Slot #%d from %p in destination window non-empty.", (int)i, (void *)slots.cnode); userError("Untyped Retype: At offset #%d length %d.", (int)nodeOffset, (int)nodeWindow); int j = 0; for(j=0;j<2048;j++){ status = ensureEmptySlot(slots.cnode + (i + j)); if (status == EXCEPTION_NONE) { userError("Next Free Slot at #%d from %p.", (int)(i+j), (void *)slots.cnode); status = EXCEPTION_SYSCALL_ERROR; break; } } return status; } } And finally, here is the output from the console: <<seL4(CPU 0) [decodeCNodeInvocation/94 T0xffffff8001a25400 "Lockmaproc" @4196e8]: CNode Copy/Mint/Move/Mutate: Destination not empty.>> <<seL4(CPU 0) [decodeUntypedInvocation/166 T0xffffff8001a25400 "Lockmaproc" @420f2c]: Untyped Retype: Slot #196 from 0xffffff807f000000 in destination window non-empty.>> <<seL4(CPU 0) [decodeUntypedInvocation/167 T0xffffff8001a25400 "Lockmaproc" @420f2c]: Untyped Retype: At offset #196 length 1.>> <<seL4(CPU 0) [decodeUntypedInvocation/172 T0xffffff8001a25400 "Lockmaproc" @420f2c]: Next Free Slot at #197 from 0xffffff807f000000.>> _refill_pool@split.c:187 Failed to retype untyped, error 8 vka_alloc_object_at_maybe_dev@object.h:59 Failed to allocate object of size 4096, error 1 dma_alloc@page_dma.c:92 Failed to allocate untyped of size 12 I need a hint... help? Thanks! Richard ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

2 1

Automatic testing using qemu
by Paolo Crisafulli 17 May '18

17 May '18

Hi there, I have written a seL4 app using CAmkES, that I am continuously building using Jenkins. I'd like to add a test step to this continuous integration process, launching the app with qemu and parsing the output to validate my expectations. The thing is, although all the active ("control") components reach their last instruction after a while, seL4 does not "exit" (which is expected I guess) and qemu does not stop, keeping my continuous integration job running for ever. Any idea on how to achieve this? Thank you very much in advance. Cheers, Paolo Crisafulli

3 5