drop support for Cogent

The Cogent project is no longer actively developed on top of seL4, and
the upstream build has broken.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-05-26 17:10:56 +10:00 committed by Gerwin Klein
parent aef13286d7
commit 3eff84e818
13 changed files with 1 additions and 618 deletions

View File

@ -1,66 +0,0 @@
#
# Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
#
# SPDX-License-Identifier: BSD-2-Clause
#
cmake_minimum_required(VERSION 3.7.2)
project(uart_cogent C)
# This only works on sabre
if(
NOT
"${KernelArch}"
STREQUAL
"arm"
OR
NOT
"${KernelARMPlatform}"
STREQUAL
"sabre"
)
message(FATAL_ERROR "uart application only supported on Arm sabre")
endif()
find_program(COGENT_TOOL NAMES "cogent")
set(driver_src_dir ${CMAKE_CURRENT_LIST_DIR}/components/Driver/src/)
set(c_flags "$CPPIN -o $CPPOUT -E -P -I${COGENT_PATH}/lib")
add_custom_command(
OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/serial_pp_inferred.c
COMMAND cp ${driver_src_dir}/serial.cogent serial.cogent
COMMAND cp ${driver_src_dir}/serial.ac serial.ac
COMMAND
${COGENT_TOOL} serial.cogent -g -Od -ogenerated
--fno-fncall-as-macro
--ffunc-purity-attr
--Wno-warn
--infer-c-funcs=serial.ac
--cpp-args=${c_flags}
--ext-types=${driver_src_dir}/types.cfg
--entry-funcs=${driver_src_dir}/entrypoints.cfg
VERBATIM
DEPENDS
${driver_src_dir}/serial.cogent
${driver_src_dir}/serial.ac
${driver_src_dir}/types.cfg
${driver_src_dir}/entrypoints.cfg
)
DeclareCAmkESComponent(Client SOURCES components/Client/src/client.c)
DeclareCAmkESComponent(
Driver
SOURCES
${CMAKE_CURRENT_BINARY_DIR}/serial_pp_inferred.c
INCLUDES
${COGENT_PATH}/lib
)
DeclareCAmkESRootserver(uart.camkes)
add_simulate_test([=[
wait_for "This message is sent via UART."
send "abcds"
wait_for "Input from UART: s"
]=])

View File

@ -1,51 +0,0 @@
<!--
Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
SPDX-License-Identifier: CC-BY-SA-4.0
-->
# UART driver in Cogent
Prototype cogent UART driver for sabre. Need to have cogent installed and repository
checked out in `./tools/cogent`.
## To build
```sh
mkdir build
cd build
../init-build.sh -DCAMKES_APP=uart_cogent -DPLATFORM=sabre
ninja
```
## To run
```
$ ./simulate
qemu-system-arm -machine sabrelite -nographic -s -serial null -serial mon:stdio -m size=1024M -kernel images/capdl-loader-image-arm-imx6
ELF-loader started on CPU: ARM Ltd. Cortex-A9 r0p0
paddr=[20000000..2025bfff]
ELF-loading image 'kernel'
paddr=[10000000..10036fff]
vaddr=[e0000000..e0036fff]
virt_entry=e0000000
ELF-loading image 'capdl-loader'
paddr=[10037000..10181fff]
vaddr=[10000..15afff]
virt_entry=1e518
Enabling MMU and paging
Jumping to kernel-image entry point...
Bootstrapping kernel
Warning: Could not infer GIC interrupt target ID, assuming 0.
Booting all finished, dropped to user space
This message is sent via UART.
Input from UART: f
Input from UART: g
Input from UART: d
Input from UART: g
Input from UART: q
UART client exit...
```

View File

@ -1,10 +0,0 @@
/*
* Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
component Client {
control;
uses uart_inf uart;
}

View File

@ -1,44 +0,0 @@
/*
* Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#include <camkes.h>
#include <string.h>
#include <stdio.h>
#include <limits.h>
static size_t uart_write(void *buf, size_t count)
{
char *data = buf;
for (size_t i = 0; i < count; ++i) {
uart_put_char(data[i]);
}
return count;
}
int run(void)
{
signed char c;
char *str = "This message is sent via UART.\n";
uart_write(str, strlen(str));
while (1) {
c = uart_get_char();
if (c != -1) {
printf("Input from UART: %c\n", c);
}
if (c == 'q') {
break;
}
}
printf("UART client exit...\n");
return 0;
}

View File

@ -1,11 +0,0 @@
/*
* Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
component Driver {
provides uart_inf uart;
dataport Buf mem;
consumes DataAvailable irq;
}

View File

@ -1,7 +0,0 @@
--
-- Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
--
-- SPDX-License-Identifier: BSD-2-Clause
--
uart_init_cg

View File

@ -1,185 +0,0 @@
/*
* Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
$esc:(#include <stdint.h>)
$esc:(#include <stdlib.h>)
$esc:(#include <string.h>)
$esc:(#include <camkes/io.h>)
$esc:(#include <sel4/sel4.h>)
/* Cogent types */
typedef void *SysState;
#include "generated.c"
#define UART_SR1_RRDY BIT( 9)
#define UART_SR1_TRDY BIT(13)
/* CR1 */
#define UART_CR1_UARTEN BIT( 0)
#define UART_CR1_RRDYEN BIT( 9)
/* CR2 */
#define UART_CR2_SRST BIT( 0)
#define UART_CR2_RXEN BIT( 1)
#define UART_CR2_TXEN BIT( 2)
#define UART_CR2_ATEN BIT( 3)
#define UART_CR2_RTSEN BIT( 4)
#define UART_CR2_WS BIT( 5)
#define UART_CR2_STPB BIT( 6)
#define UART_CR2_PROE BIT( 7)
#define UART_CR2_PREN BIT( 8)
#define UART_CR2_RTEC BIT( 9)
#define UART_CR2_ESCEN BIT(11)
#define UART_CR2_CTS BIT(12)
#define UART_CR2_CTSC BIT(13)
#define UART_CR2_IRTS BIT(14)
#define UART_CR2_ESCI BIT(15)
/* CR3 */
#define UART_CR3_RXDMUXDEL BIT( 2)
/* FCR */
#define UART_FCR_RFDIV(x) ((x) * BIT(7))
#define UART_FCR_RFDIV_MASK UART_FCR_RFDIV(0x7)
#define UART_FCR_RXTL(x) ((x) * BIT(0))
#define UART_FCR_RXTL_MASK UART_FCR_RXTL(0x1F)
/* SR2 */
#define UART_SR2_RXFIFO_RDR BIT(0)
#define UART_SR2_TXFIFO_EMPTY BIT(14)
/* RXD */
#define UART_URXD_READY_MASK BIT(15)
#define UART_BYTE_MASK 0xFF
struct imx_uart_regs {
uint32_t rxd; /* 0x000 Receiver Register */
uint32_t res0[15];
uint32_t txd; /* 0x040 Transmitter Register */
uint32_t res1[15];
uint32_t cr1; /* 0x080 Control Register 1 */
uint32_t cr2; /* 0x084 Control Register 2 */
uint32_t cr3; /* 0x088 Control Register 3 */
uint32_t cr4; /* 0x08C Control Register 4 */
uint32_t fcr; /* 0x090 FIFO Control Register */
uint32_t sr1; /* 0x094 Status Register 1 */
uint32_t sr2; /* 0x098 Status Register 2 */
uint32_t esc; /* 0x09c Escape Character Register */
uint32_t tim; /* 0x0a0 Escape Timer Register */
uint32_t bir; /* 0x0a4 BRM Incremental Register */
uint32_t bmr; /* 0x0a8 BRM Modulator Register */
uint32_t brc; /* 0x0ac Baud Rate Counter Register */
uint32_t onems; /* 0x0b0 One Millisecond Register */
uint32_t ts; /* 0x0b4 Test Register */
};
typedef volatile struct imx_uart_regs imx_uart_regs_t;
static imx_uart_regs_t *uart_regs = NULL;
static imx_uart_regs_t *uart_regs_from_cg($ty:(#IMXUartRegs) cgregs)
{
imx_uart_regs_t *regs = uart_regs;
regs->rxd = cgregs.rxd;
regs->txd = cgregs.txd;
regs->cr1 = cgregs.cr1;
regs->cr2 = cgregs.cr2;
regs->cr3 = cgregs.cr3;
regs->cr4 = cgregs.cr4;
regs->fcr = cgregs.fcr;
regs->sr1 = cgregs.sr1;
regs->sr2 = cgregs.sr2;
regs->esc = cgregs.esc;
regs->tim = cgregs.tim;
regs->bir = cgregs.bir;
regs->bmr = cgregs.bmr;
regs->brc = cgregs.brc;
regs->onems = cgregs.onems;
regs->ts = cgregs.ts;
return regs;
}
static $ty:(#IMXUartRegs) uart_regs_to_cg(imx_uart_regs_t *regs)
{
$ty:(#IMXUartRegs) cgregs;
cgregs.rxd = regs->rxd;
cgregs.txd = regs->txd;
cgregs.cr1 = regs->cr1;
cgregs.cr2 = regs->cr2;
cgregs.cr3 = regs->cr3;
cgregs.cr4 = regs->cr4;
cgregs.fcr = regs->fcr;
cgregs.sr1 = regs->sr1;
cgregs.sr2 = regs->sr2;
cgregs.esc = regs->esc;
cgregs.tim = regs->tim;
cgregs.bir = regs->bir;
cgregs.bmr = regs->bmr;
cgregs.brc = regs->brc;
cgregs.onems = regs->onems;
cgregs.ts = regs->ts;
return cgregs;
}
void irq_handle(void)
{
/* TODO */
}
char uart_get_char()
{
imx_uart_regs_t* regs = uart_regs;
uint32_t reg = 0;
int c = -1;
if (regs->sr2 & UART_SR2_RXFIFO_RDR) {
reg = regs->rxd;
if (reg & UART_URXD_READY_MASK) {
c = reg & UART_BYTE_MASK;
}
}
return c;
}
void uart_put_char(char c)
{
if (c == '\n') {
uart_put_char('\r');
}
/* Block until space in FIFO */
while (!(uart_regs->sr2 & UART_SR2_TXFIFO_EMPTY)) {}
uart_regs->txd = c;
}
int uart__init(void)
{
ps_io_ops_t ops;
$ty:(#IMXUartRegs) regscg;
int error = camkes_io_ops(&ops);
ZF_LOGF_IF(error, "Failed to get malloc ops");
/* Attempt to map the virtual address, assure this works */
uart_regs = ps_io_map(&ops.io_mapper, 0x021E8000, 0x1000, false, PS_MEM_NORMAL);
if (uart_regs == NULL) {
return -1;
}
regscg = uart_regs_to_cg(uart_regs);
regscg = uart_init_cg(regscg);
uart_regs = uart_regs_from_cg(regscg);
/* Software reset */
while (!(uart_regs->cr2 & UART_CR2_SRST));
return 0;
}
static inline u32 u64_to_u32(u64 x)
{
return (u32) x;
}

View File

@ -1,187 +0,0 @@
--
-- Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
--
-- SPDX-License-Identifier: GPL-2.0-only
--
include <gum/common/common.cogent>
const_UART_REF_CLK : U32
const_UART_REF_CLK = 50000000
-- UART flags
flag_UART_SR1_RRDY : U32
flag_UART_SR1_RRDY = 1 << 9
flag_UART_SR1_TRDY : U32
flag_UART_SR1_TRDY = 1 << 13
-- CR1
flag_UART_CR1_UARTEN : U32
flag_UART_CR1_UARTEN = 1 << 0
flag_UART_CR1_RRDYEN : U32
flag_UART_CR1_RRDYEN = 1 << 9
-- CR2
flag_UART_CR2_SRST : U32
flag_UART_CR2_SRST = 1 << 0
flag_UART_CR2_RXEN : U32
flag_UART_CR2_RXEN = 1 << 1
flag_UART_CR2_TXEN : U32
flag_UART_CR2_TXEN = 1 << 2
flag_UART_CR2_ATEN : U32
flag_UART_CR2_ATEN = 1 << 3
flag_UART_CR2_RTSEN : U32
flag_UART_CR2_RTSEN = 1 << 4
flag_UART_CR2_WS : U32
flag_UART_CR2_WS = 1 << 5
flag_UART_CR2_STPB : U32
flag_UART_CR2_STPB = 1 << 6
flag_UART_CR2_PROE : U32
flag_UART_CR2_PROE = 1 << 7
flag_UART_CR2_PREN : U32
flag_UART_CR2_PREN = 1 << 8
flag_UART_CR2_RTEC : U32
flag_UART_CR2_RTEC = 1 << 9
flag_UART_CR2_ESCEN : U32
flag_UART_CR2_ESCEN = 1 << 11
flag_UART_CR2_CTS : U32
flag_UART_CR2_CTS = 1 << 12
flag_UART_CR2_CTSC : U32
flag_UART_CR2_CTSC = 1 << 13
flag_UART_CR2_IRTS : U32
flag_UART_CR2_IRTS = 1 << 14
flag_UART_CR2_ESCI : U32
flag_UART_CR2_ESCI = 1 << 15
-- CR3
flag_UART_CR3_RXDMUXDEL : U32
flag_UART_CR3_RXDMUXDEL = 1 << 2
-- FCR
uart_FCR_RFDIV : U32 -> U32
uart_FCR_RFDIV x = x * (1 << 7)
uart_FCR_RFDIV_MASK : () -> U32
uart_FCR_RFDIV_MASK () = uart_FCR_RFDIV 0x7
uart_FCR_RXTL : U32 -> U32
uart_FCR_RXTL x = x * (1 << 0)
uart_FCR_RXTL_MASK : () -> U32
uart_FCR_RXTL_MASK () = uart_FCR_RXTL 0x1F
-- SR2
flag_UART_SR2_RXFIFO_RDR : U32
flag_UART_SR2_RXFIFO_RDR = 1 << 0
flag_UART_SR2_TXFIFO_EMPTY : U32
flag_UART_SR2_TXFIFO_EMPTY = 1 << 14
-- RXD
flag_UART_URXD_READY_MASK : U32
flag_UART_URXD_READY_MASK = 1 << 15
flag_UART_BYTE_MASK : U32
flag_UART_BYTE_MASK = 0xFF
type IMXUartRegs = #{
rxd : U32 -- 0x000 Receiver Register
, txd : U32 -- 0x040 Transmitter Register
, cr1 : U32 -- 0x080 Control Register 1
, cr2 : U32 -- 0x084 Control Register 2
, cr3 : U32 -- 0x088 Control Register 3
, cr4 : U32 -- 0x08C Control Register 4
, fcr : U32 -- 0x090 FIFO Control Register
, sr1 : U32 -- 0x094 Status Register 1
, sr2 : U32 -- 0x098 Status Register 2
, esc : U32 -- 0x09C Escape Character Register
, tim : U32 -- 0x0A0 Escape Timer Register
, bir : U32 -- 0x0A4 BRM Incremental Register
, bmr : U32 -- 0x0A8 BRM Modulator Register
, brc : U32 -- 0x0AC Baud Rate Counter Register
, onems : U32 -- 0x0B0 One Millisecond Register
, ts : U32 -- 0x0B4 Test Register
}
imx_uart_set_baud_cg : (#IMXUartRegs, U64) -> #IMXUartRegs
imx_uart_set_baud_cg (regs, bps) =
let regs { fcr, bir, bmr } = regs
and fcr = fcr .&. complement (uart_FCR_RFDIV_MASK ())
and fcr = fcr .|. uart_FCR_RFDIV 4
and bir = 0xF
and bmr = const_UART_REF_CLK / (u64_to_u32 bps - 1)
and regs = regs { fcr, bir, bmr }
in regs
type Parity = < PARITY_NONE | PARITY_EVEN | PARITY_ODD >
compute_cr2_by_parity : (Parity, U32) -> U32
compute_cr2_by_parity (p, cr2) = p
| PARITY_NONE -> let cr2 = cr2 .&. complement flag_UART_CR2_PREN
in cr2
| PARITY_ODD -> let cr2 = cr2 .|. flag_UART_CR2_PREN
and cr2 = cr2 .|. flag_UART_CR2_PROE
in cr2
| PARITY_EVEN -> let cr2 = cr2 .|. flag_UART_CR2_PREN
and cr2 = cr2 .&. complement flag_UART_CR2_PROE
in cr2
serial_configure_cg : (#IMXUartRegs, U64, U32, Parity, U32 ) -> #IMXUartRegs
serial_configure_cg (regs, bps, char_size, parity, stop_bits) =
let regs { cr2 } = regs
and cr2 =
-- character size
if | char_size == 8 -> cr2 .|. flag_UART_CR2_WS
| char_size == 7 -> cr2 .&. complement flag_UART_CR2_WS
| else -> 0 -- Need to fail here
and cr2 =
-- stop bits
if | stop_bits == 2 -> cr2 .|. flag_UART_CR2_STPB
| stop_bits == 1 -> cr2 .&. complement flag_UART_CR2_STPB
| else -> 0 -- Need to fail here
and cr2 = compute_cr2_by_parity (parity, cr2)
and regs = regs { cr2 }
and regs = imx_uart_set_baud_cg (regs, bps)
in regs
uart_sw_reset_cg : #IMXUartRegs -> #IMXUartRegs
uart_sw_reset_cg regs =
let regs { cr2 } = regs
and cr2 = cr2 .&. complement flag_UART_CR2_SRST
and regs = regs { cr2 }
in regs
uart_init_cg : #IMXUartRegs -> #IMXUartRegs
uart_init_cg regs =
let regs = uart_sw_reset_cg regs
and regs = serial_configure_cg (regs, 115200, 8, PARITY_NONE, 1)
-- enable the UART
and regs { cr1, cr2, cr3, fcr } = regs
and cr1 = cr1 .|. flag_UART_CR1_UARTEN
and cr2 = cr2 .|. flag_UART_CR2_RXEN .|. flag_UART_CR2_TXEN
and cr2 = cr2 .|. flag_UART_CR2_IRTS
and cr3 = cr3 .|. flag_UART_CR3_RXDMUXDEL
-- initialise the receiver interrupt
and cr1 = cr1 .&. complement flag_UART_CR1_RRDYEN
and fcr = fcr .&. complement (uart_FCR_RXTL_MASK ())
and fcr = fcr .|. uart_FCR_RXTL 1
and cr1 = cr1 .|. flag_UART_CR1_RRDYEN
and regs = regs { cr1, cr2, cr3, fcr }
in regs

View File

@ -1,8 +0,0 @@
--
-- Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
--
-- SPDX-License-Identifier: BSD-2-Clause
--
uint32_t
ps_io_ops_t

View File

@ -1,10 +0,0 @@
/*
* Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
procedure uart_inf {
char get_char();
void put_char(in char c);
};

View File

@ -1,37 +0,0 @@
/*
* Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
import <std_connector.camkes>;
import "interfaces/uart.idl4";
import "components/Driver/Driver.camkes";
import "components/Client/Client.camkes";
component UART {
hardware;
dataport Buf mem;
emits DataAvailable irq;
}
assembly {
composition {
component UART uart;
component Driver drv;
component Client client;
connection seL4HardwareInterrupt irq(from uart.irq, to drv.irq);
connection seL4HardwareMMIO uart_mem(from drv.mem, to uart.mem);
connection seL4RPCCall uart_inf(from client.uart, to drv.uart);
}
configuration {
uart.mem_paddr = 0x021E8000;
uart.mem_size = 0x1000;
uart.irq_irq_number = 59;
random.ID = 1;
}
}

View File

@ -19,7 +19,6 @@ list(
set(PICOTCP_PATH "${project_dir}/projects/picotcp" CACHE INTERNAL "")
set(OPENSBI_PATH "${project_dir}/tools/opensbi" CACHE STRING "OpenSBI Folder location")
set(COGENT_PATH ${project_dir}/tools/cogent/cogent CACHE INTERNAL "")
set(RUMPRUN_PATH ${project_dir}/tools/rumprun CACHE INTERNAL "")
set(SEL4_CONFIG_DEFAULT_ADVANCED ON)

View File

@ -67,7 +67,7 @@ set(cakeml_cmake "-DCAKEMLDIR=/cakeml -DCAKEML_BIN=/cake-x64-64/cake")
add_test_variant(cakeml_hello x86_64_sim cakeml)
add_test_variant(cakeml_tipc x86_64_sim cakeml)
foreach(app IN ITEMS fdtgen epit swapcounter testhwdataportlrgpages testnto1mmio uart_cogent)
foreach(app IN ITEMS fdtgen epit swapcounter testhwdataportlrgpages testnto1mmio)
add_test_variant(${app} sabre_sim "")
list(APPEND exclude_apps ${app})
endforeach()